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 35764

Description: Lemma for cvmlift 35769. 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 35760, cvmliftlem7 35761 (to show it is a function and a lift), cvmliftlem8 35762 (to show it is continuous), and cvmliftlem9 35763 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23432 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 12902	. . . 4 ⊢ ℕ = (ℤ_≥‘1)
3	1, 2	eleqtrdi 2873	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
4		eluzfz2 13561	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
5	3, 4	syl 18	. 2 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
6		eleq1 2851	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁)))
7		oveq2 7420	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (1...𝑦) = (1...1))
8		1z 12625	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
9		fzsn 13596	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → (1...1) = {1})
10	8, 9	ax-mp 5	. . . . . . . . . . 11 ⊢ (1...1) = {1}
11	7, 10	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (1...𝑦) = {1})
12	11	iuneq1d 4985	. . . . . . . . 9 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ {1} (𝑄‘𝑘))
13		1ex 11204	. . . . . . . . . 10 ⊢ 1 ∈ V
14		fveq2 6883	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑄‘𝑘) = (𝑄‘1))
15	13, 14	iunxsn 5058	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ {1} (𝑄‘𝑘) = (𝑄‘1)
16	12, 15	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = (𝑄‘1))
17		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁))
18	17	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁)))
19	18	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 = 1 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
20	19	oveq1d 7427	. . . . . . . 8 ⊢ (𝑦 = 1 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
21	16, 20	eleq12d 2857	. . . . . . 7 ⊢ (𝑦 = 1 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ (𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶)))
22	16	coeq2d 5850	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ (𝑄‘1)))
23	18	reseq2d 5980	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
24	22, 23	eqeq12d 2779	. . . . . . 7 ⊢ (𝑦 = 1 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
25	21, 24	anbi12d 643	. . . . . 6 ⊢ (𝑦 = 1 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
26	6, 25	imbi12d 347	. . . . 5 ⊢ (𝑦 = 1 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))))
27	26	imbi2d 343	. . . 4 ⊢ (𝑦 = 1 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))))
28		eleq1 2851	. . . . . 6 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁)))
29		oveq2 7420	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛))
30	29	iuneq1d 4985	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
31		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	31	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁)))
33	32	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
34	33	oveq1d 7427	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
35	30, 34	eleq12d 2857	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶)))
36	30	coeq2d 5850	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)))
37	32	reseq2d 5980	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
38	36, 37	eqeq12d 2779	. . . . . . 7 ⊢ (𝑦 = 𝑛 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
39	35, 38	anbi12d 643	. . . . . 6 ⊢ (𝑦 = 𝑛 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))
40	28, 39	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝑛 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))))
41	40	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝑛 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑛 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))))))
42		eleq1 2851	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁)))
43		oveq2 7420	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1)))
44	43	iuneq1d 4985	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
45		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
46	45	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁)))
47	46	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
48	47	oveq1d 7427	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
49	44, 48	eleq12d 2857	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)))
50	44	coeq2d 5850	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
51	46	reseq2d 5980	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
52	50, 51	eqeq12d 2779	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
53	49, 52	anbi12d 643	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
54	42, 53	imbi12d 347	. . . . 5 ⊢ (𝑦 = (𝑛 + 1) → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))))
55	54	imbi2d 343	. . . 4 ⊢ (𝑦 = (𝑛 + 1) → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → ((𝑛 + 1) ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))))
56		eleq1 2851	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁)))
57		oveq2 7420	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁))
58	57	iuneq1d 4985	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘))
59		cvmliftlem.k	. . . . . . . . 9 ⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)
60	58, 59	eqtr4di 2816	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = 𝐾)
61		oveq1 7419	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁))
62	61	oveq2d 7428	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁)))
63	62	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑁 / 𝑁))))
64	63	oveq1d 7427	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶))
65	60, 64	eleq12d 2857	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶)))
66	60	coeq2d 5850	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ 𝐾))
67	62	reseq2d 5980	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))
68	66, 67	eqeq12d 2779	. . . . . . 7 ⊢ (𝑦 = 𝑁 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
69	65, 68	anbi12d 643	. . . . . 6 ⊢ (𝑦 = 𝑁 → ((∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))) ↔ (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
70	56, 69	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝑁 → ((𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))))) ↔ (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
71	70	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝜑 → (𝑦 ∈ (1...𝑁) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁)))))) ↔ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))))
72		eluzfz1 13560	. . . . . . . . 9 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 1 ∈ (1...𝑁))
73	3, 72	syl 18	. . . . . . . 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 2763	. . . . . . . . 9 ⊢ (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (((1 − 1) / 𝑁)[,](1 / 𝑁))
86	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem8 35762	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
87	73, 86	mpdan 699	. . . . . . 7 ⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
88		1m1e0 12314	. . . . . . . . . . . 12 ⊢ (1 − 1) = 0
89	88	oveq1i 7422	. . . . . . . . . . 11 ⊢ ((1 − 1) / 𝑁) = (0 / 𝑁)
90	1	nncnd 12250	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
91	1	nnne0d 12287	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ≠ 0)
92	90, 91	div0d 11991	. . . . . . . . . . 11 ⊢ (𝜑 → (0 / 𝑁) = 0)
93	89, 92	eqtrid 2810	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 1) / 𝑁) = 0)
94	93	oveq1d 7427	. . . . . . . . 9 ⊢ (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁)))
95	94	oveq2d 7428	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
96	95	oveq1d 7427	. . . . . . 7 ⊢ (𝜑 → ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
97	87, 96	eleqtrd 2865	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
98		simpr 489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁))
99	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem7 35761	. . . . . . . . . 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 35760	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
101	73, 100	mpdan 699	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
102	101	simprd 500	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))
103	94	reseq2d 5980	. . . . . . 7 ⊢ (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
104	102, 103	eqtrd 2798	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))
105	97, 104	jca 520	. . . . 5 ⊢ (𝜑 → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
106	105	a1d 26	. . . 4 ⊢ (𝜑 → (1 ∈ (1...𝑁) → ((𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))))
107		elnnuz 12903	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
108	107	biimpi 219	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
109	108	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
110		peano2fzr 13566	. . . . . . . 8 ⊢ ((𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
111	110	ex 417	. . . . . . 7 ⊢ (𝑛 ∈ (ℤ_≥‘1) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
112	109, 111	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) ∈ (1...𝑁) → 𝑛 ∈ (1...𝑁)))
113	112	imim1d 83	. . . . 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 2763	. . . . . . . . 9 ⊢ ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))
116		0re 11211	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
117	114	simplbi 501	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
118	117	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
119	118	simprd 500	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ (1...𝑁))
120		elfznn 13583	. . . . . . . . . . . . . 14 ⊢ ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ)
121	119, 120	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℕ)
122	121	nnred 12249	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℝ)
123	1	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℕ)
124	122, 123	nndivred 12291	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
125		iccssre 13457	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
126	116, 124, 125	sylancr 598	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
127	117	simpld 499	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑛 ∈ ℕ)
128	127	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ)
129	128	nnred 12249	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℝ)
130	129, 123	nndivred 12291	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ)
131		icccld 24904	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
132	116, 130, 131	sylancr 598	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
133	83	fveq2i 6886	. . . . . . . . . . 11 ⊢ (Clsd‘𝐿) = (Clsd‘(topGen‘ran (,)))
134	132, 133	eleqtrrdi 2874	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿))
135		ssun1 4132	. . . . . . . . . . 11 ⊢ (0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
136	116	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ)
137	128	nnnn0d 12566	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ₀)
138	137	nn0ge0d 12569	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ 𝑛)
139	123	nnred 12249	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℝ)
140	123	nngt0d 12286	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 < 𝑁)
141		divge0 12085	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁))
142	129, 138, 139, 140, 141	syl22anc 851	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ (𝑛 / 𝑁))
143	129	ltp1d 12146	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 < (𝑛 + 1))
144		ltdiv1 12080	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℝ ∧ (𝑛 + 1) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
145	129, 122, 139, 140, 144	syl112anc 1401	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 < (𝑛 + 1) ↔ (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁)))
146	143, 145	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) < ((𝑛 + 1) / 𝑁))
147	130, 124, 146	ltled 11359	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
148		elicc2 13439	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
149	116, 124, 148	sylancr 598	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
150	130, 142, 147, 149	mpbir3and 1361	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)))
151		iccsplit 13513	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ ∧ (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁))) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
152	136, 124, 150, 151	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
153	135, 152	sseqtrrid 3981	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
154		uniretop 24900	. . . . . . . . . . . 12 ⊢ ℝ = ∪ (topGen‘ran (,))
155	83	unieqi 4885	. . . . . . . . . . . 12 ⊢ ∪ 𝐿 = ∪ (topGen‘ran (,))
156	154, 155	eqtr4i 2789	. . . . . . . . . . 11 ⊢ ℝ = ∪ 𝐿
157	156	restcldi 23311	. . . . . . . . . 10 ⊢ (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿) ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
158	126, 134, 153, 157	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
159		icccld 24904	. . . . . . . . . . . 12 ⊢ (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
160	130, 124, 159	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
161	160, 133	eleqtrrdi 2874	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿))
162		ssun2 4133	. . . . . . . . . . 11 ⊢ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
163	162, 152	sseqtrrid 3981	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
164	156	restcldi 23311	. . . . . . . . . 10 ⊢ (((0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿) ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁))) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
165	126, 161, 163, 164	syl3anc 1398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))))
166		retop 24899	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) ∈ Top
167	83, 166	eqeltri 2859	. . . . . . . . . . 11 ⊢ 𝐿 ∈ Top
168	156	restuni 23300	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ Top ∧ (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
169	167, 126, 168	sylancr 598	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
170	152, 169	eqtr3d 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
171	114	simprbi 502	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
172	171	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
173	172	simpld 499	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
174		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))
175	174, 75	cnf 23384	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
176	173, 175	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
177		iccssre 13457	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
178	116, 130, 177	sylancr 598	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
179	156	restuni 23300	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
180	167, 178, 179	sylancr 598	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
181	180	feq2d 6691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵))
182	176, 181	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵)
183		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
184		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑛 + 1) ∈ (1...𝑁))
185	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem7 35761	. . . . . . . . . . . . . . . 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 35760	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
187	119, 186	syldan 602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
188	187	simpld 499	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
189	128	nncnd 12250	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℂ)
190		ax-1cn 11159	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
191		pncan 11464	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
192	189, 190, 191	sylancl 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) − 1) = 𝑛)
193	192	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
194	193	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
195	194	feq2d 6691	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
196	188, 195	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
197	176	ffund 6712	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
198	128, 108	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (ℤ_≥‘1))
199		eluzfz2 13561	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ (1...𝑛))
200	198, 199	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑛))
201		fveq2 6883	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝑄‘𝑘) = (𝑄‘𝑛))
202	201	ssiun2s 5014	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑛) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
203	200, 202	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
204		peano2rem 11526	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
205	129, 204	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) ∈ ℝ)
206	205, 123	nndivred 12291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ)
207	206	rexrd 11260	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ^*)
208	130	rexrd 11260	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ^*)
209	129	ltm1d 12148	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) < 𝑛)
210		ltdiv1 12080	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
211	205, 129, 139, 140, 210	syl112anc 1401	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) < 𝑛 ↔ ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁)))
212	209, 211	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) < (𝑛 / 𝑁))
213	206, 130, 212	ltled 11359	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁))
214		ubicc2 13493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 − 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
215	207, 208, 213, 214	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
216	198, 119, 110	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑁))
217		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))
218		simpr 489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
219	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217	cvmliftlem7 35761	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))}))
220	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219	cvmliftlem6 35760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
221	216, 220	syldan 602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
222	221	simpld 499	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵)
223	222	fdmd 6718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → dom (𝑄‘𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
224	215, 223	eleqtrrd 2866	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛))
225		funssfv 6904	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛)) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
226	197, 203, 224, 225	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
227	192	fveq2d 6887	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
228	227, 193	fveq12d 6890	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
229	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84	cvmliftlem9 35763	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
230	119, 229	syldan 602	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
231	193	fveq2d 6887	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
232	230, 231	eqtr3d 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
233	226, 228, 232	3eqtr2d 2804	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
234	233	opeq2d 4846	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩ = ⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩)
235	234	sneqd 4602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩} = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
236	182	ffnd 6708	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)))
237		0xr 11257	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ^*
238	237	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ^*)
239		ubicc2 13493	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 0 ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
240	238, 208, 142, 239	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
241		fnressn 7157	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
242	236, 240, 241	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
243	196	ffnd 6708	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
244	124	rexrd 11260	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
245		lbicc2 13492	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
246	208, 244, 147, 245	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
247		fnressn 7157	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
248	243, 246, 247	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
249	235, 242, 248	3eqtr4d 2808	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
250		df-icc 13380	. . . . . . . . . . . . . . . . 17 ⊢ [,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
251		xrmaxle 13210	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧)))
252		xrlemin 13211	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^*) → (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁))))
253	250, 251, 252	ixxin 13390	. . . . . . . . . . . . . . . 16 ⊢ (((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^) ∧ ((𝑛 / 𝑁) ∈ ℝ^ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^*)) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
254	238, 208, 208, 244, 253	syl22anc 851	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
255	142	iftrued 4496	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁))
256	147	iftrued 4496	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁))
257	255, 256	oveq12d 7430	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁)))
258		iccid 13418	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 / 𝑁) ∈ ℝ^* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
259	208, 258	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
260	254, 257, 259	3eqtrd 2802	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)})
261	260	reseq2d 5980	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}))
262	260	reseq2d 5980	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
263	249, 261, 262	3eqtr4d 2808	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
264		fresaun 6751	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
265	182, 196, 263, 264	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
266		fzsuc 13601	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
267	198, 266	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
268	267	iuneq1d 4985	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) = ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘))
269		iunxun 5061	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘))
270		ovex 7445	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 + 1) ∈ V
271		fveq2 6883	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑛 + 1) → (𝑄‘𝑘) = (𝑄‘(𝑛 + 1)))
272	270, 271	iunxsn 5058	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘) = (𝑄‘(𝑛 + 1))
273	272	uneq2i 4120	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘)) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
274	269, 273	eqtri 2786	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
275	268, 274	eqtr2di 2815	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
276	275	feq1d 6689	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
277	265, 276	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
278	170	feq2d 6691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
279	277, 278	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
280	275	reseq1d 5979	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))))
281		fresaunres1 6753	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
282	182, 196, 263, 281	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
283	280, 282	eqtr3d 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
284	167	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝐿 ∈ Top)
285		ovex 7445	. . . . . . . . . . . . 13 ⊢ (0[,]((𝑛 + 1) / 𝑁)) ∈ V
286	285	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V)
287		restabs 23303	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
288	284, 153, 286, 287	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
289	288	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
290	173, 283, 289	3eltr4d 2878	. . . . . . . . 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 35762	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
292	119, 291	syldan 602	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
293	194	oveq2d 7428	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
294	293	oveq1d 7427	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
295	292, 294	eleqtrd 2865	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
296	275	reseq1d 5979	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
297		fresaunres2 6752	. . . . . . . . . . . 12 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
298	182, 196, 263, 297	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
299	296, 298	eqtr3d 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
300		restabs 23303	. . . . . . . . . . . 12 ⊢ ((𝐿 ∈ Top ∧ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)) ∧ (0[,]((𝑛 + 1) / 𝑁)) ∈ V) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
301	284, 163, 286, 300	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
302	301	oveq1d 7427	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
303	295, 299, 302	3eltr4d 2878	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
304	115, 75, 158, 165, 170, 279, 290, 303	paste 23432	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
305	152	reseq2d 5980	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
306	172	simprd 500	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
307	187	simprd 500	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
308	194	reseq2d 5980	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
309	307, 308	eqtrd 2798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
310	306, 309	uneq12d 4124	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
311		coundi 6250	. . . . . . . . . 10 ⊢ (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1))))
312		resundi 5994	. . . . . . . . . 10 ⊢ (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
313	310, 311, 312	3eqtr4g 2823	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
314	275	coeq2d 5850	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
315	305, 313, 314	3eqtr2rd 2805	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
316	304, 315	jca 520	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
317	114, 316	sylan2br 606	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
318	317	expr 461	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
319	113, 318	animpimp2impd 859	. . . 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 12252	. . 3 ⊢ (𝑁 ∈ ℕ → (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))))
321	1, 320	mpcom 39	. 2 ⊢ (𝜑 → (𝑁 ∈ (1...𝑁) → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))))
322	5, 321	mpd 16	1 ⊢ (𝜑 → (𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ∀wral 3079 {crab 3416 Vcvv 3455 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4287 ifcif 4488 𝒫 cpw 4563 {csn 4590 ⟨cop 4596 ∪ cuni 4873 ∪ ciun 4957 class class class wbr 5110 ↦ cmpt 5193 I cid 5557 × cxp 5661 ^◡ccnv 5662 dom cdm 5663 ran crn 5664 ↾ cres 5665 “ cima 5666 ∘ ccom 5667 Fun wfun 6532 Fn wfn 6533 ⟶wf 6534 ‘cfv 6538 ℩crio 7368 (class class class)co 7412 ∈ cmpo 7414 1^st c1st 7985 2^nd c2nd 7986 ℂcc 11099 ℝcr 11100 0cc0 11101 1c1 11102 + caddc 11104 ℝ^*cxr 11243 < clt 11244 ≤ cle 11245 − cmin 11442 / cdiv 11872 ℕcn 12234 ℤcz 12592 ℤ_≥cuz 12863 (,)cioo 13373 [,]cicc 13376 ...cfz 13536 seqcseq 14039 ↾_t crest 17474 topGenctg 17491 Topctop 23031 Clsdccld 23154 Cn ccn 23362 Homeochmeo 23891 IIcii 25015 CovMap ccvm 35725

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178 ax-pre-sup 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-int 4914 df-iun 4959 df-iin 4960 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-map 8827 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-fi 9372 df-sup 9403 df-inf 9404 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-2 12304 df-3 12305 df-n0 12506 df-z 12593 df-uz 12864 df-q 12974 df-rp 13018 df-xneg 13138 df-xadd 13139 df-xmul 13140 df-ioo 13377 df-icc 13380 df-fz 13537 df-seq 14040 df-exp 14100 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-rest 17476 df-topgen 17497 df-psmet 21495 df-xmet 21496 df-met 21497 df-bl 21498 df-mopn 21499 df-top 23032 df-topon 23049 df-bases 23084 df-cld 23157 df-cn 23365 df-hmeo 23893 df-ii 25017 df-cvm 35726

This theorem is referenced by: cvmliftlem11 35765

W3C validator