HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
GIF version
Theorem axacndlem4 4942
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:   y,z,w
Proof of Theorem axacndlem4
StepHypRef Expression
1 axac 4725 . . . . 5 ⊢ ∃v∀y∀z((y ∈ z ⋀ z ∈ w) → ∃w∀y(∃w((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ v)) ↔ y = w))
2 ax-4 971 . . . . . . . 8 ⊢ (∀v(y ∈ z ⋀ z ∈ w) → (y ∈ z ⋀ z ∈ w))
32imim1i 16 . . . . . . 7 ⊢ (((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.20i2 991 . . . . . 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)))
5419.22i 1038 . . . . 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)))
61, 5ax-mp 7 . . . 4 ⊢ ∃v∀y∀z(∀v(y ∈ z ⋀ z ∈ w) → ∃w∀y(∃w((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ v)) ↔ y = w))
7 hbnae 1145 . . . . . 6 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
8 hbnae 1145 . . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
9 hbnae 1145 . . . . . . 7 ⊢ (¬ ∀x x = w → ∀x ¬ ∀x x = w)
108, 9hban 1007 . . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = w) → ∀x(¬ ∀x x = y ⋀ ¬ ∀x x = w))
117, 10hban 1007 . . . . 5 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → ∀x(¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)))
12 hbnae 1145 . . . . . . 7 ⊢ (¬ ∀x x = z → ∀y ¬ ∀x x = z)
13 hbnae 1145 . . . . . . . 8 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
14 hbnae 1145 . . . . . . . 8 ⊢ (¬ ∀x x = w → ∀y ¬ ∀x x = w)
1513, 14hban 1007 . . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = w) → ∀y(¬ ∀x x = y ⋀ ¬ ∀x x = w))
1612, 15hban 1007 . . . . . 6 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → ∀y(¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)))
17 hbnae 1145 . . . . . . . 8 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
18 hbnae 1145 . . . . . . . . 9 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
19 hbnae 1145 . . . . . . . . 9 ⊢ (¬ ∀x x = w → ∀z ¬ ∀x x = w)
2018, 19hban 1007 . . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = w) → ∀z(¬ ∀x x = y ⋀ ¬ ∀x x = w))
2117, 20hban 1007 . . . . . . 7 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → ∀z(¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)))
22 ax-17 969 . . . . . . . . 9 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → ∀v(¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)))
23 ax-15 1358 . . . . . . . . . . . 12 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (y ∈ z → ∀x y ∈ z)))
2423impcom 351 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (y ∈ z → ∀x y ∈ z))
2524adantrr 395 . . . . . . . . . 10 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → (y ∈ z → ∀x y ∈ z))
26 ax-15 1358 . . . . . . . . . . . 12 ⊢ (¬ ∀x x = z → (¬ ∀x x = w → (z ∈ w → ∀x z ∈ w)))
2726imp 350 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (z ∈ w → ∀x z ∈ w))
2827adantrl 394 . . . . . . . . . 10 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → (z ∈ w → ∀x z ∈ w))
2925, 28hband 1109 . . . . . . . . 9 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → ((y ∈ z ⋀ z ∈ w) → ∀x(y ∈ z ⋀ z ∈ w)))
3022, 29hbald 1111 . . . . . . . 8 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → (∀v(y ∈ z ⋀ z ∈ w) → ∀x∀v(y ∈ z ⋀ z ∈ w)))
31 hbnae 1145 . . . . . . . . . 10 ⊢ (¬ ∀x x = z → ∀w ¬ ∀x x = z)
32 hbnae 1145 . . . . . . . . . . 11 ⊢ (¬ ∀x x = y → ∀w ¬ ∀x x = y)
33 hbnae 1145 . . . . . . . . . . 11 ⊢ (¬ ∀x x = w → ∀w ¬ ∀x x = w)
3432, 33hban 1007 . . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = w) → ∀w(¬ ∀x x = y ⋀ ¬ ∀x x = w))
3531, 34hban 1007 . . . . . . . . 9 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → ∀w(¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)))
36 ax-15 1358 . . . . . . . . . . . . . . . 16 ⊢ (¬ ∀x x = y → (¬ ∀x x = w → (y ∈ w → ∀x y ∈ w)))
3736imp 350 . . . . . . . . . . . . . . 15 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = w) → (y ∈ w → ∀x y ∈ w))
38 dveel1 1354 . . . . . . . . . . . . . . . 16 ⊢ (¬ ∀x x = w → (w ∈ v → ∀x w ∈ v))
3938adantl 388 . . . . . . . . . . . . . . 15 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = w) → (w ∈ v → ∀x w ∈ v))
4037, 39hband 1109 . . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = w) → ((y ∈ w ⋀ w ∈ v) → ∀x(y ∈ w ⋀ w ∈ v)))
4140adantl 388 . . . . . . . . . . . . 13 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → ((y ∈ w ⋀ w ∈ v) → ∀x(y ∈ w ⋀ w ∈ v)))
4229, 41hband 1109 . . . . . . . . . . . 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))))
4335, 42hbexd 1112 . . . . . . . . . . 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))))
44 ax-12 966 . . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (¬ ∀x x = w → (y = w → ∀x y = w)))
4544imp 350 . . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = w) → (y = w → ∀x y = w))
4645adantl 388 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → (y = w → ∀x y = w))
4711, 43, 46hbbid 1110 . . . . . . . . . 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)))
4816, 47hbald 1111 . . . . . . . . 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)))
4935, 48hbexd 1112 . . . . . . . 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)))
5011, 30, 49hbimd 1108 . . . . . . 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))))
5121, 50hbald 1111 . . . . . 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))))
5216, 51hbald 1111 . . . . 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))))
53 nd5 4922 . . . . . . . 8 ⊢ (¬ ∀x x = z → (v = x → ∀z v = x))
54 nd5 4922 . . . . . . . . 9 ⊢ (¬ ∀x x = y → (v = x → ∀y v = x))
5518, 54hbald 1111 . . . . . . . 8 ⊢ (¬ ∀x x = y → (∀z v = x → ∀y∀z v = x))
5653, 55sylan9 468 . . . . . . 7 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (v = x → ∀y∀z v = x))
5756adantrr 395 . . . . . 6 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → (v = x → ∀y∀z v = x))
58 hba1 1001 . . . . . . . . 9 ⊢ (∀y∀z v = x → ∀y∀y∀z v = x)
5916, 58hban 1007 . . . . . . . 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))
60 hba2 1011 . . . . . . . . . 10 ⊢ (∀y∀z v = x → ∀z∀y∀z v = x)
6121, 60hban 1007 . . . . . . . . 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))
62 pm4.2i 171 . . . . . . . . . . . . 13 ⊢ (v = x → ((y ∈ z ⋀ z ∈ w) ↔ (y ∈ z ⋀ z ∈ w)))
6362a1i 8 . . . . . . . . . . . 12 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → (v = x → ((y ∈ z ⋀ z ∈ w) ↔ (y ∈ z ⋀ z ∈ w))))
6411, 29, 63cbvald 1318 . . . . . . . . . . 11 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) → (∀v(y ∈ z ⋀ z ∈ w) ↔ ∀x(y ∈ z ⋀ z ∈ w)))
6564adantr 389 . . . . . . . . . 10 ⊢ (((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ ¬ ∀x x = w)) ⋀ ∀y∀z v = x) → (∀v(y ∈ z ⋀ z ∈ w) ↔ ∀x(y ∈ z ⋀ z ∈ w)))
66 nd5 4922 . . . . . . . . . . . . . . . 16 ⊢ (¬ ∀x x = w → (v = x → ∀w v = x))
6714, 6619.20d 994 . . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = w → (∀y v = x → ∀y∀w v = x))
68 ax-4 971 . . . . . . . . . . . . . . . 16 ⊢ (∀z v = x → v = x)
696819.20i 990 . . . . . . . . . . . . . . 15 ⊢ (∀y∀z v = x → ∀y v = x)
7067, 69syl5 21 . . . . . . . . . . . . . 14 ⊢ (¬ ∀x x = w → (∀y∀z v = x → ∀y∀w v = x))
7170adantl 388 . . . . . . . . . . . . 13 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = w) → (∀y∀z v = x → ∀y∀w v = x))
7271imdistani 443 . . . . . . . . . . . 12 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = w) ⋀ ∀y∀z v = x) → ((¬ ∀x x = y ⋀ ¬ ∀x x = w) ⋀ ∀y∀w v = x))
73 hba2 1011 . . . . . . . . . . . . . 14 ⊢ (∀y∀w v = x → ∀w∀y∀w v = x)
74 hba1 1001 . . . . . . . . . . . . . . 15 ⊢ (∀y∀w v = x → ∀y∀y∀w v = x)
75 hba1 1001 . . . . . . . . . . . . . . . . . 18 ⊢ (∀w v = x → ∀w∀w v = x)
76 elequ2 1135 . . . . . . . . . . . . . . . . . . . . 21 ⊢ (v = x → (w ∈ v ↔ w ∈ x))
7776anbi2d 615 . . . . . . . . . . . . . . . . . . . 20 ⊢ (v = x → ((y ∈ w ⋀ w ∈ v) ↔ (y ∈ w ⋀ w ∈ x)))
7877anbi2d 615 . . . . . . . . . . . . . . . . . . 19 ⊢ (v = x → (((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ v)) ↔ ((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ x))))
7978a4s 982 . . . . . . . . . . . . . . . . . 18 ⊢ (∀w v = x → (((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ v)) ↔ ((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ x))))
8075, 79exbid 1103 . . . . . . . . . . . . . . . . 17 ⊢ (∀w v = x → (∃w((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ v)) ↔ ∃w((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ x))))
8180bibi1d 618 . . . . . . . . . . . . . . . 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)))
8281a4s 982 . . . . . . . . . . . . . . 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)))
8374, 82albid 1102 . . . . . . . . . . . . . 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)))
8473, 83exbid 1103 . . . . . . . . . . . . 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)))
8584adantl 388 . . . . . . . . . . . 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)))
8672, 85syl 10 . . . . . . . . . . 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)))
8786adantll 392 . . . . . . . . . 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)))
8865, 87imbi12d 625 . . . . . . . . 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))))
8961, 88albid 1102 . . . . . . . 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))))
9059, 89albid 1102 . . . . . . 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))))
9190ex 373 . . . . . 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)))))
9257, 91syld 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)))))
9311, 52, 92cbvexd 1319 . . . 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))))
946, 93mpbii 193 . . 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)))
9594exp32 377 . 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)))))
96 axacndlem2 4940 . 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)))
97 axacndlem1 4939 . 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)))
98 hbae 1143 . . . 4 ⊢ (∀x x = w → ∀y∀x x = w)
99 hbae 1143 . . . . 5 ⊢ (∀x x = w → ∀z∀x x = w)
100 nd2 4919 . . . . . . 7 ⊢ (∀x x = w → ¬ ∀x z ∈ w)
101100pm2.21d 78 . . . . . 6 ⊢ (∀x x = w → (∀x z ∈ w → ∃w∀y(∃w((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ x)) ↔ y = w)))
102 pm3.27 323 . . . . . . 7 ⊢ ((y ∈ z ⋀ z ∈ w) → z ∈ w)
10310219.20i 990 . . . . . 6 ⊢ (∀x(y ∈ z ⋀ z ∈ w) → ∀x z ∈ w)
104101, 103syl5 21 . . . . 5 ⊢ (∀x x = w → (∀x(y ∈ z ⋀ z ∈ w) → ∃w∀y(∃w((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ x)) ↔ y = w)))
10599, 10419.21ai 996 . . . 4 ⊢ (∀x x = w → ∀z(∀x(y ∈ z ⋀ z ∈ w) → ∃w∀y(∃w((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ x)) ↔ y = w)))
10698, 10519.21ai 996 . . 3 ⊢ (∀x x = w → ∀y∀z(∀x(y ∈ z ⋀ z ∈ w) → ∃w∀y(∃w((y ∈ z ⋀ z ∈ w) ⋀ (y ∈ w ⋀ w ∈ x)) ↔ y = w)))
107 19.8a 1027 . . 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)))
108106, 107syl 10 . 2 ⊢ (∀x x = w → ∃x∀y∀z(∀x(y ∈ z ⋀ z ∈ w) → ∃w∀y(∃w((y ∈ z ⋀ z</