cvmliftlem10 - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cvmliftlem10		Structured version Visualization version GIF version

Theorem cvmliftlem10 35488

Description: Lemma for cvmlift 35493. The function 𝐾 is going to be our complete lifted path, formed by unioning together all the 𝑄 functions (each of which is defined on one segment [(𝑀 − 1) / 𝑁, 𝑀 / 𝑁] of the interval). Here we prove by induction that 𝐾 is a continuous function and a lift of 𝐺 by applying cvmliftlem6 35484, cvmliftlem7 35485 (to show it is a function and a lift), cvmliftlem8 35486 (to show it is continuous), and cvmliftlem9 35487 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23238 gives that 𝐾 is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)

**Hypotheses**
Ref	Expression
cvmliftlem.1	⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
cvmliftlem.b	⊢ 𝐵 = ∪ 𝐶
cvmliftlem.x	⊢ 𝑋 = ∪ 𝐽
cvmliftlem.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
cvmliftlem.g	⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))
cvmliftlem.p	⊢ (𝜑 → 𝑃 ∈ 𝐵)
cvmliftlem.e	⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))
cvmliftlem.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
cvmliftlem.t	⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
cvmliftlem.a	⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1^st ‘(𝑇‘𝑘)))
cvmliftlem.l	⊢ 𝐿 = (topGen‘ran (,))
cvmliftlem.q	⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
cvmliftlem.k	⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)
cvmliftlem10.1	⊢ (𝜒 ↔ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))

**Assertion**
Ref	Expression
cvmliftlem10	⊢ (𝜑 → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))

Distinct variable groups: 𝑣,𝑏,𝑧,𝐵 𝑗,𝑏,𝑘,𝑚,𝑛,𝑠,𝑢,𝑥,𝐹,𝑣,𝑧 𝑛,𝐿,𝑧 𝑃,𝑏,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑧 𝐶,𝑏,𝑗,𝑘,𝑛,𝑠,𝑢,𝑣,𝑧 𝜑,𝑗,𝑛,𝑠,𝑥,𝑧 𝑁,𝑏,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑧 𝑆,𝑏,𝑗,𝑘,𝑛,𝑠,𝑢,𝑣,𝑥,𝑧 𝑗,𝑋 𝐺,𝑏,𝑗,𝑘,𝑚,𝑛,𝑠,𝑢,𝑣,𝑥,𝑧 𝑇,𝑏,𝑗,𝑘,𝑚,𝑠,𝑢,𝑣,𝑥,𝑧 𝐽,𝑏,𝑗,𝑘,𝑛,𝑠,𝑢,𝑣,𝑥,𝑧 𝑄,𝑏,𝑘,𝑚,𝑛,𝑢,𝑣,𝑥,𝑧 Allowed substitution hints: 𝜑(𝑣,𝑢,𝑘,𝑚,𝑏) 𝜒(𝑥,𝑧,𝑣,𝑢,𝑗,𝑘,𝑚,𝑛,𝑠,𝑏) 𝐵(𝑥,𝑢,𝑗,𝑘,𝑚,𝑛,𝑠) 𝐶(𝑥,𝑚) 𝑃(𝑗,𝑠) 𝑄(𝑗,𝑠) 𝑆(𝑚) 𝑇(𝑛) 𝐽(𝑚) 𝐾(𝑥,𝑧,𝑣,𝑢,𝑗,𝑘,𝑚,𝑛,𝑠,𝑏) 𝐿(𝑥,𝑣,𝑢,𝑗,𝑘,𝑚,𝑠,𝑏) 𝑁(𝑗,𝑠) 𝑋(𝑥,𝑧,𝑣,𝑢,𝑘,𝑚,𝑛,𝑠,𝑏)

