Metamath Proof Explorer

Theorem axpowndlem4

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) (Proof shortened by Mario Carneiro, 10-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion axpowndlem4 ⊢ ¬ ∀ y y = x → ¬ ∀ y y = z → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x

Proof

Step Hyp Ref Expression
1 axpowndlem3 ⊢ ¬ x = w → ∃ x ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x
2 1 ax-gen ⊢ ∀ w ¬ x = w → ∃ x ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x
3 nfnae ⊢ Ⅎ y ¬ ∀ y y = x
4 nfnae ⊢ Ⅎ y ¬ ∀ y y = z
5 3 4 nfan ⊢ Ⅎ y ¬ ∀ y y = x ∧ ¬ ∀ y y = z
6 nfcvf ⊢ ¬ ∀ y y = x → Ⅎ _ y x
7 6 adantr ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ _ y x
8 nfcvd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ _ y w
9 7 8 nfeqd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y x = w
10 9 nfnd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y ¬ x = w
11 nfnae ⊢ Ⅎ x ¬ ∀ y y = x
12 nfnae ⊢ Ⅎ x ¬ ∀ y y = z
13 11 12 nfan ⊢ Ⅎ x ¬ ∀ y y = x ∧ ¬ ∀ y y = z
14 nfv ⊢ Ⅎ w ¬ ∀ y y = x ∧ ¬ ∀ y y = z
15 nfnae ⊢ Ⅎ z ¬ ∀ y y = x
16 nfnae ⊢ Ⅎ z ¬ ∀ y y = z
17 15 16 nfan ⊢ Ⅎ z ¬ ∀ y y = x ∧ ¬ ∀ y y = z
18 7 8 nfeld ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y x ∈ w
19 17 18 nfexd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y ∃ z x ∈ w
20 nfcvf ⊢ ¬ ∀ y y = z → Ⅎ _ y z
21 20 adantl ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ _ y z
22 7 21 nfeld ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y x ∈ z
23 14 22 nfald ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y ∀ w x ∈ z
24 19 23 nfimd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y ∃ z x ∈ w → ∀ w x ∈ z
25 13 24 nfald ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y ∀ x ∃ z x ∈ w → ∀ w x ∈ z
26 8 7 nfeld ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y w ∈ x
27 25 26 nfimd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x
28 14 27 nfald ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x
29 13 28 nfexd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y ∃ x ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x
30 10 29 nfimd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ y ¬ x = w → ∃ x ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x
31 equequ2 ⊢ w = y → x = w ↔ x = y
32 31 notbid ⊢ w = y → ¬ x = w ↔ ¬ x = y
33 32 adantl ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → ¬ x = w ↔ ¬ x = y
34 nfcvd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ _ x w
35 nfcvf2 ⊢ ¬ ∀ y y = x → Ⅎ _ x y
36 35 adantr ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ _ x y
37 34 36 nfeqd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ x w = y
38 13 37 nfan1 ⊢ Ⅎ x ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y
39 nfcvd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ _ z w
40 nfcvf2 ⊢ ¬ ∀ y y = z → Ⅎ _ z y
41 40 adantl ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ _ z y
42 39 41 nfeqd ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → Ⅎ z w = y
43 17 42 nfan1 ⊢ Ⅎ z ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y
44 elequ2 ⊢ w = y → x ∈ w ↔ x ∈ y
45 44 adantl ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → x ∈ w ↔ x ∈ y
46 43 45 exbid ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → ∃ z x ∈ w ↔ ∃ z x ∈ y
47 biidd ⊢ w = y → x ∈ z ↔ x ∈ z
48 47 a1i ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → w = y → x ∈ z ↔ x ∈ z
49 5 22 48 cbvald ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → ∀ w x ∈ z ↔ ∀ y x ∈ z
50 49 adantr ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → ∀ w x ∈ z ↔ ∀ y x ∈ z
51 46 50 imbi12d ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → ∃ z x ∈ w → ∀ w x ∈ z ↔ ∃ z x ∈ y → ∀ y x ∈ z
52 38 51 albid ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → ∀ x ∃ z x ∈ w → ∀ w x ∈ z ↔ ∀ x ∃ z x ∈ y → ∀ y x ∈ z
53 elequ1 ⊢ w = y → w ∈ x ↔ y ∈ x
54 53 adantl ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → w ∈ x ↔ y ∈ x
55 52 54 imbi12d ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x ↔ ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
56 55 ex ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → w = y → ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x ↔ ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
57 5 27 56 cbvald ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x ↔ ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
58 13 57 exbid ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → ∃ x ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x ↔ ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
59 58 adantr ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → ∃ x ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x ↔ ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
60 33 59 imbi12d ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z ∧ w = y → ¬ x = w → ∃ x ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x ↔ ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
61 60 ex ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → w = y → ¬ x = w → ∃ x ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x ↔ ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
62 5 30 61 cbvald ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → ∀ w ¬ x = w → ∃ x ∀ w ∀ x ∃ z x ∈ w → ∀ w x ∈ z → w ∈ x ↔ ∀ y ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
63 2 62 mpbii ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → ∀ y ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
64 63 19.21bi ⊢ ¬ ∀ y y = x ∧ ¬ ∀ y y = z → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
65 64 ex ⊢ ¬ ∀ y y = x → ¬ ∀ y y = z → ¬ x = y → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x