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

Proof

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