Theorem axpowndlem3

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 4-Jan-2002) (Revised by Mario Carneiro, 10-Dec-2016) (Proof shortened by Wolf Lammen, 10-Jun-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	axpowndlem3	⊢ ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		sp	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
2		p0ex	⊢ { ∅ } ∈ V
3		eleq2	⊢ ( 𝑥 = { ∅ } → ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ { ∅ } ) )
4	3	imbi2d	⊢ ( 𝑥 = { ∅ } → ( ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) ↔ ( 𝑤 = ∅ → 𝑤 ∈ { ∅ } ) ) )
5	4	albidv	⊢ ( 𝑥 = { ∅ } → ( ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ { ∅ } ) ) )
6	2 5	spcev	⊢ ( ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ { ∅ } ) → ∃ 𝑥 ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) )
7		0ex	⊢ ∅ ∈ V
8	7	snid	⊢ ∅ ∈ { ∅ }
9		eleq1	⊢ ( 𝑤 = ∅ → ( 𝑤 ∈ { ∅ } ↔ ∅ ∈ { ∅ } ) )
10	8 9	mpbiri	⊢ ( 𝑤 = ∅ → 𝑤 ∈ { ∅ } )
11	6 10	mpg	⊢ ∃ 𝑥 ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 )
12		neq0	⊢ ( ¬ 𝑤 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑤 )
13	12	con1bii	⊢ ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 ↔ 𝑤 = ∅ )
14	13	imbi1i	⊢ ( ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) )
15	14	albii	⊢ ( ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) )
16	15	exbii	⊢ ( ∃ 𝑥 ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑤 ( 𝑤 = ∅ → 𝑤 ∈ 𝑥 ) )
17	11 16	mpbir	⊢ ∃ 𝑥 ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 )
18		nfnae	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
19		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
20		nfcvf2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 )
21		nfcvd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 )
22	20 21	nfeld	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 ∈ 𝑤 )
23	18 22	nfexd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ∃ 𝑥 𝑥 ∈ 𝑤 )
24	23	nfnd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ¬ ∃ 𝑥 𝑥 ∈ 𝑤 )
25	21 20	nfeld	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 ∈ 𝑥 )
26	24 25	nfimd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) )
27		nfeqf2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑤 = 𝑦 )
28	18 27	nfan1	⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 )
29		elequ2	⊢ ( 𝑤 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
30	29	adantl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( 𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦 ) )
31	28 30	exbid	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑥 𝑥 ∈ 𝑤 ↔ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
32	31	notbid	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 ↔ ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
33		elequ1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
34	33	adantl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( 𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
35	32 34	imbi12d	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑤 = 𝑦 ) → ( ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) ) )
36	35	ex	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ( ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) ) ) )
37	19 26 36	cbvald	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) ) )
38	18 37	exbid	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∀ 𝑤 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑤 → 𝑤 ∈ 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) ) )
39	17 38	mpbii	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) )
40		nfae	⊢ Ⅎ 𝑥 ∀ 𝑥 𝑥 = 𝑧
41		nfae	⊢ Ⅎ 𝑦 ∀ 𝑥 𝑥 = 𝑧
42		axc11r	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑧 ¬ 𝑥 ∈ 𝑦 → ∀ 𝑥 ¬ 𝑥 ∈ 𝑦 ) )
43		alnex	⊢ ( ∀ 𝑧 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑧 𝑥 ∈ 𝑦 )
44		alnex	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝑦 ↔ ¬ ∃ 𝑥 𝑥 ∈ 𝑦 )
45	42 43 44	3imtr3g	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∃ 𝑧 𝑥 ∈ 𝑦 → ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
46		nd3	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ¬ ∀ 𝑦 𝑥 ∈ 𝑧 )
47	46	pm2.21d	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑦 𝑥 ∈ 𝑧 → ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
48	45 47	jad	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
49	48	spsd	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → ¬ ∃ 𝑥 𝑥 ∈ 𝑦 ) )
50	49	imim1d	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) → ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
51	41 50	alimd	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) → ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
52	40 51	eximd	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑥 ∀ 𝑦 ( ¬ ∃ 𝑥 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
53	39 52	syl5com	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
54		axpowndlem2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
55	53 54	pm2.61d	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
56	1 55	nsyl5	⊢ ( ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( ∃ 𝑧 𝑥 ∈ 𝑦 → ∀ 𝑦 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )