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

Proof

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