Metamath Proof Explorer

Theorem axacnd

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

Ref Expression
Assertion axacnd ⊢∃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 axacndlem5 ⊢∃x∀y∀v∀xy∈v∧v∈w→∃w∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w
2 nfnae ⊢Ⅎx¬∀zz=x
3 nfnae ⊢Ⅎx¬∀zz=y
4 nfnae ⊢Ⅎx¬∀zz=w
5 2 3 4 nf3an ⊢Ⅎx¬∀zz=x∧¬∀zz=y∧¬∀zz=w
6 nfnae ⊢Ⅎy¬∀zz=x
7 nfnae ⊢Ⅎy¬∀zz=y
8 nfnae ⊢Ⅎy¬∀zz=w
9 6 7 8 nf3an ⊢Ⅎy¬∀zz=x∧¬∀zz=y∧¬∀zz=w
10 nfnae ⊢Ⅎz¬∀zz=x
11 nfnae ⊢Ⅎz¬∀zz=y
12 nfnae ⊢Ⅎz¬∀zz=w
13 10 11 12 nf3an ⊢Ⅎz¬∀zz=x∧¬∀zz=y∧¬∀zz=w
14 nfcvf ⊢¬∀zz=y→Ⅎ_zy
15 14 3ad2ant2 ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_zy
16 nfcvd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_zv
17 15 16 nfeld ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎzy∈v
18 nfcvf ⊢¬∀zz=w→Ⅎ_zw
19 18 3ad2ant3 ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_zw
20 16 19 nfeld ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎzv∈w
21 17 20 nfand ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎzy∈v∧v∈w
22 5 21 nfald ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎz∀xy∈v∧v∈w
23 nfnae ⊢Ⅎw¬∀zz=x
24 nfnae ⊢Ⅎw¬∀zz=y
25 nfnae ⊢Ⅎw¬∀zz=w
26 23 24 25 nf3an ⊢Ⅎw¬∀zz=x∧¬∀zz=y∧¬∀zz=w
27 15 19 nfeld ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎzy∈w
28 nfcvf ⊢¬∀zz=x→Ⅎ_zx
29 28 3ad2ant1 ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_zx
30 19 29 nfeld ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎzw∈x
31 27 30 nfand ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎzy∈w∧w∈x
32 21 31 nfand ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎzy∈v∧v∈w∧y∈w∧w∈x
33 26 32 nfexd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎz∃wy∈v∧v∈w∧y∈w∧w∈x
34 15 19 nfeqd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎzy=w
35 33 34 nfbid ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎz∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w
36 9 35 nfald ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎz∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w
37 26 36 nfexd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎz∃w∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w
38 22 37 nfimd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎz∀xy∈v∧v∈w→∃w∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w
39 nfcvd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_xv
40 nfcvf2 ⊢¬∀zz=x→Ⅎ_xz
41 40 3ad2ant1 ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_xz
42 39 41 nfeqd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎxv=z
43 5 42 nfan1 ⊢Ⅎx¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z
44 simpr ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→v=z
45 44 eleq2d ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→y∈v↔y∈z
46 44 eleq1d ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→v∈w↔z∈w
47 45 46 anbi12d ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→y∈v∧v∈w↔y∈z∧z∈w
48 43 47 albid ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→∀xy∈v∧v∈w↔∀xy∈z∧z∈w
49 nfcvd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_wv
50 nfcvf2 ⊢¬∀zz=w→Ⅎ_wz
51 50 3ad2ant3 ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_wz
52 49 51 nfeqd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎwv=z
53 26 52 nfan1 ⊢Ⅎw¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z
54 nfcvd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_yv
55 nfcvf2 ⊢¬∀zz=y→Ⅎ_yz
56 55 3ad2ant2 ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎ_yz
57 54 56 nfeqd ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→Ⅎyv=z
58 9 57 nfan1 ⊢Ⅎy¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z
59 47 anbi1d ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→y∈v∧v∈w∧y∈w∧w∈x↔y∈z∧z∈w∧y∈w∧w∈x
60 53 59 exbid ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→∃wy∈v∧v∈w∧y∈w∧w∈x↔∃wy∈z∧z∈w∧y∈w∧w∈x
61 60 bibi1d ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w↔∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
62 58 61 albid ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w↔∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
63 53 62 exbid ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→∃w∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w↔∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
64 48 63 imbi12d ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w∧v=z→∀xy∈v∧v∈w→∃w∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w↔∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
65 64 ex ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→v=z→∀xy∈v∧v∈w→∃w∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w↔∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
66 13 38 65 cbvald ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→∀v∀xy∈v∧v∈w→∃w∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w↔∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
67 9 66 albid ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→∀y∀v∀xy∈v∧v∈w→∃w∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w↔∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
68 5 67 exbid ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→∃x∀y∀v∀xy∈v∧v∈w→∃w∀y∃wy∈v∧v∈w∧y∈w∧w∈x↔y=w↔∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
69 1 68 mpbii ⊢¬∀zz=x∧¬∀zz=y∧¬∀zz=w→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
70 69 3exp ⊢¬∀zz=x→¬∀zz=y→¬∀zz=w→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
71 axacndlem2 ⊢∀xx=z→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
72 71 aecoms ⊢∀zz=x→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
73 axacndlem3 ⊢∀yy=z→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
74 73 aecoms ⊢∀zz=y→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
75 nfae ⊢Ⅎy∀zz=w
76 simpr ⊢y∈z∧z∈w→z∈w
77 76 alimi ⊢∀xy∈z∧z∈w→∀xz∈w
78 nd3 ⊢∀zz=w→¬∀xz∈w
79 78 pm2.21d ⊢∀zz=w→∀xz∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
80 77 79 syl5 ⊢∀zz=w→∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
81 80 axc4i ⊢∀zz=w→∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
82 75 81 alrimi ⊢∀zz=w→∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
83 82 19.8ad ⊢∀zz=w→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
84 70 72 74 83 pm2.61iii ⊢∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w