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