This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axprlem2

Description: Lemma for axpr . There exists a set to which all sets whose only members are empty sets belong. (Contributed by Rohan Ridenour, 9-Aug-2023) (Revised by BJ, 13-Aug-2023)

Ref Expression
Assertion axprlem2 ⊢ ∃ x ∀ y ∀ z ∈ y ∀ w ¬ w ∈ z → y ∈ x

Proof

Step Hyp Ref Expression
1 ax-pow ⊢ ∃ x ∀ y ∀ z z ∈ y → z ∈ v → y ∈ x
2 df-ral ⊢ ∀ z ∈ y ∀ w ¬ w ∈ z ↔ ∀ z z ∈ y → ∀ w ¬ w ∈ z
3 imim2 ⊢ ∀ w ¬ w ∈ z → z ∈ v → z ∈ y → ∀ w ¬ w ∈ z → z ∈ y → z ∈ v
4 3 al2imi ⊢ ∀ z ∀ w ¬ w ∈ z → z ∈ v → ∀ z z ∈ y → ∀ w ¬ w ∈ z → ∀ z z ∈ y → z ∈ v
5 2 4 biimtrid ⊢ ∀ z ∀ w ¬ w ∈ z → z ∈ v → ∀ z ∈ y ∀ w ¬ w ∈ z → ∀ z z ∈ y → z ∈ v
6 5 imim1d ⊢ ∀ z ∀ w ¬ w ∈ z → z ∈ v → ∀ z z ∈ y → z ∈ v → y ∈ x → ∀ z ∈ y ∀ w ¬ w ∈ z → y ∈ x
7 6 alimdv ⊢ ∀ z ∀ w ¬ w ∈ z → z ∈ v → ∀ y ∀ z z ∈ y → z ∈ v → y ∈ x → ∀ y ∀ z ∈ y ∀ w ¬ w ∈ z → y ∈ x
8 7 eximdv ⊢ ∀ z ∀ w ¬ w ∈ z → z ∈ v → ∃ x ∀ y ∀ z z ∈ y → z ∈ v → y ∈ x → ∃ x ∀ y ∀ z ∈ y ∀ w ¬ w ∈ z → y ∈ x
9 1 8 mpi ⊢ ∀ z ∀ w ¬ w ∈ z → z ∈ v → ∃ x ∀ y ∀ z ∈ y ∀ w ¬ w ∈ z → y ∈ x
10 axprlem1 ⊢ ∃ v ∀ z ∀ w ¬ w ∈ z → z ∈ v
11 9 10 exlimiiv ⊢ ∃ x ∀ y ∀ z ∈ y ∀ w ¬ w ∈ z → y ∈ x