Metamath Proof Explorer

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 ⊢ ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x

Proof

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