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 ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w

Proof

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