HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
GIF version
Theorem axacndlem4 3756
Description: Lemma for the Axiom of Choice with no distinct variable conditions.
Assertion
Ref Expression
axacndlem4 ⊢ ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))
Distinct variable group(s):   y,z,w
Proof of Theorem axacndlem4
StepHypRef Expression
1 axac 1085 . . . . 5 ⊢ ∃v∀y∀z((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w))
2 ax-4 673 . . . . . . . . 9 ⊢ (∀v(y ∈ z ∧ z ∈ w) → (y ∈ z ∧ z ∈ w))
32syl4 19 . . . . . . . 8 ⊢ (((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)) → (∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)))
4319.20i 691 . . . . . . 7 ⊢ (∀z((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)) → ∀z(∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)))
5419.20i 691 . . . . . 6 ⊢ (∀y∀z((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)) → ∀y∀z(∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)))
6519.22i 723 . . . . 5 ⊢ (∃v∀y∀z((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)) → ∃v∀y∀z(∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)))
71, 6ax-mp 6 . . . 4 ⊢ ∃v∀y∀z(∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w))
8 eq6 826 . . . . . 6 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
9 eq6 826 . . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
10 eq6 826 . . . . . . 7 ⊢ (¬ ∀x x = w → ∀x ¬ ∀x x = w)
119, 10hban 704 . . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = w) → ∀x(¬ ∀x x = y ∧ ¬ ∀x x = w))
128, 11hban 704 . . . . 5 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → ∀x(¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)))
13 eq6 826 . . . . . . 7 ⊢ (¬ ∀x x = z → ∀y ¬ ∀x x = z)
14 eq6 826 . . . . . . . 8 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
15 eq6 826 . . . . . . . 8 ⊢ (¬ ∀x x = w → ∀y ¬ ∀x x = w)
1614, 15hban 704 . . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = w) → ∀y(¬ ∀x x = y ∧ ¬ ∀x x = w))
1713, 16hban 704 . . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → ∀y(¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)))
18 eq6 826 . . . . . . . 8 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
19 eq6 826 . . . . . . . . 9 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
20 eq6 826 . . . . . . . . 9 ⊢ (¬ ∀x x = w → ∀z ¬ ∀x x = w)
2119, 20hban 704 . . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = w) → ∀z(¬ ∀x x = y ∧ ¬ ∀x x = w))
2218, 21hban 704 . . . . . . 7 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → ∀z(¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)))
23 ax-17 925 . . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → ∀v(¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)))
24 ax15 1006 . . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (y ∈ z → ∀x y ∈ z)))
2524com12 13 . . . . . . . . . . . 12 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (y ∈ z → ∀x y ∈ z)))
2625imp 277 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (y ∈ z → ∀x y ∈ z))
2726adantrr 312 . . . . . . . . . 10 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (y ∈ z → ∀x y ∈ z))
28 ax15 1006 . . . . . . . . . . . 12 ⊢ (¬ ∀x x = z → (¬ ∀x x = w → (z ∈ w → ∀x z ∈ w)))
2928imp 277 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = w) → (z ∈ w → ∀x z ∈ w))
3029adantrl 311 . . . . . . . . . 10 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (z ∈ w → ∀x z ∈ w))
3127, 30hband 788 . . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → ((y ∈ z ∧ z ∈ w) → ∀x(y ∈ z ∧ z ∈ w)))
3223, 31hbald 790 . . . . . . . 8 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (∀v(y ∈ z ∧ z ∈ w) → ∀x∀v(y ∈ z ∧ z ∈ w)))
33 eq6 826 . . . . . . . . . 10 ⊢ (¬ ∀x x = z → ∀w ¬ ∀x x = z)
34 eq6 826 . . . . . . . . . . 11 ⊢ (¬ ∀x x = y → ∀w ¬ ∀x x = y)
35 eq6 826 . . . . . . . . . . 11 ⊢ (¬ ∀x x = w → ∀w ¬ ∀x x = w)
3634, 35hban 704 . . . . . . . . . 10 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = w) → ∀w(¬ ∀x x = y ∧ ¬ ∀x x = w))
3733, 36hban 704 . . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → ∀w(¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)))
38 ax15 1006 . . . . . . . . . . . . . . . 16 ⊢ (¬ ∀x x = y → (¬ ∀x x = w → (y ∈ w → ∀x y ∈ w)))
3938imp 277 . . . . . . . . . . . . . . 15 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = w) → (y ∈ w → ∀x y ∈ w))
40 ddeel1 1003 . . . . . . . . . . . . . . . 16 ⊢ (¬ ∀x x = w → (w ∈ v → ∀x w ∈ v))
4140adantl 305 . . . . . . . . . . . . . . 15 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = w) → (w ∈ v → ∀x w ∈ v))
4239, 41hband 788 . . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = w) → ((y ∈ w ∧ w ∈ v) → ∀x(y ∈ w ∧ w ∈ v)))
4342adantl 305 . . . . . . . . . . . . 13 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → ((y ∈ w ∧ w ∈ v) → ∀x(y ∈ w ∧ w ∈ v)))
4431, 43hband 788 . . . . . . . . . . . 12 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) → ∀x((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v))))
4537, 44hbexd 791 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) → ∀x∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v))))
46 ax-12 802 . . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (¬ ∀x x = w → (y = w → ∀x y = w)))
4746imp 277 . . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = w) → (y = w → ∀x y = w))
4847adantl 305 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (y = w → ∀x y = w))
4912, 45, 48hbbid 789 . . . . . . . . . 10 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → ((∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w) → ∀x(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)))
5017, 49hbald 790 . . . . . . . . 9 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w) → ∀x∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)))
5137, 50hbexd 791 . . . . . . . 8 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w) → ∀x∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)))
5212, 32, 51hbimd 787 . . . . . . 7 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → ((∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)) → ∀x(∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w))))
5322, 52hbald 790 . . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (∀z(∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)) → ∀x∀z(∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w))))
5417, 53hbald 790 . . . . 5 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (∀y∀z(∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w)) → ∀x∀y∀z(∀v(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ y = w))))
55 nd5 3736 . . . . . . . 8 ⊢ (¬ ∀x x = z → (v = x → ∀z v = x))
56 nd5 3736 . . . . . . . . 9 ⊢ (¬ ∀x x = y → (v = x → ∀y v = x))
5719, 56hbald 790 . . . . . . . 8 ⊢ (¬ ∀x x = y → (∀z v = x → ∀y∀z v = x))
5855, 57sylan9 359 . . . . . . 7 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (v = x → ∀y∀z v = x))
5958adantrr 312 . . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (v = x → ∀y∀z v = x))
60 hba1 698 . . . . . . . . 9 ⊢ (∀y∀z v = x → ∀y∀y∀z v = x)
6117, 60hban 704 . . . . . . . 8 ⊢ (((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) ∧ ∀y∀z v = x) → ∀y((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) ∧ ∀y∀z v = x))
62 hba1 698 . . . . . . . . . . 11 ⊢ (∀z v = x → ∀z∀z v = x)
6362hbal 700 . . . . . . . . . 10 ⊢ (∀y∀z v = x → ∀z∀y∀z v = x)
6422, 63hban 704 . . . . . . . . 9 ⊢ (((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) ∧ ∀y∀z v = x) → ∀z((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) ∧ ∀y∀z v = x))
65 pm4.2i 149 . . . . . . . . . . . . 13 ⊢ (v = x → ((y ∈ z ∧ z ∈ w) ↔ (y ∈ z ∧ z ∈ w)))
6665a1i 7 . . . . . . . . . . . 12 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (v = x → ((y ∈ z ∧ z ∈ w) ↔ (y ∈ z ∧ z ∈ w))))
6712, 31, 66cbvald 977 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (∀v(y ∈ z ∧ z ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
6867adantr 306 . . . . . . . . . 10 ⊢ (((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) ∧ ∀y∀z v = x) → (∀v(y ∈ z ∧ z ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
69 nd5 3736 . . . . . . . . . . . . . . . 16 ⊢ (¬ ∀x x = w → (v = x → ∀w v = x))
7015, 6919.20d 693 . . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = w → (∀y v = x → ∀y∀w v = x))
71 ax-4 673 . . . . . . . . . . . . . . . 16 ⊢ (∀z v = x → v = x)
727119.20i 691 . . . . . . . . . . . . . . 15 ⊢ (∀y∀z v = x → ∀y v = x)
7370, 72syl5 22 . . . . . . . . . . . . . 14 ⊢ (¬ ∀x x = w → (∀y∀z v = x → ∀y∀w v = x))
7473adantl 305 . . . . . . . . . . . . 13 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = w) → (∀y∀z v = x → ∀y∀w v = x))
7574imdistani 340 . . . . . . . . . . . 12 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = w) ∧ ∀y∀z v = x) → ((¬ ∀x x = y ∧ ¬ ∀x x = w) ∧ ∀y∀w v = x))
76 hba1 698 . . . . . . . . . . . . . . 15 ⊢ (∀w v = x → ∀w∀w v = x)
7776hbal 700 . . . . . . . . . . . . . 14 ⊢ (∀y∀w v = x → ∀w∀y∀w v = x)
78 hba1 698 . . . . . . . . . . . . . . 15 ⊢ (∀y∀w v = x → ∀y∀y∀w v = x)
79 a14b 820 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (v = x → (w ∈ v ↔ w ∈ x))
8079anbi2d 468 . . . . . . . . . . . . . . . . . . . 20 ⊢ (v = x → ((y ∈ w ∧ w ∈ v) ↔ (y ∈ w ∧ w ∈ x)))
8180anbi2d 468 . . . . . . . . . . . . . . . . . . 19 ⊢ (v = x → (((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ ((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
8281a4s 682 . . . . . . . . . . . . . . . . . 18 ⊢ (∀w v = x → (((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ ((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
8376, 82biexd 783 . . . . . . . . . . . . . . . . 17 ⊢ (∀w v = x → (∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ v)) ↔ ∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
8483bibi1d 471 . . . . . . . . . . . . . . . 16 ⊢ (∀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)))
8584a4s 682 . . . . . . . . . . . . . . 15 ⊢ (∀y∀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)))
8678, 85biald 782 . . . . . . . . . . . . . 14 ⊢ (∀y∀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)))
8777, 86biexd 783 . . . . . . . . . . . . 13 ⊢ (∀y∀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)))
8887adantl 305 . . . . . . . . . . . 12 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = w) ∧ ∀y∀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)))
8975, 88syl 12 . . . . . . . . . . 11 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = w) ∧ ∀y∀z 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)))
9089adantll 309 . . . . . . . . . 10 ⊢ (((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) ∧ ∀y∀z 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)))
9168, 90imbi12d 474 . . . . . . . . 9 ⊢ (((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) ∧ ∀y∀z v = x) → ((∀v(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))))
9264, 91biald 782 . . . . . . . 8 ⊢ (((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) ∧ ∀y∀z v = x) → (∀z(∀v(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))))
9361, 92biald 782 . . . . . . 7 ⊢ (((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) ∧ ∀y∀z v = x) → (∀y∀z(∀v(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))))
9493exp 291 . . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (∀y∀z v = x → (∀y∀z(∀v(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)))))
9559, 94syld 27 . . . . 5 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (v = x → (∀y∀z(∀v(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)))))
9612, 54, 95cbvexd 978 . . . 4 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ ¬ ∀x x = w)) → (∃v∀y∀z(∀v(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))))
977, 96mpbii 168 . . 3 ⊢ ((¬ ∀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)))
9897exp32 294 . 2 ⊢ (¬ ∀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)))))
99 axacndlem2 3754 . 2 ⊢ (∀x x = z → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
100 axacndlem1 3753 . 2 ⊢ (∀x x = y → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
101 eq5 824 . . . 4 ⊢ (∀x x = w → ∀y∀x x = w)
102 eq5 824 . . . . 5 ⊢ (∀x x = w → ∀z∀x x = w)
103 nd2 3733 . . . . . . 7 ⊢ (∀x x = w → ¬ ∀x z ∈ w)
104103pm2.21d 74 . . . . . 6 ⊢ (∀x x = w → (∀x z ∈ w → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
105 pm3.27 260 . . . . . . 7 ⊢ ((y ∈ z ∧ z ∈ w) → z ∈ w)
10610519.20i 691 . . . . . 6 ⊢ (∀x(y ∈ z ∧ z ∈ w) → ∀x z ∈ w)
107104, 106syl5 22 . . . . 5 ⊢ (∀x x = w → (∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
108102, 10719.21ai 740 . . . 4 ⊢ (∀x x = w → ∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
109101, 10819.21ai 740 . . 3 ⊢ (∀x x = w → ∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
110 19.8a 712 . . 3 ⊢ (∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ 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)))
111109, 110syl 12 . 2 ⊢ (∀x x = w → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
11298, 99, 100, 111pm2.61iii 114 1 ⊢ ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))
Colors of variables: wff set class
Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803
This theorem is referenced by:  axacndlem5 3757
This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077  ax-reg 1078  ax-ac 1080
This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489