UnorderedPairBuilder Show Code edit
thm (UnorderedPairBuilder () () (→ (∧ (= A0 B0) (= A1 B1)) (= (unorderedPair A0 A1) (unorderedPair B0 B1)))
A0 B0 A1 B1 a b UnorderedPairBuilder-1
(→ (∧ (= A0 B0) (= A1 B1)) (= (abstract a (∨ (= a A0) (= a A1))) (abstract b (∨ (= b B0) (= b B1)))))
A0 A1 a UnorderedPairAsAbstraction
(= (unorderedPair A0 A1) (abstract a (∨ (= a A0) (= a A1))))
B0 B1 b UnorderedPairAsAbstraction
(= (unorderedPair B0 B1) (abstract b (∨ (= b B0) (= b B1))))
buildEquality
(↔ (= (unorderedPair A0 A1) (unorderedPair B0 B1)) (= (abstract a (∨ (= a A0) (= a A1))) (abstract b (∨ (= b B0) (= b B1)))))
eliminateBiconditionalForward
(→ (= (abstract a (∨ (= a A0) (= a A1))) (abstract b (∨ (= b B0) (= b B1)))) (= (unorderedPair A0 A1) (unorderedPair B0 B1)))
applySyllogism
(→ (∧ (= A0 B0) (= A1 B1)) (= (unorderedPair A0 A1) (unorderedPair B0 B1)))
)
edit