Theorem kmlem14 10205

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4. (Contributed by NM, 4-Apr-2004.)

Hypotheses

Ref	Expression
kmlem14.1	⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))
kmlem14.2	⊢ (𝜓 ↔ (𝑧 ∈ 𝑥 → ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑧 ∧ 𝑢 ∈ 𝑦) → 𝑢 = 𝑣))))
kmlem14.3	⊢ (𝜒 ↔ ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))

Assertion

Ref	Expression
kmlem14	⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢   𝜑,𝑢

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣)   𝜓(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝜒(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)

Proof of Theorem kmlem14

Step	Hyp	Ref	Expression
1		neeq1 3002	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 𝑤 ↔ 𝑦 ≠ 𝑤))
2		ineq1 4212	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 ∩ 𝑤) = (𝑦 ∩ 𝑤))
3	2	eleq2d 2826	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ 𝑣 ∈ (𝑦 ∩ 𝑤)))
4	1, 3	anbi12d 632	. . . . 5 ⊢ (𝑧 = 𝑦 → ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
5	4	rexbidv 3178	. . . 4 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
6	5	raleqbi1dv 3337	. . 3 ⊢ (𝑧 = 𝑦 → (∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
7	6	cbvrexvw 3237	. 2 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)))
8		df-rex 3070	. 2 ⊢ (∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
9		eleq1w 2823	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑤)))
10	9	anbi2d 630	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → ((𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
11	10	rexbidv 3178	. . . . . . 7 ⊢ (𝑣 = 𝑧 → (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
12	11	cbvralvw 3236	. . . . . 6 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))
13		df-ral 3061	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
14	12, 13	bitri 275	. . . . 5 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
15	14	anbi2i 623	. . . 4 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
16		19.28v 1989	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
17		neeq2 3003	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑦 ≠ 𝑤 ↔ 𝑦 ≠ 𝑣))
18		ineq2 4213	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑣 → (𝑦 ∩ 𝑤) = (𝑦 ∩ 𝑣))
19	18	eleq2d 2826	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑧 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
20	17, 19	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → ((𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
21	20	cbvrexvw 3237	. . . . . . . . . 10 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))
22		df-rex 3070	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
23	21, 22	bitri 275	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
24	23	imbi2i 336	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
25		19.37v 1990	. . . . . . . 8 ⊢ (∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
26	24, 25	bitr4i 278	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
27	26	anbi2i 623	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
28		19.42v 1952	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
29		19.3v 1980	. . . . . . . 8 ⊢ (∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ 𝜑))
30		kmlem14.1	. . . . . . . . . 10 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))
31		elin 3966	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑦 ∩ 𝑣) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝑣))
32	31	baibr 536	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
33	32	anbi2d 630	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
34		anass 468	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
35	33, 34	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
36	35	pm5.74i 271	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)) ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
37	30, 36	bitri 275	. . . . . . . . 9 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
38	37	anbi2i 623	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
39	29, 38	bitr2i 276	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
40	39	exbii 1847	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
41	27, 28, 40	3bitr2i 299	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
42	41	albii 1818	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
43	15, 16, 42	3bitr2i 299	. . 3 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
44	43	exbii 1847	. 2 ⊢ (∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
45	7, 8, 44	3bitri 297	1 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1537  ∃wex 1778   ∈ wcel 2107  ∃!weu 2567   ≠ wne 2939  ∀wral 3060  ∃wrex 3069   ∩ cin 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-in 3957

This theorem is referenced by:  kmlem16  10207