EmptySetAsAbstraction Show Code edit
defthm (EmptySetAsAbstraction object (∅) () () (= (∅) (abstract y (⊥)))
# We need to prove { x | ⊥ } = { y | ⊥ }.
# We start with z ∈ { x | ⊥ } ↔ [ z / x ] ⊥.
emptySet z x axnul-with-subst
(∃ emptySet (∀ z (↔ (∈ z emptySet) (subst z x (⊥)))))
Abstraction
(↔ (∈ z (abstract x (⊥))) (subst z x (⊥)))
# But [ z / x ] ⊥ is just ⊥ (because x does not occur free in ⊥).
z x (⊥) NullSubstitution
(↔ (subst z x (⊥)) (⊥))
applyBiconditionalTransitivity
(↔ (∈ z (abstract x (⊥))) (⊥))
# The same process shows z ∈ { y | ⊥ } ↔ ⊥
emptySet z y axnul-with-subst
(∃ emptySet (∀ z (↔ (∈ z emptySet) (subst z y (⊥)))))
Abstraction
(↔ (∈ z (abstract y (⊥))) (subst z y (⊥)))
z y (⊥) NullSubstitution
(↔ (subst z y (⊥)) (⊥))
applyBiconditionalTransitivity
(↔ (∈ z (abstract y (⊥))) (⊥))
# Combining, we get z ∈ { x | ⊥ } ↔ z ∈ { y | ⊥ }, which leads to { x | ⊥ } = { y | ⊥ }
swapBiconditional
(↔ (⊥) (∈ z (abstract y (⊥))))
applyBiconditionalTransitivity
(↔ (∈ z (abstract x (⊥))) (∈ z (abstract y (⊥))))
applyExtensionality
(= (abstract x (⊥)) (abstract y (⊥)))
)
edit