Proof of Theorem cvmliftlem10 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvmliftlem.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2		nnuz 12790	. . . 4 ⊢ ℕ = (ℤ_≥‘1)
3	1, 2	eleqtrdi 2846	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
4		eluzfz2 13448	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
6		eleq1 2824	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁)))
7		oveq2 7366	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (1...𝑦) = (1...1))
8		1z 12521	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
9		fzsn 13482	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → (1...1) = {1})
10	8, 9	ax-mp 5	. . . . . . . . . . 11 ⊢ (1...1) = {1}
11	7, 10	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (1...𝑦) = {1})
12	11	iuneq1d 4974	. . . . . . . . 9 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ {1} (𝑄‘𝑘))
13		1ex 11128	. . . . . . . . . 10 ⊢ 1 ∈ V
14		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑄‘𝑘) = (𝑄‘1))
15	13, 14	iunxsn 5046	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ {1} (𝑄‘𝑘) = (𝑄‘1)
16	12, 15	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = (𝑄‘1))
17		oveq1 7365	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁))
18	17	oveq2d 7374	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁)))
19	18	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑦 = 1 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
20	19	oveq1d 7373	. . . . . . . 8 ⊢ (𝑦 = 1 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
21	16, 20	eleq12d 2830	. . . . . . 7 ⊢ (𝑦 = 1 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ (𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶)))
22	16	coeq2d 5811	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ (𝑄‘1)))
23	18	reseq2d 5938	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
24	22, 23	eqeq12d 2752	. . . . . . 7 ⊢ (𝑦 = 1 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
25	21, 24	anbi12d 632	. . . . . 6 ⊢ (𝑦 = 1 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
26	6, 25	imbi12d 344	. . . . 5 ⊢ (𝑦 = 1 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))))
27	26	imbi2d 340	. . . 4 ⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))))
28		eleq1 2824	. . . . . 6 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁)))
29		oveq2 7366	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛))
30	29	iuneq1d 4974	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
31		oveq1 7365	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	31	oveq2d 7374	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁)))
33	32	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
34	33	oveq1d 7373	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
35	30, 34	eleq12d 2830	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶)))
36	30	coeq2d 5811	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)))
37	32	reseq2d 5938	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
38	36, 37	eqeq12d 2752	. . . . . . 7 ⊢ (𝑦 = 𝑛 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
39	35, 38	anbi12d 632	. . . . . 6 ⊢ (𝑦 = 𝑛 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
40	28, 39	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
41	40	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))))
42		eleq1 2824	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁)))
43		oveq2 7366	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1)))
44	43	iuneq1d 4974	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
45		oveq1 7365	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
46	45	oveq2d 7374	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁)))
47	46	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
48	47	oveq1d 7373	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
49	44, 48	eleq12d 2830	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)))
50	44	coeq2d 5811	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
51	46	reseq2d 5938	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
52	50, 51	eqeq12d 2752	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
53	49, 52	anbi12d 632	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
54	42, 53	imbi12d 344	. . . . 5 ⊢ (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))
55	54	imbi2d 340	. . . 4 ⊢ (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
56		eleq1 2824	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁)))
57		oveq2 7366	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁))
58	57	iuneq1d 4974	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘))
59		cvmliftlem.k	. . . . . . . . 9 ⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)
60	58, 59	eqtr4di 2789	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = 𝐾)
61		oveq1 7365	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁))
62	61	oveq2d 7374	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁)))
63	62	oveq2d 7374	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑁 / 𝑁))))
64	63	oveq1d 7373	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶))
65	60, 64	eleq12d 2830	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶)))
66	60	coeq2d 5811	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ 𝐾))
67	62	reseq2d 5938	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))
68	66, 67	eqeq12d 2752	. . . . . . 7 ⊢ (𝑦 = 𝑁 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
69	65, 68	anbi12d 632	. . . . . 6 ⊢ (𝑦 = 𝑁 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
70	56, 69	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
71	70	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))))
72		eluzfz1 13447	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 1 ∈ (1...𝑁))
73	3, 72	syl 17	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ (1...𝑁))
74		cvmliftlem.1	. . . . . . . . 9 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
75		cvmliftlem.b	. . . . . . . . 9 ⊢ 𝐵 = ∪ 𝐶
76		cvmliftlem.x	. . . . . . . . 9 ⊢ 𝑋 = ∪ 𝐽
77		cvmliftlem.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
78		cvmliftlem.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))
79		cvmliftlem.p	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
80		cvmliftlem.e	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))
81		cvmliftlem.t	. . . . . . . . 9 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
82		cvmliftlem.a	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1^st ‘(𝑇‘𝑘)))
83		cvmliftlem.l	. . . . . . . . 9 ⊢ 𝐿 = (topGen‘ran (,))
84		cvmliftlem.q	. . . . . . . . 9 ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
85		eqid 2736	. . . . . . . . 9 ⊢ (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (((1 − 1) / 𝑁)[,](1 / 𝑁))
86	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem8 35486	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
87	73, 86	mpdan 687	. . . . . . 7 ⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
88		1m1e0 12217	. . . . . . . . . . . 12 ⊢ (1 − 1) = 0
89	88	oveq1i 7368	. . . . . . . . . . 11 ⊢ ((1 − 1) / 𝑁) = (0 / 𝑁)
90	1	nncnd 12161	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
91	1	nnne0d 12195	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ≠ 0)
92	90, 91	div0d 11916	. . . . . . . . . . 11 ⊢ (𝜑 → (0 / 𝑁) = 0)
93	89, 92	eqtrid 2783	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 1) / 𝑁) = 0)
94	93	oveq1d 7373	. . . . . . . . 9 ⊢ (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁)))
95	94	oveq2d 7374	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
96	95	oveq1d 7373	. . . . . . 7 ⊢ (𝜑 → ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
97	87, 96	eleqtrd 2838	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
98		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁))
99	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem7 35485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘(1 − 1))‘((1 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((1 − 1) / 𝑁))}))
100	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99	cvmliftlem6 35484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
101	73, 100	mpdan 687	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
102	101	simprd 495	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))
103	94	reseq2d 5938	. . . . . . 7 ⊢ (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
104	102, 103	eqtrd 2771	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))
105	97, 104	jca 511	. . . . 5 ⊢ (𝜑 → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
106	105	a1d 25	. . . 4 ⊢ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
107		elnnuz 12791	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
108	107	biimpi 216	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
109	108	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
110		peano2fzr 13453	. . . . . . . 8 ⊢ ((𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
111	110	ex 412	. . . . . . 7 ⊢ (𝑛 ∈ (ℤ_≥‘1) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
112	109, 111	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
113	112	imim1d 82	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))) → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
114		cvmliftlem10.1	. . . . . . 7 ⊢ (𝜒 ↔ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
115		eqid 2736	. . . . . . . . 9 ⊢ ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))
116		0re 11134	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
117	114	simplbi 497	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
118	117	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
119	118	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ (1...𝑁))
120		elfznn 13469	. . . . . . . . . . . . . 14 ⊢ ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ)
121	119, 120	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℕ)
122	121	nnred 12160	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℝ)
123	1	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℕ)
124	122, 123	nndivred 12199	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
125		iccssre 13345	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
126	116, 124, 125	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
127	117	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑛 ∈ ℕ)
128	127	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ)
129	128	nnred 12160	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℝ)
130	129, 123	nndivred 12199	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ)
131		icccld 24710	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
132	116, 130, 131	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
133	83	fveq2i 6837	. . . . . . . . . . 11 ⊢ (Clsd‘𝐿) = (Clsd‘(topGen‘ran (,)))
134	132, 133	eleqtrrdi 2847	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿))
135		ssun1 4130	. . . . . . . . . . 11 ⊢ (0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
136	116	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ)
137	128	nnnn0d 12462	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ₀)
138	137	nn0ge0d 12465	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ 𝑛)
139	123	nnred 12160	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℝ)
140	123	nngt0d 12194	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 < 𝑁)
141		divge0 12011	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁))
142	129, 138, 139, 140, 141	syl22anc 838	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ (𝑛 / 𝑁))
143	129	ltp1d 12072	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 < (𝑛 + 1))
144		ltdiv1 12006	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
145	129, 122, 139, 140, 144	syl112anc 1376	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
146	143, 145	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
147	130, 124, 146	ltled 11281	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
148		elicc2 13327	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
149	116, 124, 148	sylancr 587	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
150	130, 142, 147, 149	mpbir3and 1343	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)))
151		iccsplit 13401	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ ∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
152	136, 124, 150, 151	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
153	135, 152	sseqtrrid 3977	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
154		uniretop 24706	. . . . . . . . . . . 12 ⊢ ℝ = ∪ (topGen‘ran (,))
155	83	unieqi 4875	. . . . . . . . . . . 12 ⊢ ∪ 𝐿 = ∪ (topGen‘ran (,))
156	154, 155	eqtr4i 2762	. . . . . . . . . . 11 ⊢ ℝ = ∪ 𝐿
157	156	restcldi 23117	. . . . . . . . . 10 ⊢ (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿) ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
158	126, 134, 153, 157	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
159		icccld 24710	. . . . . . . . . . . 12 ⊢ (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
160	130, 124, 159	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
161	160, 133	eleqtrrdi 2847	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿))
162		ssun2 4131	. . . . . . . . . . 11 ⊢ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
163	162, 152	sseqtrrid 3977	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
164	156	restcldi 23117	. . . . . . . . . 10 ⊢ (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
165	126, 161, 163, 164	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
166		retop 24705	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) ∈ Top
167	83, 166	eqeltri 2832	. . . . . . . . . . 11 ⊢ 𝐿 ∈ Top
168	156	restuni 23106	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ Top ∧ (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
169	167, 126, 168	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
170	152, 169	eqtr3d 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
171	114	simprbi 496	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
172	171	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
173	172	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
174		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))
175	174, 75	cnf 23190	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
176	173, 175	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
177		iccssre 13345	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
178	116, 130, 177	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
179	156	restuni 23106	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
180	167, 178, 179	sylancr 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
181	180	feq2d 6646	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵))
182	176, 181	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵)
183		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
184		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑛 + 1) ∈ (1...𝑁))
185	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem7 35485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘(((𝑛 + 1) − 1) / 𝑁))}))
186	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185	cvmliftlem6 35484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
187	119, 186	syldan 591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
188	187	simpld 494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
189	128	nncnd 12161	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℂ)
190		ax-1cn 11084	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
191		pncan 11386	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
192	189, 190, 191	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) − 1) = 𝑛)
193	192	oveq1d 7373	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
194	193	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
195	194	feq2d 6646	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
196	188, 195	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
197	176	ffund 6666	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
198	128, 108	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (ℤ_≥‘1))
199		eluzfz2 13448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ (1...𝑛))
200	198, 199	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑛))
201		fveq2 6834	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝑄‘𝑘) = (𝑄‘𝑛))
202	201	ssiun2s 5004	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑛) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
203	200, 202	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
204		peano2rem 11448	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
205	129, 204	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) ∈ ℝ)
206	205, 123	nndivred 12199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ)
207	206	rexrd 11182	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ^*)
208	130	rexrd 11182	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ^*)
209	129	ltm1d 12074	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) < 𝑛)
210		ltdiv1 12006	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
211	205, 129, 139, 140, 210	syl112anc 1376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
212	209, 211	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))
213	206, 130, 212	ltled 11281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁))
214		ubicc2 13381	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 − 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
215	207, 208, 213, 214	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
216	198, 119, 110	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑁))
217		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))
218		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
219	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217	cvmliftlem7 35485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))}))
220	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219	cvmliftlem6 35484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
221	216, 220	syldan 591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
222	221	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵)
223	222	fdmd 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → dom (𝑄‘𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
224	215, 223	eleqtrrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛))
225		funssfv 6855	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛)) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
226	197, 203, 224, 225	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
227	192	fveq2d 6838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
228	227, 193	fveq12d 6841	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
229	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84	cvmliftlem9 35487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
230	119, 229	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
231	193	fveq2d 6838	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
232	230, 231	eqtr3d 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
233	226, 228, 232	3eqtr2d 2777	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
234	233	opeq2d 4836	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩ = ⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩)
235	234	sneqd 4592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩} = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
236	182	ffnd 6663	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)))
237		0xr 11179	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ^*
238	237	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ^*)
239		ubicc2 13381	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 0 ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
240	238, 208, 142, 239	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
241		fnressn 7103	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
242	236, 240, 241	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
243	196	ffnd 6663	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
244	124	rexrd 11182	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
245		lbicc2 13380	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
246	208, 244, 147, 245	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
247		fnressn 7103	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
248	243, 246, 247	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
249	235, 242, 248	3eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
250		df-icc 13268	. . . . . . . . . . . . . . . . 17 ⊢ [,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
251		xrmaxle 13098	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧)))
252		xrlemin 13099	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^*) → (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁))))
253	250, 251, 252	ixxin 13278	. . . . . . . . . . . . . . . 16 ⊢ (((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^) ∧ ((𝑛 / 𝑁) ∈ ℝ^ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^*)) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
254	238, 208, 208, 244, 253	syl22anc 838	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
255	142	iftrued 4487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁))
256	147	iftrued 4487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁))
257	255, 256	oveq12d 7376	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁)))
258		iccid 13306	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 / 𝑁) ∈ ℝ^* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
259	208, 258	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
260	254, 257, 259	3eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)})
261	260	reseq2d 5938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}))
262	260	reseq2d 5938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
263	249, 261, 262	3eqtr4d 2781	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
264		fresaun 6705	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
265	182, 196, 263, 264	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
266		fzsuc 13487	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
267	198, 266	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
268	267	iuneq1d 4974	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) = ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘))
269		iunxun 5049	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘))
270		ovex 7391	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 + 1) ∈ V
271		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑛 + 1) → (𝑄‘𝑘) = (𝑄‘(𝑛 + 1)))
272	270, 271	iunxsn 5046	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘) = (𝑄‘(𝑛 + 1))
273	272	uneq2i 4117	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘)) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
274	269, 273	eqtri 2759	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
275	268, 274	eqtr2di 2788	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
276	275	feq1d 6644	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
277	265, 276	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
278	170	feq2d 6646	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
279	277, 278	mpbid 232	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
280	275	reseq1d 5937	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))))
281		fresaunres1 6707	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
282	182, 196, 263, 281	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
283	280, 282	eqtr3d 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
284	167	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝐿 ∈ Top)
285		ovex 7391	. . . . . . . . . . . . 13 ⊢ (0[,]((𝑛 + 1) / 𝑁)) ∈ V
286	285	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V)
287		restabs 23109	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
288	284, 153, 286, 287	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
289	288	oveq1d 7373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
290	173, 283, 289	3eltr4d 2851	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) ∈ (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
291	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem8 35486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
292	119, 291	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
293	194	oveq2d 7374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
294	293	oveq1d 7373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
295	292, 294	eleqtrd 2838	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
296	275	reseq1d 5937	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
297		fresaunres2 6706	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
298	182, 196, 263, 297	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
299	296, 298	eqtr3d 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
300		restabs 23109	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
301	284, 163, 286, 300	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
302	301	oveq1d 7373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
303	295, 299, 302	3eltr4d 2851	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
304	115, 75, 158, 165, 170, 279, 290, 303	paste 23238	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
305	152	reseq2d 5938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
306	172	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
307	187	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
308	194	reseq2d 5938	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
309	307, 308	eqtrd 2771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
310	306, 309	uneq12d 4121	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
311		coundi 6205	. . . . . . . . . 10 ⊢ (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1))))
312		resundi 5952	. . . . . . . . . 10 ⊢ (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
313	310, 311, 312	3eqtr4g 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
314	275	coeq2d 5811	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
315	305, 313, 314	3eqtr2rd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
316	304, 315	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
317	114, 316	sylan2br 595	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
318	317	expr 456	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
319	113, 318	animpimp2impd 846	. . . 4 ⊢ (𝑛 ∈ ℕ → ((𝜑 → (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
320	27, 41, 55, 71, 106, 319	nnind 12163	. . 3 ⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
321	1, 320	mpcom 38	. 2 ⊢ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
322	5, 321	mpd 15	1 ⊢ (𝜑 → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∀wral 3051 {crab 3399 Vcvv 3440 ∖ cdif 3898 ∪ cun 3899 ∩ cin 3900 ⊆ wss 3901 ∅c0 4285 ifcif 4479 𝒫 cpw 4554 {csn 4580 ⟨cop 4586 ∪ cuni 4863 ∪ ciun 4946 class class class wbr 5098 ↦ cmpt 5179 I cid 5518 × cxp 5622 ^◡ccnv 5623 dom cdm 5624 ran crn 5625 ↾ cres 5626 “ cima 5627 ∘ ccom 5628 Fun wfun 6486 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 ℩crio 7314 (class class class)co 7358 ∈ cmpo 7360 1^st c1st 7931 2^nd c2nd 7932 ℂcc 11024 ℝcr 11025 0cc0 11026 1c1 11027 + caddc 11029 ℝ^*cxr 11165 < clt 11166 ≤ cle 11167 − cmin 11364 / cdiv 11794 ℕcn 12145 ℤcz 12488 ℤ_≥cuz 12751 (,)cioo 13261 [,]cicc 13264 ...cfz 13423 seqcseq 13924 ↾_t crest 17340 topGenctg 17357 Topctop 22837 Clsdccld 22960 Cn ccn 23168 Homeochmeo 23697 IIcii 24824 CovMap ccvm 35449

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-er 8635 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fi 9314 df-sup 9345 df-inf 9346 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-n0 12402 df-z 12489 df-uz 12752 df-q 12862 df-rp 12906 df-xneg 13026 df-xadd 13027 df-xmul 13028 df-ioo 13265 df-icc 13268 df-fz 13424 df-seq 13925 df-exp 13985 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-rest 17342 df-topgen 17363 df-psmet 21301 df-xmet 21302 df-met 21303 df-bl 21304 df-mopn 21305 df-top 22838 df-topon 22855 df-bases 22890 df-cld 22963 df-cn 23171 df-hmeo 23699 df-ii 24826 df-cvm 35450

This theorem is referenced by: cvmliftlem11 35489

W3C validator