Metamath Proof Explorer

Theorem axnulregtco

Description: Derivation of ax-nul from ax-reg and ax-tco . Use ax-nul instead. (Contributed by Matthew House, 7-Apr-2026) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axnulregtco ⊢ ∃ x ∀ y ¬ y ∈ x

Proof

Step Hyp Ref Expression
1 elequ1 ⊢ x = z → x ∈ w ↔ z ∈ w
2 1 biimprd ⊢ x = z → z ∈ w → x ∈ w
3 2 spimevw ⊢ z ∈ w → ∃ x x ∈ w
4 ax-reg ⊢ ∃ x x ∈ w → ∃ x x ∈ w ∧ ∀ y y ∈ x → ¬ y ∈ w
5 3 4 syl ⊢ z ∈ w → ∃ x x ∈ w ∧ ∀ y y ∈ x → ¬ y ∈ w
6 pm2.65 ⊢ y ∈ x → y ∈ w → y ∈ x → ¬ y ∈ w → ¬ y ∈ x
7 6 al2imi ⊢ ∀ y y ∈ x → y ∈ w → ∀ y y ∈ x → ¬ y ∈ w → ∀ y ¬ y ∈ x
8 7 imim2i ⊢ x ∈ w → ∀ y y ∈ x → y ∈ w → x ∈ w → ∀ y y ∈ x → ¬ y ∈ w → ∀ y ¬ y ∈ x
9 8 impd ⊢ x ∈ w → ∀ y y ∈ x → y ∈ w → x ∈ w ∧ ∀ y y ∈ x → ¬ y ∈ w → ∀ y ¬ y ∈ x
10 9 aleximi ⊢ ∀ x x ∈ w → ∀ y y ∈ x → y ∈ w → ∃ x x ∈ w ∧ ∀ y y ∈ x → ¬ y ∈ w → ∃ x ∀ y ¬ y ∈ x
11 5 10 mpan9 ⊢ z ∈ w ∧ ∀ x x ∈ w → ∀ y y ∈ x → y ∈ w → ∃ x ∀ y ¬ y ∈ x
12 ax-tco ⊢ ∃ w z ∈ w ∧ ∀ x x ∈ w → ∀ y y ∈ x → y ∈ w
13 11 12 exlimiiv ⊢ ∃ x ∀ y ¬ y ∈ x