Theorem kmlem14 8985

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 2856	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 𝑤 ↔ 𝑦 ≠ 𝑤))
2		ineq1 3807	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (𝑧 ∩ 𝑤) = (𝑦 ∩ 𝑤))
3	2	eleq2d 2687	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ 𝑣 ∈ (𝑦 ∩ 𝑤)))
4	1, 3	anbi12d 747	. . . . 5 ⊢ (𝑧 = 𝑦 → ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
5	4	rexbidv 3052	. . . 4 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
6	5	raleqbi1dv 3146	. . 3 ⊢ (𝑧 = 𝑦 → (∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
7	6	cbvrexv 3172	. 2 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)))
8		df-rex 2918	. 2 ⊢ (∃𝑦 ∈ 𝑥 ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))))
9		eleq1 2689	. . . . . . . . 9 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑤)))
10	9	anbi2d 740	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → ((𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
11	10	rexbidv 3052	. . . . . . 7 ⊢ (𝑣 = 𝑧 → (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
12	11	cbvralv 3171	. . . . . 6 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))
13		df-ral 2917	. . . . . 6 ⊢ (∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
14	12, 13	bitri 264	. . . . 5 ⊢ (∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤)) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))))
15	14	anbi2i 730	. . . 4 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
16		19.28v 1909	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))))
17		neeq2 2857	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑦 ≠ 𝑤 ↔ 𝑦 ≠ 𝑣))
18		ineq2 3808	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑣 → (𝑦 ∩ 𝑤) = (𝑦 ∩ 𝑣))
19	18	eleq2d 2687	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑧 ∈ (𝑦 ∩ 𝑤) ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
20	17, 19	anbi12d 747	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑣 → ((𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
21	20	cbvrexv 3172	. . . . . . . . . 10 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))
22		df-rex 2918	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑥 (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
23	21, 22	bitri 264	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)) ↔ ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
24	23	imbi2i 326	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
25		19.37v 1910	. . . . . . . 8 ⊢ (∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))) ↔ (𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
26	24, 25	bitr4i 267	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
27	26	anbi2i 730	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
28		19.42v 1918	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ (𝑦 ∈ 𝑥 ∧ ∃𝑣(𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
29		19.3v 1897	. . . . . . . 8 ⊢ (∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ 𝜑))
30		kmlem14.1	. . . . . . . . . 10 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)))
31		elin 3796	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ (𝑦 ∩ 𝑣) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ 𝑣))
32	31	baibr 945	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ 𝑣 ↔ 𝑧 ∈ (𝑦 ∩ 𝑣)))
33	32	anbi2d 740	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
34		anass 681	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))
35	33, 34	syl6bb 276	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑦 → (((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣) ↔ (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
36	35	pm5.74i 260	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 → ((𝑣 ∈ 𝑥 ∧ 𝑦 ≠ 𝑣) ∧ 𝑧 ∈ 𝑣)) ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
37	30, 36	bitri 264	. . . . . . . . 9 ⊢ (𝜑 ↔ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣)))))
38	37	anbi2i 730	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝜑) ↔ (𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))))
39	29, 38	bitr2i 265	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
40	39	exbii 1774	. . . . . 6 ⊢ (∃𝑣(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → (𝑣 ∈ 𝑥 ∧ (𝑦 ≠ 𝑣 ∧ 𝑧 ∈ (𝑦 ∩ 𝑣))))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
41	27, 28, 40	3bitr2i 288	. . . . 5 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
42	41	albii 1747	. . . 4 ⊢ (∀𝑧(𝑦 ∈ 𝑥 ∧ (𝑧 ∈ 𝑦 → ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑧 ∈ (𝑦 ∩ 𝑤)))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
43	15, 16, 42	3bitr2i 288	. . 3 ⊢ ((𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
44	43	exbii 1774	. 2 ⊢ (∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑦 ∃𝑤 ∈ 𝑥 (𝑦 ≠ 𝑤 ∧ 𝑣 ∈ (𝑦 ∩ 𝑤))) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))
45	7, 8, 44	3bitri 286	1 ⊢ (∃𝑧 ∈ 𝑥 ∀𝑣 ∈ 𝑧 ∃𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑦∀𝑧∃𝑣∀𝑢(𝑦 ∈ 𝑥 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481  ∃wex 1704   ∈ wcel 1990  ∃!weu 2470   ≠ wne 2794  ∀wral 2912  ∃wrex 2913   ∩ cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581

This theorem is referenced by:  kmlem16  8987