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

Proof

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