Metamath Proof Explorer

Theorem axpowndlem2

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

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

Proof

Step Hyp Ref Expression
1 zfpow ⊢ ∃ w ∀ y ∀ w w ∈ y → w ∈ z → y ∈ w
2 19.8a ⊢ w ∈ y → ∃ z w ∈ y
3 sp ⊢ ∀ y w ∈ z → w ∈ z
4 2 3 imim12i ⊢ ∃ z w ∈ y → ∀ y w ∈ z → w ∈ y → w ∈ z
5 4 alimi ⊢ ∀ w ∃ z w ∈ y → ∀ y w ∈ z → ∀ w w ∈ y → w ∈ z
6 5 imim1i ⊢ ∀ w w ∈ y → w ∈ z → y ∈ w → ∀ w ∃ z w ∈ y → ∀ y w ∈ z → y ∈ w
7 6 alimi ⊢ ∀ y ∀ w w ∈ y → w ∈ z → y ∈ w → ∀ y ∀ w ∃ z w ∈ y → ∀ y w ∈ z → y ∈ w
8 1 7 eximii ⊢ ∃ w ∀ y ∀ w ∃ z w ∈ y → ∀ y w ∈ z → y ∈ w
9 nfnae ⊢ Ⅎ x ¬ ∀ x x = y
10 nfnae ⊢ Ⅎ x ¬ ∀ x x = z
11 9 10 nfan ⊢ Ⅎ x ¬ ∀ x x = y ∧ ¬ ∀ x x = z
12 nfnae ⊢ Ⅎ y ¬ ∀ x x = y
13 nfnae ⊢ Ⅎ y ¬ ∀ x x = z
14 12 13 nfan ⊢ Ⅎ y ¬ ∀ x x = y ∧ ¬ ∀ x x = z
15 nfv ⊢ Ⅎ w ¬ ∀ x x = y ∧ ¬ ∀ x x = z
16 nfnae ⊢ Ⅎ z ¬ ∀ x x = y
17 nfcvd ⊢ ¬ ∀ x x = y → Ⅎ _ x w
18 nfcvf ⊢ ¬ ∀ x x = y → Ⅎ _ x y
19 17 18 nfeld ⊢ ¬ ∀ x x = y → Ⅎ x w ∈ y
20 16 19 nfexd ⊢ ¬ ∀ x x = y → Ⅎ x ∃ z w ∈ y
21 20 adantr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∃ z w ∈ y
22 nfcvd ⊢ ¬ ∀ x x = z → Ⅎ _ x w
23 nfcvf ⊢ ¬ ∀ x x = z → Ⅎ _ x z
24 22 23 nfeld ⊢ ¬ ∀ x x = z → Ⅎ x w ∈ z
25 13 24 nfald ⊢ ¬ ∀ x x = z → Ⅎ x ∀ y w ∈ z
26 25 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∀ y w ∈ z
27 21 26 nfimd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∃ z w ∈ y → ∀ y w ∈ z
28 15 27 nfald ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∀ w ∃ z w ∈ y → ∀ y w ∈ z
29 18 17 nfeld ⊢ ¬ ∀ x x = y → Ⅎ x y ∈ w
30 29 adantr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x y ∈ w
31 28 30 nfimd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∀ w ∃ z w ∈ y → ∀ y w ∈ z → y ∈ w
32 14 31 nfald ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ x ∀ y ∀ w ∃ z w ∈ y → ∀ y w ∈ z → y ∈ w
33 nfeqf2 ⊢ ¬ ∀ y y = x → Ⅎ y w = x
34 33 naecoms ⊢ ¬ ∀ x x = y → Ⅎ y w = x
35 34 adantr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → Ⅎ y w = x
36 14 35 nfan1 ⊢ Ⅎ y ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x
37 nfnae ⊢ Ⅎ z ¬ ∀ x x = z
38 nfeqf2 ⊢ ¬ ∀ z z = x → Ⅎ z w = x
39 38 naecoms ⊢ ¬ ∀ x x = z → Ⅎ z w = x
40 37 39 nfan1 ⊢ Ⅎ z ¬ ∀ x x = z ∧ w = x
41 elequ1 ⊢ w = x → w ∈ y ↔ x ∈ y
42 41 adantl ⊢ ¬ ∀ x x = z ∧ w = x → w ∈ y ↔ x ∈ y
43 40 42 exbid ⊢ ¬ ∀ x x = z ∧ w = x → ∃ z w ∈ y ↔ ∃ z x ∈ y
44 43 adantll ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∃ z w ∈ y ↔ ∃ z x ∈ y
45 12 34 nfan1 ⊢ Ⅎ y ¬ ∀ x x = y ∧ w = x
46 elequ1 ⊢ w = x → w ∈ z ↔ x ∈ z
47 46 adantl ⊢ ¬ ∀ x x = y ∧ w = x → w ∈ z ↔ x ∈ z
48 45 47 albid ⊢ ¬ ∀ x x = y ∧ w = x → ∀ y w ∈ z ↔ ∀ y x ∈ z
49 48 adantlr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∀ y w ∈ z ↔ ∀ y x ∈ z
50 44 49 imbi12d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∃ z w ∈ y → ∀ y w ∈ z ↔ ∃ z x ∈ y → ∀ y x ∈ z
51 50 ex ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → w = x → ∃ z w ∈ y → ∀ y w ∈ z ↔ ∃ z x ∈ y → ∀ y x ∈ z
52 11 27 51 cbvald ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∀ w ∃ z w ∈ y → ∀ y w ∈ z ↔ ∀ x ∃ z x ∈ y → ∀ y x ∈ z
53 52 adantr ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∀ w ∃ z w ∈ y → ∀ y w ∈ z ↔ ∀ x ∃ z x ∈ y → ∀ y x ∈ z
54 elequ2 ⊢ w = x → y ∈ w ↔ y ∈ x
55 54 adantl ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → y ∈ w ↔ y ∈ x
56 53 55 imbi12d ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∀ w ∃ z w ∈ y → ∀ y w ∈ z → y ∈ w ↔ ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
57 36 56 albid ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z ∧ w = x → ∀ y ∀ w ∃ z w ∈ y → ∀ y w ∈ z → y ∈ w ↔ ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
58 57 ex ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → w = x → ∀ y ∀ w ∃ z w ∈ y → ∀ y w ∈ z → y ∈ w ↔ ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
59 11 32 58 cbvexd ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∃ w ∀ y ∀ w ∃ z w ∈ y → ∀ y w ∈ z → y ∈ w ↔ ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
60 8 59 mpbii ⊢ ¬ ∀ x x = y ∧ ¬ ∀ x x = z → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x
61 60 ex ⊢ ¬ ∀ x x = y → ¬ ∀ x x = z → ∃ x ∀ y ∀ x ∃ z x ∈ y → ∀ y x ∈ z → y ∈ x