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 35881

Description: Lemma for cvmlift 35886. 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 35877, cvmliftlem7 35878 (to show it is a function and a lift), cvmliftlem8 35879 (to show it is continuous), and cvmliftlem9 35880 (to show that different 𝑄 functions agree on the intersection of their domains, so that the pasting lemma paste 23525 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 12930	. . . 4 ⊢ ℕ = (ℤ_≥‘1)
3	1, 2	eleqtrdi 2872	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
4		eluzfz2 13590	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘1) → 𝑁 ∈ (1...𝑁))
5	3, 4	syl 18	. 2 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
6		eleq1 2850	. . . . . 6 ⊢ (𝑦 = 1 → (𝑦 ∈ (1...𝑁) ↔ 1 ∈ (1...𝑁)))
7		oveq2 7425	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (1...𝑦) = (1...1))
8		1z 12652	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
9		fzsn 13625	. . . . . . . . . . . 12 ⊢ (1 ∈ ℤ → (1...1) = {1})
10	8, 9	ax-mp 5	. . . . . . . . . . 11 ⊢ (1...1) = {1}
11	7, 10	eqtrdi 2813	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (1...𝑦) = {1})
12	11	iuneq1d 4982	. . . . . . . . 9 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ {1} (𝑄‘𝑘))
13		1ex 11231	. . . . . . . . . 10 ⊢ 1 ∈ V
14		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑄‘𝑘) = (𝑄‘1))
15	13, 14	iunxsn 5055	. . . . . . . . 9 ⊢ ∪ 𝑘 ∈ {1} (𝑄‘𝑘) = (𝑄‘1)
16	12, 15	eqtrdi 2813	. . . . . . . 8 ⊢ (𝑦 = 1 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = (𝑄‘1))
17		oveq1 7424	. . . . . . . . . . 11 ⊢ (𝑦 = 1 → (𝑦 / 𝑁) = (1 / 𝑁))
18	17	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝑦 = 1 → (0[,](𝑦 / 𝑁)) = (0[,](1 / 𝑁)))
19	18	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑦 = 1 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
20	19	oveq1d 7432	. . . . . . . 8 ⊢ (𝑦 = 1 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
21	16, 20	eleq12d 2856	. . . . . . 7 ⊢ (𝑦 = 1 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ (𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶)))
22	16	coeq2d 5846	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ (𝑄‘1)))
23	18	reseq2d 5976	. . . . . . . 8 ⊢ (𝑦 = 1 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
24	22, 23	eqeq12d 2778	. . . . . . 7 ⊢ (𝑦 = 1 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁)))))
25	21, 24	anbi12d 644	. . . . . 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 2850	. . . . . 6 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ (1...𝑁) ↔ 𝑛 ∈ (1...𝑁)))
29		oveq2 7425	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (1...𝑦) = (1...𝑛))
30	29	iuneq1d 4982	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
31		oveq1 7424	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑛 → (𝑦 / 𝑁) = (𝑛 / 𝑁))
32	31	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝑦 = 𝑛 → (0[,](𝑦 / 𝑁)) = (0[,](𝑛 / 𝑁)))
33	32	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑦 = 𝑛 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
34	33	oveq1d 7432	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
35	30, 34	eleq12d 2856	. . . . . . 7 ⊢ (𝑦 = 𝑛 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶)))
36	30	coeq2d 5846	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)))
37	32	reseq2d 5976	. . . . . . . 8 ⊢ (𝑦 = 𝑛 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
38	36, 37	eqeq12d 2778	. . . . . . 7 ⊢ (𝑦 = 𝑛 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
39	35, 38	anbi12d 644	. . . . . 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 2850	. . . . . 6 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 ∈ (1...𝑁) ↔ (𝑛 + 1) ∈ (1...𝑁)))
43		oveq2 7425	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (1...𝑦) = (1...(𝑛 + 1)))
44	43	iuneq1d 4982	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
45		oveq1 7424	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑛 + 1) → (𝑦 / 𝑁) = ((𝑛 + 1) / 𝑁))
46	45	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝑦 = (𝑛 + 1) → (0[,](𝑦 / 𝑁)) = (0[,]((𝑛 + 1) / 𝑁)))
47	46	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑦 = (𝑛 + 1) → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
48	47	oveq1d 7432	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
49	44, 48	eleq12d 2856	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶)))
50	44	coeq2d 5846	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
51	46	reseq2d 5976	. . . . . . . 8 ⊢ (𝑦 = (𝑛 + 1) → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
52	50, 51	eqeq12d 2778	. . . . . . 7 ⊢ (𝑦 = (𝑛 + 1) → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
53	49, 52	anbi12d 644	. . . . . 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 2850	. . . . . 6 ⊢ (𝑦 = 𝑁 → (𝑦 ∈ (1...𝑁) ↔ 𝑁 ∈ (1...𝑁)))
57		oveq2 7425	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (1...𝑦) = (1...𝑁))
58	57	iuneq1d 4982	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘))
59		cvmliftlem.k	. . . . . . . . 9 ⊢ 𝐾 = ∪ 𝑘 ∈ (1...𝑁)(𝑄‘𝑘)
60	58, 59	eqtr4di 2815	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) = 𝐾)
61		oveq1 7424	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑁 → (𝑦 / 𝑁) = (𝑁 / 𝑁))
62	61	oveq2d 7433	. . . . . . . . . 10 ⊢ (𝑦 = 𝑁 → (0[,](𝑦 / 𝑁)) = (0[,](𝑁 / 𝑁)))
63	62	oveq2d 7433	. . . . . . . . 9 ⊢ (𝑦 = 𝑁 → (𝐿 ↾_t (0[,](𝑦 / 𝑁))) = (𝐿 ↾_t (0[,](𝑁 / 𝑁))))
64	63	oveq1d 7432	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶))
65	60, 64	eleq12d 2856	. . . . . . 7 ⊢ (𝑦 = 𝑁 → (∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑦 / 𝑁))) Cn 𝐶) ↔ 𝐾 ∈ ((𝐿 ↾_t (0[,](𝑁 / 𝑁))) Cn 𝐶)))
66	60	coeq2d 5846	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐹 ∘ 𝐾))
67	62	reseq2d 5976	. . . . . . . 8 ⊢ (𝑦 = 𝑁 → (𝐺 ↾ (0[,](𝑦 / 𝑁))) = (𝐺 ↾ (0[,](𝑁 / 𝑁))))
68	66, 67	eqeq12d 2778	. . . . . . 7 ⊢ (𝑦 = 𝑁 → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑦)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑦 / 𝑁))) ↔ (𝐹 ∘ 𝐾) = (𝐺 ↾ (0[,](𝑁 / 𝑁)))))
69	65, 68	anbi12d 644	. . . . . 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 13589	. . . . . . . . 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 2762	. . . . . . . . 9 ⊢ (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (((1 − 1) / 𝑁)[,](1 / 𝑁))
86	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem8 35879	. . . . . . . 8 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
87	73, 86	mpdan 700	. . . . . . 7 ⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶))
88		1m1e0 12341	. . . . . . . . . . . 12 ⊢ (1 − 1) = 0
89	88	oveq1i 7427	. . . . . . . . . . 11 ⊢ ((1 − 1) / 𝑁) = (0 / 𝑁)
90	1	nncnd 12277	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
91	1	nnne0d 12314	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ≠ 0)
92	90, 91	div0d 12018	. . . . . . . . . . 11 ⊢ (𝜑 → (0 / 𝑁) = 0)
93	89, 92	eqtrid 2809	. . . . . . . . . 10 ⊢ (𝜑 → ((1 − 1) / 𝑁) = 0)
94	93	oveq1d 7432	. . . . . . . . 9 ⊢ (𝜑 → (((1 − 1) / 𝑁)[,](1 / 𝑁)) = (0[,](1 / 𝑁)))
95	94	oveq2d 7433	. . . . . . . 8 ⊢ (𝜑 → (𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐿 ↾_t (0[,](1 / 𝑁))))
96	95	oveq1d 7432	. . . . . . 7 ⊢ (𝜑 → ((𝐿 ↾_t (((1 − 1) / 𝑁)[,](1 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
97	87, 96	eleqtrd 2864	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) ∈ ((𝐿 ↾_t (0[,](1 / 𝑁))) Cn 𝐶))
98		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → 1 ∈ (1...𝑁))
99	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem7 35878	. . . . . . . . . 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 35877	. . . . . . . . 9 ⊢ ((𝜑 ∧ 1 ∈ (1...𝑁)) → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
101	73, 100	mpdan 700	. . . . . . . 8 ⊢ (𝜑 → ((𝑄‘1):(((1 − 1) / 𝑁)[,](1 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁)))))
102	101	simprd 501	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))))
103	94	reseq2d 5976	. . . . . . 7 ⊢ (𝜑 → (𝐺 ↾ (((1 − 1) / 𝑁)[,](1 / 𝑁))) = (𝐺 ↾ (0[,](1 / 𝑁))))
104	102, 103	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → (𝐹 ∘ (𝑄‘1)) = (𝐺 ↾ (0[,](1 / 𝑁))))
105	97, 104	jca 521	. . . . 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 12931	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
108	107	biimpi 219	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ (ℤ_≥‘1))
109	108	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
110		peano2fzr 13595	. . . . . . . 8 ⊢ ((𝑛 ∈ (ℤ_≥‘1) ∧ (𝑛 + 1) ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
111	110	ex 418	. . . . . . 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 2762	. . . . . . . . 9 ⊢ ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))
116		0re 11238	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
117	114	simplbi 502	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
118	117	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)))
119	118	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ (1...𝑁))
120		elfznn 13612	. . . . . . . . . . . . . 14 ⊢ ((𝑛 + 1) ∈ (1...𝑁) → (𝑛 + 1) ∈ ℕ)
121	119, 120	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℕ)
122	121	nnred 12276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 + 1) ∈ ℝ)
123	1	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℕ)
124	122, 123	nndivred 12318	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ)
125		iccssre 13486	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
126	116, 124, 125	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ)
127	117	simpld 500	. . . . . . . . . . . . . . 15 ⊢ (𝜒 → 𝑛 ∈ ℕ)
128	127	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ)
129	128	nnred 12276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℝ)
130	129, 123	nndivred 12318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ)
131		icccld 24998	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
132	116, 130, 131	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
133	83	fveq2i 6885	. . . . . . . . . . 11 ⊢ (Clsd‘𝐿) = (Clsd‘(topGen‘ran (,)))
134	132, 133	eleqtrrdi 2873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ∈ (Clsd‘𝐿))
135		ssun1 4127	. . . . . . . . . . 11 ⊢ (0[,](𝑛 / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
136	116	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ)
137	128	nnnn0d 12593	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℕ₀)
138	137	nn0ge0d 12596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ 𝑛)
139	123	nnred 12276	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 𝑁 ∈ ℝ)
140	123	nngt0d 12313	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → 0 < 𝑁)
141		divge0 12112	. . . . . . . . . . . . . 14 ⊢ (((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → 0 ≤ (𝑛 / 𝑁))
142	129, 138, 139, 140, 141	syl22anc 852	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → 0 ≤ (𝑛 / 𝑁))
143	129	ltp1d 12173	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 < (𝑛 + 1))
144		ltdiv1 12107	. . . . . . . . . . . . . . . 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 11386	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))
148		elicc2 13468	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
149	116, 124, 148	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)) ↔ ((𝑛 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑛 / 𝑁) ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁))))
150	130, 142, 147, 149	mpbir3and 1361	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,]((𝑛 + 1) / 𝑁)))
151		iccsplit 13542	. . . . . . . . . . . 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 3977	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
154		uniretop 24994	. . . . . . . . . . . 12 ⊢ ℝ = ∪ (topGen‘ran (,))
155	83	unieqi 4882	. . . . . . . . . . . 12 ⊢ ∪ 𝐿 = ∪ (topGen‘ran (,))
156	154, 155	eqtr4i 2788	. . . . . . . . . . 11 ⊢ ℝ = ∪ 𝐿
157	156	restcldi 23404	. . . . . . . . . 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 24998	. . . . . . . . . . . 12 ⊢ (((𝑛 / 𝑁) ∈ ℝ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
160	130, 124, 159	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘(topGen‘ran (,))))
161	160, 133	eleqtrrdi 2873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∈ (Clsd‘𝐿))
162		ssun2 4128	. . . . . . . . . . 11 ⊢ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
163	162, 152	sseqtrrid 3977	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ⊆ (0[,]((𝑛 + 1) / 𝑁)))
164	156	restcldi 23404	. . . . . . . . . 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 24993	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) ∈ Top
167	83, 166	eqeltri 2858	. . . . . . . . . . 11 ⊢ 𝐿 ∈ Top
168	156	restuni 23393	. . . . . . . . . . 11 ⊢ ((𝐿 ∈ Top ∧ (0[,]((𝑛 + 1) / 𝑁)) ⊆ ℝ) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
169	167, 126, 168	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
170	152, 169	eqtr3d 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = ∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))))
171	114	simprbi 503	. . . . . . . . . . . . . . . 16 ⊢ (𝜒 → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
172	171	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))
173	172	simpld 500	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
174		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))
175	174, 75	cnf 23477	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
176	173, 175	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵)
177		iccssre 13486	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ (𝑛 / 𝑁) ∈ ℝ) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
178	116, 130, 177	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) ⊆ ℝ)
179	156	restuni 23393	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ Top ∧ (0[,](𝑛 / 𝑁)) ⊆ ℝ) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
180	167, 178, 179	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (0[,](𝑛 / 𝑁)) = ∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁))))
181	180	feq2d 6690	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,](𝑛 / 𝑁)))⟶𝐵))
182	176, 181	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘):(0[,](𝑛 / 𝑁))⟶𝐵)
183		eqid 2762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))
184		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑛 + 1) ∈ (1...𝑁))
185	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem7 35878	. . . . . . . . . . . . . . . 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 35877	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
187	119, 186	syldan 603	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
188	187	simpld 500	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
189	128	nncnd 12277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ ℂ)
190		ax-1cn 11186	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
191		pncan 11491	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
192	189, 190, 191	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) − 1) = 𝑛)
193	192	oveq1d 7432	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (((𝑛 + 1) − 1) / 𝑁) = (𝑛 / 𝑁))
194	193	oveq1d 7432	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁)) = ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
195	194	feq2d 6690	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)):((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵 ↔ (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵))
196	188, 195	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)):((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))⟶𝐵)
197	176	ffund 6711	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
198	128, 108	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (ℤ_≥‘1))
199		eluzfz2 13590	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ (1...𝑛))
200	198, 199	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑛))
201		fveq2 6882	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑛 → (𝑄‘𝑘) = (𝑄‘𝑛))
202	201	ssiun2s 5011	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑛) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
203	200, 202	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
204		peano2rem 11553	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
205	129, 204	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) ∈ ℝ)
206	205, 123	nndivred 12318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ)
207	206	rexrd 11287	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ∈ ℝ^*)
208	130	rexrd 11287	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ℝ^*)
209	129	ltm1d 12175	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 − 1) < 𝑛)
210		ltdiv1 12107	. . . . . . . . . . . . . . . . . . . . . . 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 11386	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁))
214		ubicc2 13522	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑛 − 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 − 1) / 𝑁) ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
215	207, 208, 213, 214	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
216	198, 119, 110	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝜒) → 𝑛 ∈ (1...𝑁))
217		eqid 2762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))
218		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ (1...𝑁))
219	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217	cvmliftlem7 35878	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘(𝑛 − 1))‘((𝑛 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑛 − 1) / 𝑁))}))
220	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 217, 218, 219	cvmliftlem6 35877	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
221	216, 220	syldan 603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑛)) = (𝐺 ↾ (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))))
222	221	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘𝑛):(((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁))⟶𝐵)
223	222	fdmd 6717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝜒) → dom (𝑄‘𝑛) = (((𝑛 − 1) / 𝑁)[,](𝑛 / 𝑁)))
224	215, 223	eleqtrrd 2865	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛))
225		funssfv 6903	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑄‘𝑛) ⊆ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∧ (𝑛 / 𝑁) ∈ dom (𝑄‘𝑛)) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
226	197, 203, 224, 225	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
227	192	fveq2d 6886	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘((𝑛 + 1) − 1)) = (𝑄‘𝑛))
228	227, 193	fveq12d 6889	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘𝑛)‘(𝑛 / 𝑁)))
229	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84	cvmliftlem9 35880	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
230	119, 229	syldan 603	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)))
231	193	fveq2d 6886	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
232	230, 231	eqtr3d 2799	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘((𝑛 + 1) − 1))‘(((𝑛 + 1) − 1) / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
233	226, 228, 232	3eqtr2d 2803	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁)) = ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁)))
234	233	opeq2d 4843	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩ = ⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩)
235	234	sneqd 4599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩} = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
236	182	ffnd 6707	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)))
237		0xr 11284	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ^*
238	237	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → 0 ∈ ℝ^*)
239		ubicc2 13522	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 0 ≤ (𝑛 / 𝑁)) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
240	238, 208, 142, 239	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁)))
241		fnressn 7159	. . . . . . . . . . . . . . 15 ⊢ ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) Fn (0[,](𝑛 / 𝑁)) ∧ (𝑛 / 𝑁) ∈ (0[,](𝑛 / 𝑁))) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
242	236, 240, 241	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)‘(𝑛 / 𝑁))⟩})
243	196	ffnd 6707	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
244	124	rexrd 11287	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 + 1) / 𝑁) ∈ ℝ^*)
245		lbicc2 13521	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^* ∧ (𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁)) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
246	208, 244, 147, 245	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))
247		fnressn 7159	. . . . . . . . . . . . . . 15 ⊢ (((𝑄‘(𝑛 + 1)) Fn ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)) ∧ (𝑛 / 𝑁) ∈ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
248	243, 246, 247	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}) = {⟨(𝑛 / 𝑁), ((𝑄‘(𝑛 + 1))‘(𝑛 / 𝑁))⟩})
249	235, 242, 248	3eqtr4d 2807	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
250		df-icc 13409	. . . . . . . . . . . . . . . . 17 ⊢ [,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)})
251		xrmaxle 13239	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ 𝑧 ∈ ℝ^*) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) ≤ 𝑧 ↔ (0 ≤ 𝑧 ∧ (𝑛 / 𝑁) ≤ 𝑧)))
252		xrlemin 13240	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^* ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^*) → (𝑧 ≤ if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) ↔ (𝑧 ≤ (𝑛 / 𝑁) ∧ 𝑧 ≤ ((𝑛 + 1) / 𝑁))))
253	250, 251, 252	ixxin 13419	. . . . . . . . . . . . . . . 16 ⊢ (((0 ∈ ℝ^* ∧ (𝑛 / 𝑁) ∈ ℝ^) ∧ ((𝑛 / 𝑁) ∈ ℝ^ ∧ ((𝑛 + 1) / 𝑁) ∈ ℝ^*)) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
254	238, 208, 208, 244, 253	syl22anc 852	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))))
255	142	iftrued 4493	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0) = (𝑛 / 𝑁))
256	147	iftrued 4493	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝜒) → if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁)) = (𝑛 / 𝑁))
257	255, 256	oveq12d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → (if(0 ≤ (𝑛 / 𝑁), (𝑛 / 𝑁), 0)[,]if((𝑛 / 𝑁) ≤ ((𝑛 + 1) / 𝑁), (𝑛 / 𝑁), ((𝑛 + 1) / 𝑁))) = ((𝑛 / 𝑁)[,](𝑛 / 𝑁)))
258		iccid 13447	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 / 𝑁) ∈ ℝ^* → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
259	208, 258	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝜒) → ((𝑛 / 𝑁)[,](𝑛 / 𝑁)) = {(𝑛 / 𝑁)})
260	254, 257, 259	3eqtrd 2801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = {(𝑛 / 𝑁)})
261	260	reseq2d 5976	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ {(𝑛 / 𝑁)}))
262	260	reseq2d 5976	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ {(𝑛 / 𝑁)}))
263	249, 261, 262	3eqtr4d 2807	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝑄‘(𝑛 + 1)) ↾ ((0[,](𝑛 / 𝑁)) ∩ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
264		fresaun 6750	. . . . . . . . . . . 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 13630	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘1) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
267	198, 266	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜒) → (1...(𝑛 + 1)) = ((1...𝑛) ∪ {(𝑛 + 1)}))
268	267	iuneq1d 4982	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) = ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘))
269		iunxun 5058	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘))
270		ovex 7450	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 + 1) ∈ V
271		fveq2 6882	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑛 + 1) → (𝑄‘𝑘) = (𝑄‘(𝑛 + 1)))
272	270, 271	iunxsn 5055	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘) = (𝑄‘(𝑛 + 1))
273	272	uneq2i 4115	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑛 + 1)} (𝑄‘𝑘)) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
274	269, 273	eqtri 2785	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ((1...𝑛) ∪ {(𝑛 + 1)})(𝑄‘𝑘) = (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))
275	268, 274	eqtr2di 2814	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) = ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘))
276	275	feq1d 6688	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
277	265, 276	mpbid 235	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
278	170	feq2d 6690	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))⟶𝐵 ↔ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵))
279	277, 278	mpbid 235	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘):∪ (𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁)))⟶𝐵)
280	275	reseq1d 5975	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ (0[,](𝑛 / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))))
281		fresaunres1 6752	. . . . . . . . . . . 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 2799	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ (0[,](𝑛 / 𝑁))) = ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘))
284	167	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → 𝐿 ∈ Top)
285		ovex 7450	. . . . . . . . . . . . 13 ⊢ (0[,]((𝑛 + 1) / 𝑁)) ∈ V
286	285	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (0[,]((𝑛 + 1) / 𝑁)) ∈ V)
287		restabs 23396	. . . . . . . . . . . 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 7432	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶))
290	173, 283, 289	3eltr4d 2877	. . . . . . . . 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 35879	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 + 1) ∈ (1...𝑁)) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
292	119, 291	syldan 603	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
293	194	oveq2d 7433	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
294	293	oveq1d 7432	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((𝐿 ↾_t ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
295	292, 294	eleqtrd 2864	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (𝑄‘(𝑛 + 1)) ∈ ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
296	275	reseq1d 5975	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1))) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
297		fresaunres2 6751	. . . . . . . . . . . 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 2799	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝑄‘(𝑛 + 1)))
300		restabs 23396	. . . . . . . . . . . 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 7432	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) = ((𝐿 ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
303	295, 299, 302	3eltr4d 2877	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) ∈ (((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) ↾_t ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
304	115, 75, 158, 165, 170, 279, 290, 303	paste 23525	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶))
305	152	reseq2d 5976	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
306	172	simprd 501	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁))))
307	187	simprd 501	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))))
308	194	reseq2d 5976	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜒) → (𝐺 ↾ ((((𝑛 + 1) − 1) / 𝑁)[,]((𝑛 + 1) / 𝑁))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
309	307, 308	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (𝑄‘(𝑛 + 1))) = (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
310	306, 309	uneq12d 4119	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝜒) → ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
311		coundi 6247	. . . . . . . . . 10 ⊢ (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = ((𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) ∪ (𝐹 ∘ (𝑄‘(𝑛 + 1))))
312		resundi 5990	. . . . . . . . . 10 ⊢ (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))) = ((𝐺 ↾ (0[,](𝑛 / 𝑁))) ∪ (𝐺 ↾ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁))))
313	310, 311, 312	3eqtr4g 2822	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐺 ↾ ((0[,](𝑛 / 𝑁)) ∪ ((𝑛 / 𝑁)[,]((𝑛 + 1) / 𝑁)))))
314	275	coeq2d 5846	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∪ (𝑄‘(𝑛 + 1)))) = (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)))
315	305, 313, 314	3eqtr2rd 2804	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝜒) → (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))
316	304, 315	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜒) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
317	114, 316	sylan2br 607	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁)) ∧ (∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁)))))
318	317	expr 462	. . . . 5 ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ (1...𝑁))) → ((∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,](𝑛 / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...𝑛)(𝑄‘𝑘)) = (𝐺 ↾ (0[,](𝑛 / 𝑁)))) → (∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘) ∈ ((𝐿 ↾_t (0[,]((𝑛 + 1) / 𝑁))) Cn 𝐶) ∧ (𝐹 ∘ ∪ 𝑘 ∈ (1...(𝑛 + 1))(𝑄‘𝑘)) = (𝐺 ↾ (0[,]((𝑛 + 1) / 𝑁))))))
319	113, 318	animpimp2impd 860	. . . 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 12279	. . 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

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∀wral 3078 {crab 3414 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 ifcif 4485 𝒫 cpw 4560 {csn 4587 ⟨cop 4593 ∪ cuni 4870 ∪ ciun 4954 class class class wbr 5107 ↦ cmpt 5190 I cid 5553 × cxp 5657 ^◡ccnv 5658 dom cdm 5659 ran crn 5660 ↾ cres 5661 “ cima 5662 ∘ ccom 5663 Fun wfun 6531 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 ℩crio 7373 (class class class)co 7417 ∈ cmpo 7419 1^st c1st 7988 2^nd c2nd 7989 ℂcc 11126 ℝcr 11127 0cc0 11128 1c1 11129 + caddc 11131 ℝ^*cxr 11270 < clt 11271 ≤ cle 11272 − cmin 11469 / cdiv 11899 ℕcn 12261 ℤcz 12619 ℤ_≥cuz 12891 (,)cioo 13402 [,]cicc 13405 ...cfz 13565 seqcseq 14069 ↾_t crest 17511 topGenctg 17528 Topctop 23124 Clsdccld 23247 Cn ccn 23455 Homeochmeo 23985 IIcii 25109 CovMap ccvm 35842

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-er 8700 df-map 8832 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fi 9385 df-sup 9416 df-inf 9417 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-n0 12533 df-z 12620 df-uz 12892 df-q 13002 df-rp 13047 df-xneg 13167 df-xadd 13168 df-xmul 13169 df-ioo 13406 df-icc 13409 df-fz 13566 df-seq 14070 df-exp 14130 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-rest 17513 df-topgen 17534 df-psmet 21583 df-xmet 21584 df-met 21585 df-bl 21586 df-mopn 21587 df-top 23125 df-topon 23142 df-bases 23177 df-cld 23250 df-cn 23458 df-hmeo 23987 df-ii 25111 df-cvm 35843

This theorem is used by: cvmliftlem11 35882

W3C validator