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 ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 )

Proof

Step Hyp Ref Expression
1 ax-pow ⊢ ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) → 𝑦 ∈ 𝑥 )
2 df-ral ⊢ ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 ) )
3 imim2 ⊢ ( ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 ) → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) ) )
4 3 al2imi ⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 ) → ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) ) )
5 2 4 biimtrid ⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) ) )
6 5 imim1d ⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) → 𝑦 ∈ 𝑥 ) → ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) ) )
7 6 alimdv ⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ∀ 𝑦 ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) → 𝑦 ∈ 𝑥 ) → ∀ 𝑦 ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) ) )
8 7 eximdv ⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) → 𝑦 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) ) )
9 1 8 mpi ⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) )
10 axprlem1 ⊢ ∃ 𝑣 ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 )
11 9 10 exlimiiv ⊢ ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 )