Theorem kmlem14 3593

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4.

Hypotheses

Ref	Expression
kmlem14.1	⊢ (φ ↔ (z ∈ y → ((v ∈ x ∧ ¬ y = v) ∧ z ∈ v)))
kmlem14.2	⊢ (ψ ↔ (z ∈ x → ((v ∈ z ∧ v ∈ y) ∧ ((u ∈ z ∧ u ∈ y) → u = v))))
kmlem14.3	⊢ (χ ↔ ∀z ∈ x ∃!v v ∈ (z ∩ y))

Assertion

Ref	Expression
kmlem14	⊢ (∃z ∈ x ∀v ∈ z ∃w ∈ x (¬ z = w ∧ v ∈ (z ∩ w)) ↔ ∃y∀z∃v∀u(y ∈ x ∧ φ))

Distinct variable group(s):   x,y,z,w,v,u   φ,u

Proof of Theorem kmlem14

Step	Hyp	Ref	Expression
1		cleq1 1107	. . . . . . 7 ⊢ (z = y → (z = w ↔ y = w))
2	1	negbid 463	. . . . . 6 ⊢ (z = y → (¬ z = w ↔ ¬ y = w))
3		ineq1 1638	. . . . . . 7 ⊢ (z = y → (z ∩ w) = (y ∩ w))
4	3	eleq2d 1156	. . . . . 6 ⊢ (z = y → (v ∈ (z ∩ w) ↔ v ∈ (y ∩ w)))
5	2, 4	anbi12d 476	. . . . 5 ⊢ (z = y → ((¬ z = w ∧ v ∈ (z ∩ w)) ↔ (¬ y = w ∧ v ∈ (y ∩ w))))
6	5	birexdv 1220	. . . 4 ⊢ (z = y → (∃w ∈ x (¬ z = w ∧ v ∈ (z ∩ w)) ↔ ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w))))
7	6	raleqd 1327	. . 3 ⊢ (z = y → (∀v ∈ z ∃w ∈ x (¬ z = w ∧ v ∈ (z ∩ w)) ↔ ∀v ∈ y ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w))))
8	7	cbvrexv 1334	. 2 ⊢ (∃z ∈ x ∀v ∈ z ∃w ∈ x (¬ z = w ∧ v ∈ (z ∩ w)) ↔ ∃y ∈ x ∀v ∈ y ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w)))
9		df-rex 1206	. 2 ⊢ (∃y ∈ x ∀v ∈ y ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w)) ↔ ∃y(y ∈ x ∧ ∀v ∈ y ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w))))
10		eleq1 1149	. . . . . . . . 9 ⊢ (v = z → (v ∈ (y ∩ w) ↔ z ∈ (y ∩ w)))
11	10	anbi2d 468	. . . . . . . 8 ⊢ (v = z → ((¬ y = w ∧ v ∈ (y ∩ w)) ↔ (¬ y = w ∧ z ∈ (y ∩ w))))
12	11	birexdv 1220	. . . . . . 7 ⊢ (v = z → (∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w)) ↔ ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w))))
13	12	cbvralv 1333	. . . . . 6 ⊢ (∀v ∈ y ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w)) ↔ ∀z ∈ y ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)))
14		df-ral 1205	. . . . . 6 ⊢ (∀z ∈ y ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)) ↔ ∀z(z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w))))
15	13, 14	bitr 151	. . . . 5 ⊢ (∀v ∈ y ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w)) ↔ ∀z(z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w))))
16	15	anbi2i 367	. . . 4 ⊢ ((y ∈ x ∧ ∀v ∈ y ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w))) ↔ (y ∈ x ∧ ∀z(z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)))))
17		19.28v 957	. . . . 5 ⊢ (∀z(y ∈ x ∧ (z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)))) ↔ (y ∈ x ∧ ∀z(z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)))))
18		cleq2 1110	. . . . . . . . . . . . . 14 ⊢ (w = v → (y = w ↔ y = v))
19	18	negbid 463	. . . . . . . . . . . . 13 ⊢ (w = v → (¬ y = w ↔ ¬ y = v))
20		ineq2 1639	. . . . . . . . . . . . . 14 ⊢ (w = v → (y ∩ w) = (y ∩ v))
21	20	eleq2d 1156	. . . . . . . . . . . . 13 ⊢ (w = v → (z ∈ (y ∩ w) ↔ z ∈ (y ∩ v)))
22	19, 21	anbi12d 476	. . . . . . . . . . . 12 ⊢ (w = v → ((¬ y = w ∧ z ∈ (y ∩ w)) ↔ (¬ y = v ∧ z ∈ (y ∩ v))))
23	22	cbvrexv 1334	. . . . . . . . . . 11 ⊢ (∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)) ↔ ∃v ∈ x (¬ y = v ∧ z ∈ (y ∩ v)))
24		df-rex 1206	. . . . . . . . . . 11 ⊢ (∃v ∈ x (¬ y = v ∧ z ∈ (y ∩ v)) ↔ ∃v(v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))
25	23, 24	bitr 151	. . . . . . . . . 10 ⊢ (∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)) ↔ ∃v(v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))
26	25	imbi2i 160	. . . . . . . . 9 ⊢ ((z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w))) ↔ (z ∈ y → ∃v(v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v)))))
27		19.37v 961	. . . . . . . . 9 ⊢ (∃v(z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v)))) ↔ (z ∈ y → ∃v(v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v)))))
28	26, 27	bitr4 154	. . . . . . . 8 ⊢ ((z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w))) ↔ ∃v(z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v)))))
29	28	anbi2i 367	. . . . . . 7 ⊢ ((y ∈ x ∧ (z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)))) ↔ (y ∈ x ∧ ∃v(z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))))
30		19.42v 966	. . . . . . . 8 ⊢ (∃v(y ∈ x ∧ (z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))) ↔ (y ∈ x ∧ ∃v(z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))))
31		kmlem14.1	. . . . . . . . . . . 12 ⊢ (φ ↔ (z ∈ y → ((v ∈ x ∧ ¬ y = v) ∧ z ∈ v)))
32		elin 1635	. . . . . . . . . . . . . . . 16 ⊢ (z ∈ (y ∩ v) ↔ (z ∈ y ∧ z ∈ v))
33	32	baibr 507	. . . . . . . . . . . . . . 15 ⊢ (z ∈ y → (z ∈ v ↔ z ∈ (y ∩ v)))
34	33	anbi2d 468	. . . . . . . . . . . . . 14 ⊢ (z ∈ y → (((v ∈ x ∧ ¬ y = v) ∧ z ∈ v) ↔ ((v ∈ x ∧ ¬ y = v) ∧ z ∈ (y ∩ v))))
35		anass 336	. . . . . . . . . . . . . 14 ⊢ (((v ∈ x ∧ ¬ y = v) ∧ z ∈ (y ∩ v)) ↔ (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))
36	34, 35	syl6bb 414	. . . . . . . . . . . . 13 ⊢ (z ∈ y → (((v ∈ x ∧ ¬ y = v) ∧ z ∈ v) ↔ (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v)))))
37	36	pm5.74i 443	. . . . . . . . . . . 12 ⊢ ((z ∈ y → ((v ∈ x ∧ ¬ y = v) ∧ z ∈ v)) ↔ (z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v)))))
38	31, 37	bitr 151	. . . . . . . . . . 11 ⊢ (φ ↔ (z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v)))))
39	38	anbi2i 367	. . . . . . . . . 10 ⊢ ((y ∈ x ∧ φ) ↔ (y ∈ x ∧ (z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))))
40		ax-17 925	. . . . . . . . . . 11 ⊢ ((y ∈ x ∧ φ) → ∀u(y ∈ x ∧ φ))
41	40	19.3r 714	. . . . . . . . . 10 ⊢ ((y ∈ x ∧ φ) ↔ ∀u(y ∈ x ∧ φ))
42	39, 41	bitr3 153	. . . . . . . . 9 ⊢ ((y ∈ x ∧ (z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))) ↔ ∀u(y ∈ x ∧ φ))
43	42	biex 733	. . . . . . . 8 ⊢ (∃v(y ∈ x ∧ (z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))) ↔ ∃v∀u(y ∈ x ∧ φ))
44	30, 43	bitr3 153	. . . . . . 7 ⊢ ((y ∈ x ∧ ∃v(z ∈ y → (v ∈ x ∧ (¬ y = v ∧ z ∈ (y ∩ v))))) ↔ ∃v∀u(y ∈ x ∧ φ))
45	29, 44	bitr 151	. . . . . 6 ⊢ ((y ∈ x ∧ (z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)))) ↔ ∃v∀u(y ∈ x ∧ φ))
46	45	bial 695	. . . . 5 ⊢ (∀z(y ∈ x ∧ (z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)))) ↔ ∀z∃v∀u(y ∈ x ∧ φ))
47	17, 46	bitr3 153	. . . 4 ⊢ ((y ∈ x ∧ ∀z(z ∈ y → ∃w ∈ x (¬ y = w ∧ z ∈ (y ∩ w)))) ↔ ∀z∃v∀u(y ∈ x ∧ φ))
48	16, 47	bitr 151	. . 3 ⊢ ((y ∈ x ∧ ∀v ∈ y ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w))) ↔ ∀z∃v∀u(y ∈ x ∧ φ))
49	48	biex 733	. 2 ⊢ (∃y(y ∈ x ∧ ∀v ∈ y ∃w ∈ x (¬ y = w ∧ v ∈ (y ∩ w))) ↔ ∃y∀z∃v∀u(y ∈ x ∧ φ))
50	8, 9, 49	3bitr 155	1 ⊢ (∃z ∈ x ∀v ∈ z ∃w ∈ x (¬ z = w ∧ v ∈ (z ∩ w)) ↔ ∃y∀z∃v∀u(y ∈ x ∧ φ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803  ∃!weu 1007   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202   ∩ cin 1486

This theorem is referenced by:  kmlem16 3595

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-16 922  ax-17 925  ax-ext 1074

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-in 1491

metamath.org