TwonessLemma2 Show Code edit
thm (TwonessLemma2 () () (↔ (∃ a (∃ b (¬ (= a b)))) (∃ b (∃ c (¬ (= b c)))))
# Starting from the inside, our first substitution is <code>b = c → (a ≠ b ↔ a ≠ c)</code>
b c a EqualityBuilderLL
(→ (= b c) (↔ (= a b) (= a c)))
addNegationInConsequent
(→ (= b c) (↔ (¬ (= a b)) (¬ (= a c))))
# That leads to the variable change <code>∃ b a ≠ b ↔ ∃ c a ≠ c</code>.
ChangeVariableThereExists
(↔ (∃ b (¬ (= a b))) (∃ c (¬ (= a c))))
a buildThereExists
(↔ (∃ a (∃ b (¬ (= a b)))) (∃ a (∃ c (¬ (= a c)))))
# We repeat the process with the outer quantifiers. The substitution is <code>a = b → (∃ c a ≠ c ↔ ∃ c b ≠ c)</code>.
a b c EqualityBuilderRR
(→ (= a b) (↔ (= a c) (= b c)))
addNegationInConsequent
(→ (= a b) (↔ (¬ (= a c)) (¬ (= b c))))
c buildThereExistsInConsequent
(→ (= a b) (↔ (∃ c (¬ (= a c))) (∃ c (¬ (= b c)))))
# The corresponding variable change is <code>∃ a ∃ c a ≠ c ↔ ∃ b ∃ c b ≠ c</code>. Combining this with the first variable change proves our lemma.
ChangeVariableThereExists
(↔ (∃ a (∃ c (¬ (= a c)))) (∃ b (∃ c (¬ (= b c)))))
applyBiconditionalTransitivity
(↔ (∃ a (∃ b (¬ (= a b)))) (∃ b (∃ c (¬ (= b c)))))
)
edit