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

Proof

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