Theorem axacndlem5 3757

Description: Lemma for the Axiom of Choice with no distinct variable conditions.

Assertion

Ref	Expression
axacndlem5	⊢ ∃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):   z,w

Proof of Theorem axacndlem5

Step	Hyp	Ref	Expression
1		axacndlem4 3756	. . . 4 ⊢ ∃x∀v∀z(∀x(v ∈ z ∧ z ∈ w) → ∃w∀v(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w))
2		eq6 826	. . . . . 6 ⊢ (¬ ∀y y = z → ∀x ¬ ∀y y = z)
3		eq6 826	. . . . . . 7 ⊢ (¬ ∀y y = x → ∀x ¬ ∀y y = x)
4		eq6 826	. . . . . . 7 ⊢ (¬ ∀y y = w → ∀x ¬ ∀y y = w)
5	3, 4	hban 704	. . . . . 6 ⊢ ((¬ ∀y y = x ∧ ¬ ∀y y = w) → ∀x(¬ ∀y y = x ∧ ¬ ∀y y = w))
6	2, 5	hban 704	. . . . 5 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → ∀x(¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)))
7		eq6 826	. . . . . . 7 ⊢ (¬ ∀y y = z → ∀y ¬ ∀y y = z)
8		eq6 826	. . . . . . . 8 ⊢ (¬ ∀y y = x → ∀y ¬ ∀y y = x)
9		eq6 826	. . . . . . . 8 ⊢ (¬ ∀y y = w → ∀y ¬ ∀y y = w)
10	8, 9	hban 704	. . . . . . 7 ⊢ ((¬ ∀y y = x ∧ ¬ ∀y y = w) → ∀y(¬ ∀y y = x ∧ ¬ ∀y y = w))
11	7, 10	hban 704	. . . . . 6 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → ∀y(¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)))
12		eq6 826	. . . . . . . 8 ⊢ (¬ ∀y y = z → ∀z ¬ ∀y y = z)
13		eq6 826	. . . . . . . . 9 ⊢ (¬ ∀y y = x → ∀z ¬ ∀y y = x)
14		eq6 826	. . . . . . . . 9 ⊢ (¬ ∀y y = w → ∀z ¬ ∀y y = w)
15	13, 14	hban 704	. . . . . . . 8 ⊢ ((¬ ∀y y = x ∧ ¬ ∀y y = w) → ∀z(¬ ∀y y = x ∧ ¬ ∀y y = w))
16	12, 15	hban 704	. . . . . . 7 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → ∀z(¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)))
17		ddeel2 1004	. . . . . . . . . . 11 ⊢ (¬ ∀y y = z → (v ∈ z → ∀y v ∈ z))
18	17	adantr 306	. . . . . . . . . 10 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (v ∈ z → ∀y v ∈ z))
19		ax15 1006	. . . . . . . . . . . 12 ⊢ (¬ ∀y y = z → (¬ ∀y y = w → (z ∈ w → ∀y z ∈ w)))
20	19	imp 277	. . . . . . . . . . 11 ⊢ ((¬ ∀y y = z ∧ ¬ ∀y y = w) → (z ∈ w → ∀y z ∈ w))
21	20	adantrl 311	. . . . . . . . . 10 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (z ∈ w → ∀y z ∈ w))
22	18, 21	hband 788	. . . . . . . . 9 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → ((v ∈ z ∧ z ∈ w) → ∀y(v ∈ z ∧ z ∈ w)))
23	6, 22	hbald 790	. . . . . . . 8 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (∀x(v ∈ z ∧ z ∈ w) → ∀y∀x(v ∈ z ∧ z ∈ w)))
24		eq6 826	. . . . . . . . . 10 ⊢ (¬ ∀y y = z → ∀w ¬ ∀y y = z)
25		eq6 826	. . . . . . . . . . 11 ⊢ (¬ ∀y y = x → ∀w ¬ ∀y y = x)
26		eq6 826	. . . . . . . . . . 11 ⊢ (¬ ∀y y = w → ∀w ¬ ∀y y = w)
27	25, 26	hban 704	. . . . . . . . . 10 ⊢ ((¬ ∀y y = x ∧ ¬ ∀y y = w) → ∀w(¬ ∀y y = x ∧ ¬ ∀y y = w))
28	24, 27	hban 704	. . . . . . . . 9 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → ∀w(¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)))
29		ax-17 925	. . . . . . . . . 10 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → ∀v(¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)))
30		ddeel2 1004	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀y y = w → (v ∈ w → ∀y v ∈ w))
31	30	ad2antrr 323	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (v ∈ w → ∀y v ∈ w))
32		ax15 1006	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ∀y y = w → (¬ ∀y y = x → (w ∈ x → ∀y w ∈ x)))
33	32	com12 13	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∀y y = x → (¬ ∀y y = w → (w ∈ x → ∀y w ∈ x)))
34	33	imp 277	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∀y y = x ∧ ¬ ∀y y = w) → (w ∈ x → ∀y w ∈ x))
35	34	adantl 305	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (w ∈ x → ∀y w ∈ x))
36	31, 35	hband 788	. . . . . . . . . . . . 13 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → ((v ∈ w ∧ w ∈ x) → ∀y(v ∈ w ∧ w ∈ x)))
37	22, 36	hband 788	. . . . . . . . . . . 12 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) → ∀y((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x))))
38	28, 37	hbexd 791	. . . . . . . . . . 11 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) → ∀y∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x))))
39		ddeeq2 1002	. . . . . . . . . . . 12 ⊢ (¬ ∀y y = w → (v = w → ∀y v = w))
40	39	ad2antrr 323	. . . . . . . . . . 11 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (v = w → ∀y v = w))
41	11, 38, 40	hbbid 789	. . . . . . . . . 10 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → ((∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w) → ∀y(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w)))
42	29, 41	hbald 790	. . . . . . . . 9 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (∀v(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w) → ∀y∀v(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w)))
43	28, 42	hbexd 791	. . . . . . . 8 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (∃w∀v(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w) → ∀y∃w∀v(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w)))
44	11, 23, 43	hbimd 787	. . . . . . 7 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → ((∀x(v ∈ z ∧ z ∈ w) → ∃w∀v(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w)) → ∀y(∀x(v ∈ z ∧ z ∈ w) → ∃w∀v(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w))))
45	16, 44	hbald 790	. . . . . 6 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (∀z(∀x(v ∈ z ∧ z ∈ w) → ∃w∀v(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w)) → ∀y∀z(∀x(v ∈ z ∧ z ∈ w) → ∃w∀v(∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ v = w))))
46		nd5 3736	. . . . . . . . . 10 ⊢ (¬ ∀y y = z → (v = y → ∀z v = y))
47	46	adantr 306	. . . . . . . . 9 ⊢ ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) → (v = y → ∀z v = y))
48	47	imdistani 340	. . . . . . . 8 ⊢ (((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) ∧ v = y) → ((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) ∧ ∀z v = y))
49		hba1 698	. . . . . . . . . 10 ⊢ (∀z v = y → ∀z∀z v = y)
50	16, 49	hban 704	. . . . . . . . 9 ⊢ (((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) ∧ ∀z v = y) → ∀z((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) ∧ ∀z v = y))
51		nd5 3736	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀y y = x → (v = y → ∀x v = y))
52	51	imdistani 340	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀y y = x ∧ v = y) → (¬ ∀y y = x ∧ ∀x v = y))
53		hba1 698	. . . . . . . . . . . . . . . 16 ⊢ (∀x v = y → ∀x∀x v = y)
54		a13b 819	. . . . . . . . . . . . . . . . . 18 ⊢ (v = y → (v ∈ z ↔ y ∈ z))
55	54	anbi1d 469	. . . . . . . . . . . . . . . . 17 ⊢ (v = y → ((v ∈ z ∧ z ∈ w) ↔ (y ∈ z ∧ z ∈ w)))
56	55	a4s 682	. . . . . . . . . . . . . . . 16 ⊢ (∀x v = y → ((v ∈ z ∧ z ∈ w) ↔ (y ∈ z ∧ z ∈ w)))
57	53, 56	biald 782	. . . . . . . . . . . . . . 15 ⊢ (∀x v = y → (∀x(v ∈ z ∧ z ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
58	57	adantl 305	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀y y = x ∧ ∀x v = y) → (∀x(v ∈ z ∧ z ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
59	52, 58	syl 12	. . . . . . . . . . . . 13 ⊢ ((¬ ∀y y = x ∧ v = y) → (∀x(v ∈ z ∧ z ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
60		ax-4 673	. . . . . . . . . . . . 13 ⊢ (∀z v = y → v = y)
61	59, 60	sylan2 346	. . . . . . . . . . . 12 ⊢ ((¬ ∀y y = x ∧ ∀z v = y) → (∀x(v ∈ z ∧ z ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
62	61	adantlr 310	. . . . . . . . . . 11 ⊢ (((¬ ∀y y = x ∧ ¬ ∀y y = w) ∧ ∀z v = y) → (∀x(v ∈ z ∧ z ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
63	62	adantll 309	. . . . . . . . . 10 ⊢ (((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) ∧ ∀z v = y) → (∀x(v ∈ z ∧ z ∈ w) ↔ ∀x(y ∈ z ∧ z ∈ w)))
64		nd5 3736	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ∀y y = w → (v = y → ∀w v = y))
65	64	imdistani 340	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ ∀y y = w ∧ v = y) → (¬ ∀y y = w ∧ ∀w v = y))
66		hba1 698	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀w v = y → ∀w∀w v = y)
67		a13b 819	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (v = y → (v ∈ w ↔ y ∈ w))
68	67	anbi1d 469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (v = y → ((v ∈ w ∧ w ∈ x) ↔ (y ∈ w ∧ w ∈ x)))
69	55, 68	anbi12d 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (v = y → (((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ ((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
70	69	a4s 682	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀w v = y → (((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ ((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
71	66, 70	biexd 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀w v = y → (∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ ∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
72	71	adantl 305	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ ∀y y = w ∧ ∀w v = y) → (∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ ∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
73	65, 72	syl 12	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ ∀y y = w ∧ v = y) → (∃w((v ∈ z ∧ z ∈ w) ∧ (v ∈ w ∧ w ∈ x)) ↔ ∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x))))
74	73	adantll 309	. . . . . . . . . . . . . . . 16 ⊢ (((¬ ∀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))))
75	74	adantll 309	. . . . . . . . . . . . . . 15 ⊢ (((¬ ∀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))))
76		a8b 817	. . . . . . . . . . . . . . . 16 ⊢ (v = y → (v = w ↔ y = w))
77	76	adantl 305	. . . . . . . . . . . . . . 15 ⊢ (((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) ∧ v = y) → (v = w ↔ y = w))
78	75, 77	bibi12d 477	. . . . . . . . . . . . . 14 ⊢ (((¬ ∀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)))
79	78	exp 291	. . . . . . . . . . . . 13 ⊢ ((¬ ∀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))))
80	11, 41, 79	cbvald 977	. . . . . . . . . . . 12 ⊢ ((¬ ∀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)))
81	28, 80	biexd 783	. . . . . . . . . . 11 ⊢ ((¬ ∀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)))
82	81	adantr 306	. . . . . . . . . 10 ⊢ (((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) ∧ ∀z 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)))
83	63, 82	imbi12d 474	. . . . . . . . 9 ⊢ (((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) ∧ ∀z 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))))
84	50, 83	biald 782	. . . . . . . 8 ⊢ (((¬ ∀y y = z ∧ (¬ ∀y y = x ∧ ¬ ∀y y = w)) ∧ ∀z 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))))
85	48, 84	syl 12	. . . . . . 7 ⊢ (((¬ ∀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))))
86	85	exp 291	. . . . . 6 ⊢ ((¬ ∀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)))))
87	11, 45, 86	cbvald 977	. . . . 5 ⊢ ((¬ ∀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))))
88	6, 87	biexd 783	. . . 4 ⊢ ((¬ ∀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))))
89	1, 88	mpbii 168	. . 3 ⊢ ((¬ ∀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)))
90	89	exp32 294	. 2 ⊢ (¬ ∀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)))))
91		axacndlem3 3755	. 2 ⊢ (∀y y = z → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
92		axacndlem1 3753	. . 3 ⊢ (∀x x = y → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
93	92	eq4s 822	. 2 ⊢ (∀y y = x → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
94		eq5 824	. . . . 5 ⊢ (∀y y = w → ∀z∀y y = w)
95		en2lp 3453	. . . . . . . . 9 ⊢ ¬ (y ∈ z ∧ z ∈ y)
96		a14b 820	. . . . . . . . . 10 ⊢ (y = w → (z ∈ y ↔ z ∈ w))
97	96	anbi2d 468	. . . . . . . . 9 ⊢ (y = w → ((y ∈ z ∧ z ∈ y) ↔ (y ∈ z ∧ z ∈ w)))
98	95, 97	mtbii 538	. . . . . . . 8 ⊢ (y = w → ¬ (y ∈ z ∧ z ∈ w))
99	98	a4s 682	. . . . . . 7 ⊢ (∀y y = w → ¬ (y ∈ z ∧ z ∈ w))
100	99	pm2.21d 74	. . . . . 6 ⊢ (∀y y = w → ((y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
101	100	a4sd 683	. . . . 5 ⊢ (∀y y = w → (∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
102	94, 101	19.21ai 740	. . . 4 ⊢ (∀y y = w → ∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
103	102	a5i 687	. . 3 ⊢ (∀y y = w → ∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
104		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)))
105	103, 104	syl 12	. 2 ⊢ (∀y y = w → ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w)))
106	90, 91, 93, 105	pm2.61iii 114	1 ⊢ ∃x∀y∀z(∀x(y ∈ z ∧ z ∈ w) → ∃w∀y(∃w((y ∈ z ∧ z ∈ w) ∧ (y ∈ w ∧ w ∈ x)) ↔ y = w))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803

This theorem is referenced by:  axacnd 3758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 67‰  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  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063  df-opab 2098  df-eprel 2122  df-fr 2169

metamath.org