Metamath Proof Explorer

Theorem axacndlem5

Description: Lemma for 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 axacndlem5 ⊢∃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 axacndlem4 ⊢∃x∀v∀z∀xv∈z∧z∈w→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w
2 nfnae ⊢Ⅎx¬∀yy=z
3 nfnae ⊢Ⅎx¬∀yy=x
4 nfnae ⊢Ⅎx¬∀yy=w
5 2 3 4 nf3an ⊢Ⅎx¬∀yy=z∧¬∀yy=x∧¬∀yy=w
6 nfnae ⊢Ⅎy¬∀yy=z
7 nfnae ⊢Ⅎy¬∀yy=x
8 nfnae ⊢Ⅎy¬∀yy=w
9 6 7 8 nf3an ⊢Ⅎy¬∀yy=z∧¬∀yy=x∧¬∀yy=w
10 nfnae ⊢Ⅎz¬∀yy=z
11 nfnae ⊢Ⅎz¬∀yy=x
12 nfnae ⊢Ⅎz¬∀yy=w
13 10 11 12 nf3an ⊢Ⅎz¬∀yy=z∧¬∀yy=x∧¬∀yy=w
14 nfcvd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_yv
15 nfcvf ⊢¬∀yy=z→Ⅎ_yz
16 15 3ad2ant1 ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_yz
17 14 16 nfeld ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎyv∈z
18 nfcvf ⊢¬∀yy=w→Ⅎ_yw
19 18 3ad2ant3 ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_yw
20 16 19 nfeld ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎyz∈w
21 17 20 nfand ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎyv∈z∧z∈w
22 5 21 nfald ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎy∀xv∈z∧z∈w
23 nfnae ⊢Ⅎw¬∀yy=z
24 nfnae ⊢Ⅎw¬∀yy=x
25 nfnae ⊢Ⅎw¬∀yy=w
26 23 24 25 nf3an ⊢Ⅎw¬∀yy=z∧¬∀yy=x∧¬∀yy=w
27 nfv ⊢Ⅎv¬∀yy=z∧¬∀yy=x∧¬∀yy=w
28 14 19 nfeld ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎyv∈w
29 nfcvf ⊢¬∀yy=x→Ⅎ_yx
30 29 3ad2ant2 ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_yx
31 19 30 nfeld ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎyw∈x
32 28 31 nfand ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎyv∈w∧w∈x
33 21 32 nfand ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎyv∈z∧z∈w∧v∈w∧w∈x
34 26 33 nfexd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎy∃wv∈z∧z∈w∧v∈w∧w∈x
35 14 19 nfeqd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎyv=w
36 34 35 nfbid ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎy∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w
37 27 36 nfald ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎy∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w
38 26 37 nfexd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎy∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w
39 22 38 nfimd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎy∀xv∈z∧z∈w→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w
40 13 39 nfald ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎy∀z∀xv∈z∧z∈w→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w
41 nfcvd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_zv
42 nfcvf2 ⊢¬∀yy=z→Ⅎ_zy
43 42 3ad2ant1 ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_zy
44 41 43 nfeqd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎzv=y
45 13 44 nfan1 ⊢Ⅎz¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y
46 nfcvd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_xv
47 nfcvf2 ⊢¬∀yy=x→Ⅎ_xy
48 47 3ad2ant2 ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_xy
49 46 48 nfeqd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎxv=y
50 5 49 nfan1 ⊢Ⅎx¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y
51 simpr ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→v=y
52 51 eleq1d ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→v∈z↔y∈z
53 52 anbi1d ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→v∈z∧z∈w↔y∈z∧z∈w
54 50 53 albid ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→∀xv∈z∧z∈w↔∀xy∈z∧z∈w
55 nfcvd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_wv
56 nfcvf2 ⊢¬∀yy=w→Ⅎ_wy
57 56 3ad2ant3 ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎ_wy
58 55 57 nfeqd ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→Ⅎwv=y
59 26 58 nfan1 ⊢Ⅎw¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y
60 51 eleq1d ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→v∈w↔y∈w
61 60 anbi1d ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→v∈w∧w∈x↔y∈w∧w∈x
62 53 61 anbi12d ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→v∈z∧z∈w∧v∈w∧w∈x↔y∈z∧z∈w∧y∈w∧w∈x
63 59 62 exbid ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→∃wv∈z∧z∈w∧v∈w∧w∈x↔∃wy∈z∧z∈w∧y∈w∧w∈x
64 51 eqeq1d ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→v=w↔y=w
65 63 64 bibi12d ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
66 65 ex ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→v=y→∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
67 9 36 66 cbvald ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
68 26 67 exbid ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
69 68 adantr ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
70 54 69 imbi12d ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→∀xv∈z∧z∈w→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
71 45 70 albid ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w∧v=y→∀z∀xv∈z∧z∈w→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
72 71 ex ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→v=y→∀z∀xv∈z∧z∈w→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
73 9 40 72 cbvald ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→∀v∀z∀xv∈z∧z∈w→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
74 5 73 exbid ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→∃x∀v∀z∀xv∈z∧z∈w→∃w∀v∃wv∈z∧z∈w∧v∈w∧w∈x↔v=w↔∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
75 1 74 mpbii ⊢¬∀yy=z∧¬∀yy=x∧¬∀yy=w→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
76 75 3exp ⊢¬∀yy=z→¬∀yy=x→¬∀yy=w→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
77 axacndlem3 ⊢∀yy=z→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
78 axacndlem1 ⊢∀xx=y→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
79 78 aecoms ⊢∀yy=x→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
80 nfae ⊢Ⅎz∀yy=w
81 en2lp ⊢¬y∈z∧z∈y
82 elequ2 ⊢y=w→z∈y↔z∈w
83 82 anbi2d ⊢y=w→y∈z∧z∈y↔y∈z∧z∈w
84 81 83 mtbii ⊢y=w→¬y∈z∧z∈w
85 84 sps ⊢∀yy=w→¬y∈z∧z∈w
86 85 pm2.21d ⊢∀yy=w→y∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
87 86 spsd ⊢∀yy=w→∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
88 80 87 alrimi ⊢∀yy=w→∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
89 88 axc4i ⊢∀yy=w→∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
90 89 19.8ad ⊢∀yy=w→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w
91 76 77 79 90 pm2.61iii ⊢∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w