Metamath Proof Explorer

Theorem axacndlem4

Description: Lemma for the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 8-Jan-2002) (Proof shortened by Mario Carneiro, 10-Dec-2016)

Ref Expression
Assertion axacndlem4 ⊢∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w

Proof

Step Hyp Ref Expression
1 zfac ⊢∃v∀y∀zy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w
2 nfnae ⊢Ⅎx¬∀xx=z
3 nfnae ⊢Ⅎx¬∀xx=y
4 nfnae ⊢Ⅎx¬∀xx=w
5 2 3 4 nf3an ⊢Ⅎx¬∀xx=z∧¬∀xx=y∧¬∀xx=w
6 nfnae ⊢Ⅎy¬∀xx=z
7 nfnae ⊢Ⅎy¬∀xx=y
8 nfnae ⊢Ⅎy¬∀xx=w
9 6 7 8 nf3an ⊢Ⅎy¬∀xx=z∧¬∀xx=y∧¬∀xx=w
10 nfnae ⊢Ⅎz¬∀xx=z
11 nfnae ⊢Ⅎz¬∀xx=y
12 nfnae ⊢Ⅎz¬∀xx=w
13 10 11 12 nf3an ⊢Ⅎz¬∀xx=z∧¬∀xx=y∧¬∀xx=w
14 nfcvf ⊢¬∀xx=y→Ⅎ_xy
15 14 3ad2ant2 ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_xy
16 nfcvf ⊢¬∀xx=z→Ⅎ_xz
17 16 3ad2ant1 ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_xz
18 15 17 nfeld ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎxy∈z
19 nfcvf ⊢¬∀xx=w→Ⅎ_xw
20 19 3ad2ant3 ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_xw
21 17 20 nfeld ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎxz∈w
22 18 21 nfand ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎxy∈z∧z∈w
23 nfnae ⊢Ⅎw¬∀xx=z
24 nfnae ⊢Ⅎw¬∀xx=y
25 nfnae ⊢Ⅎw¬∀xx=w
26 23 24 25 nf3an ⊢Ⅎw¬∀xx=z∧¬∀xx=y∧¬∀xx=w
27 15 20 nfeld ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎxy∈w
28 nfcvd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_xv
29 20 28 nfeld ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎxw∈v
30 27 29 nfand ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎxy∈w∧w∈v
31 22 30 nfand ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎxy∈z∧z∈w∧y∈w∧w∈v
32 26 31 nfexd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎx∃wy∈z∧z∈w∧y∈w∧w∈v
33 15 20 nfeqd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎxy=w
34 32 33 nfbid ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎx∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w
35 9 34 nfald ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎx∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w
36 26 35 nfexd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎx∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w
37 22 36 nfimd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎxy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w
38 13 37 nfald ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎx∀zy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w
39 9 38 nfald ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎx∀y∀zy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w
40 nfcvd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_yv
41 nfcvf2 ⊢¬∀xx=y→Ⅎ_yx
42 41 3ad2ant2 ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_yx
43 40 42 nfeqd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎyv=x
44 9 43 nfan1 ⊢Ⅎy¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x
45 nfcvd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_zv
46 nfcvf2 ⊢¬∀xx=z→Ⅎ_zx
47 46 3ad2ant1 ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_zx
48 45 47 nfeqd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎzv=x
49 13 48 nfan1 ⊢Ⅎz¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x
50 22 nf5rd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→y∈z∧z∈w→∀xy∈z∧z∈w
51 50 adantr ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→y∈z∧z∈w→∀xy∈z∧z∈w
52 sp ⊢∀xy∈z∧z∈w→y∈z∧z∈w
53 51 52 impbid1 ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→y∈z∧z∈w↔∀xy∈z∧z∈w
54 nfcvd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_wv
55 nfcvf2 ⊢¬∀xx=w→Ⅎ_wx
56 55 3ad2ant3 ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎ_wx
57 54 56 nfeqd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→Ⅎwv=x
58 26 57 nfan1 ⊢Ⅎw¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x
59 simpr ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→v=x
60 59 eleq2d ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→w∈v↔w∈x
61 60 anbi2d ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→y∈w∧w∈v↔y∈w∧w∈x
62 61 anbi2d ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→y∈z∧z∈w∧y∈w∧w∈v↔y∈z∧z∈w∧y∈w∧w∈x
63 58 62 exbid ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→∃wy∈z∧z∈w∧y∈w∧w∈v↔∃wy∈z∧z∈w∧y∈w∧w∈x
64 63 bibi1d ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w↔∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
65 44 64 albid ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w↔∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
66 58 65 exbid ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w↔∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
67 53 66 imbi12d ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→y∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w↔∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
68 49 67 albid ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→∀zy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w↔∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
69 44 68 albid ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w∧v=x→∀y∀zy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w↔∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
70 69 ex ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→v=x→∀y∀zy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w↔∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
71 5 39 70 cbvexd ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→∃v∀y∀zy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈v↔y=w↔∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
72 1 71 mpbii ⊢¬∀xx=z∧¬∀xx=y∧¬∀xx=w→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
73 72 3exp ⊢¬∀xx=z→¬∀xx=y→¬∀xx=w→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
74 axacndlem2 ⊢∀xx=z→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
75 axacndlem1 ⊢∀xx=y→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
76 nfae ⊢Ⅎy∀xx=w
77 nfae ⊢Ⅎz∀xx=w
78 simpr ⊢y∈z∧z∈w→z∈w
79 78 alimi ⊢∀xy∈z∧z∈w→∀xz∈w
80 nd2 ⊢∀xx=w→¬∀xz∈w
81 80 pm2.21d ⊢∀xx=w→∀xz∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
82 79 81 syl5 ⊢∀xx=w→∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
83 77 82 alrimi ⊢∀xx=w→∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
84 76 83 alrimi ⊢∀xx=w→∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
85 84 19.8ad ⊢∀xx=w→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
86 73 74 75 85 pm2.61iii ⊢∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w