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	syl5bi	⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) ) )
6	5	imim1d	⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) → 𝑦 ∈ 𝑥 ) → ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) ) )
7	6	alimdv	⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ∀ 𝑦 ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) → 𝑦 ∈ 𝑥 ) → ∀ 𝑦 ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) ) )
8	7	eximdv	⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ( ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑣 ) → 𝑦 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) ) )
9	1 8	mpi	⊢ ( ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 ) )
10		axprlem1	⊢ ∃ 𝑣 ∀ 𝑧 ( ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑧 ∈ 𝑣 )
11	9 10	exlimiiv	⊢ ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ¬ 𝑤 ∈ 𝑧 → 𝑦 ∈ 𝑥 )