EmptySetVariable Show Code edit
thm (EmptySetVariable () () (¬ (∈ x (∅)))
# To apply <code>Abstraction</code>, we need <code>∃ result ∀ x (x ∈ result ↔ [x / y]⊥)</code>. This follows from <code>axnul</code>, the <code>NegationBiconditional</code> relationship between negation and <code>⊥</code>, and the fact that substituting a variable in <code>⊥</code> has no effect.
result x axnul
(∃ result (∀ x (¬ (∈ x result))))
(∈ x result) NegationBiconditional
(↔ (¬ (∈ x result)) (↔ (∈ x result) (⊥)))
(∈ x result) BiconditionalReflexivity
(↔ (∈ x result) (∈ x result))
x y (⊥) NullSubstitution swapBiconditional
(↔ (⊥) (subst x y (⊥)))
buildBiconditional
(↔ (↔ (∈ x result) (⊥)) (↔ (∈ x result) (subst x y (⊥))))
applyBiconditionalTransitivity
(↔ (¬ (∈ x result)) (↔ (∈ x result) (subst x y (⊥))))
x buildForAll
(↔ (∀ x (¬ (∈ x result))) (∀ x (↔ (∈ x result) (subst x y (⊥)))))
result buildThereExists
(↔ (∃ result (∀ x (¬ (∈ x result)))) (∃ result (∀ x (↔ (∈ x result) (subst x y (⊥))))))
eliminateBiconditionalReverse
(→ (∃ result (∀ x (¬ (∈ x result)))) (∃ result (∀ x (↔ (∈ x result) (subst x y (⊥))))))
applyModusPonens
(∃ result (∀ x (↔ (∈ x result) (subst x y (⊥)))))
# Now that we have <code>∃ result ∀ x (x ∈ result ↔ [x / y] ⊥)</code>, we can apply <code>Abstraction</code> to get <code>x ∈ {y | ⊥} ↔ [x / y] ⊥</code>.
Abstraction
(↔ (∈ x (abstract y (⊥))) (subst x y (⊥)))
# Removing the substitution which has no effect
x y (⊥) NullSubstitution
(↔ (subst x y (⊥)) (⊥))
applyBiconditionalTransitivity
(↔ (∈ x (abstract y (⊥))) (⊥))
# gives us <code>x ∈ {y | ⊥} ↔ ⊥</code>
# and then <code>NegationBiconditional</code> gives us our desired result.
(∈ x (abstract y (⊥))) NegationBiconditional
(↔ (¬ (∈ x (abstract y (⊥)))) (↔ (∈ x (abstract y (⊥))) (⊥)))
eliminateBiconditionalForward
(→ (↔ (∈ x (abstract y (⊥))) (⊥)) (¬ (∈ x (abstract y (⊥)))))
applyModusPonens
(¬ (∈ x (abstract y (⊥))))
(= (∅) (abstract y (⊥)))
swapEquality
(= (abstract y (⊥)) (∅))
(abstract y (⊥)) (∅) x MembershipBuilderLL
(→ (= (abstract y (⊥)) (∅)) (↔ (∈ x (abstract y (⊥))) (∈ x (∅))))
applyModusPonens
(↔ (∈ x (abstract y (⊥))) (∈ x (∅)))