UnorderedPairBuilder-1 Show Code edit
thm (UnorderedPairBuilder-1
((A0 a) (A1 a) (B0 b) (B1 b))
()
(→ (∧ (= A0 B0) (= A1 B1)) (= (abstract a (∨ (= a A0) (= a A1))) (abstract b (∨ (= b B0) (= b B1)))))
# Applying builders for equality and disjunction, we get <code>A0 = B0 ∧ A1 = B1 → (z = A0 ∨ z = A1 ↔ z = B0 ∨ z = B1)</code>.
(= A0 B0) (= A1 B1) ConjunctionRightElimination
(→ (∧ (= A0 B0) (= A1 B1)) (= A0 B0))
A0 B0 z EqualityBuilderLL
(→ (= A0 B0) (↔ (= z A0) (= z B0)))
applySyllogism
(→ (∧ (= A0 B0) (= A1 B1)) (↔ (= z A0) (= z B0)))
(= A0 B0) (= A1 B1) ConjunctionLeftElimination
(→ (∧ (= A0 B0) (= A1 B1)) (= A1 B1))
A1 B1 z EqualityBuilderLL
(→ (= A1 B1) (↔ (= z A1) (= z B1)))
applySyllogism
(→ (∧ (= A0 B0) (= A1 B1)) (↔ (= z A1) (= z B1)))
composeConjunction
(→ (∧ (= A0 B0) (= A1 B1)) (∧ (↔ (= z A0) (= z B0)) (↔ (= z A1) (= z B1))))
(= z A0) (= z B0) (= z A1) (= z B1) DisjunctionFunction
(→ (∧ (↔ (= z A0) (= z B0)) (↔ (= z A1) (= z B1))) (↔ (∨ (= z A0) (= z A1)) (∨ (= z B0) (= z B1))))
applySyllogism
(→ (∧ (= A0 B0) (= A1 B1)) (↔ (∨ (= z A0) (= z A1)) (∨ (= z B0) (= z B1))))
# Applying <code>UnorderedPair</code>, we get <code>A0 = B0 ∧ A1 = B1 → (z ∈ {A0, A1} ↔ z ∈ {B0, B1})</code>.
z a A0 A1 UnorderedPairObject
(↔ (∈ z (abstract a (∨ (= a A0) (= a A1)))) (∨ (= z A0) (= z A1)))
swapBiconditional
(↔ (∨ (= z A0) (= z A1)) (∈ z (abstract a (∨ (= a A0) (= a A1)))))
transformImplicationBiconditionalLeft
(→ (∧ (= A0 B0) (= A1 B1)) (↔ (∈ z (abstract a (∨ (= a A0) (= a A1)))) (∨ (= z B0) (= z B1))))
z b B0 B1 UnorderedPairObject
(↔ (∈ z (abstract b (∨ (= b B0) (= b B1)))) (∨ (= z B0) (= z B1)))
swapBiconditional
(↔ (∨ (= z B0) (= z B1)) (∈ z (abstract b (∨ (= b B0) (= b B1)))))
transformImplicationBiconditionalRight
(→ (∧ (= A0 B0) (= A1 B1)) (↔ (∈ z (abstract a (∨ (= a A0) (= a A1)))) (∈ z (abstract b (∨ (= b B0) (= b B1))))))
# By extensionality, the right hand side implies <code>{A0, A1} = {B0, B1}</code>.
z addForAllToConsequent
(→ (∧ (= A0 B0) (= A1 B1)) (∀ z (↔ (∈ z (abstract a (∨ (= a A0) (= a A1)))) (∈ z (abstract b (∨ (= b B0) (= b B1)))))))
z (abstract a (∨ (= a A0) (= a A1))) (abstract b (∨ (= b B0) (= b B1))) Extensionality
(→ (∀ z (↔ (∈ z (abstract a (∨ (= a A0) (= a A1)))) (∈ z (abstract b (∨ (= b B0) (= b B1)))))) (= (abstract a (∨ (= a A0) (= a A1))) (abstract b (∨ (= b B0) (= b B1)))))
applySyllogism
(→ (∧ (= A0 B0) (= A1 B1)) (= (abstract a (∨ (= a A0) (= a A1))) (abstract b (∨ (= b B0) (= b B1)))))
)
edit