cvmliftlem15 - Mathbox for Mario Carneiro

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

Theorem cvmliftlem15 35520

Description: Lemma for cvmlift 35521. Discharge the assumptions of cvmliftlem14 35519. The set of all open subsets 𝑢 of the unit interval such that 𝐺 “ 𝑢 is contained in an even covering of some open set in 𝐽 is a cover of II by the definition of a covering map, so by the Lebesgue number lemma lebnumii 24938, there is a subdivision of the closed unit interval into 𝑁 equal parts such that each part is entirely contained within one such open set of 𝐽. Then using finite choice ac6sfi 9198 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 35519. (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))

**Assertion**
Ref	Expression
cvmliftlem15	⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))

Distinct variable groups: 𝑣,𝐵 𝑓,𝑘,𝑠,𝑢,𝑣,𝐹 𝑃,𝑓,𝑘,𝑢,𝑣 𝐶,𝑓,𝑘,𝑠,𝑢,𝑣 𝜑,𝑓,𝑠 𝑆,𝑓,𝑘,𝑠,𝑢,𝑣 𝑓,𝐺,𝑘,𝑠,𝑢,𝑣 𝑓,𝐽,𝑘,𝑠,𝑢,𝑣 Allowed substitution hints: 𝜑(𝑣,𝑢,𝑘) 𝐵(𝑢,𝑓,𝑘,𝑠) 𝑃(𝑠) 𝑋(𝑣,𝑢,𝑓,𝑘,𝑠)

Proof of Theorem cvmliftlem15 Dummy variables 𝑏 𝑦 𝑧 𝑎 𝑐 𝑔 𝑗 𝑚 𝑛 𝑡 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssrab2 4034	. . 3 ⊢ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ II
2		cvmliftlem.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))
3	2	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝐺 ∈ (II Cn 𝐽))
4		simprl 771	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝑗 ∈ 𝐽)
5		cnima 23226	. . . . . . . . . 10 ⊢ ((𝐺 ∈ (II Cn 𝐽) ∧ 𝑗 ∈ 𝐽) → (^◡𝐺 “ 𝑗) ∈ II)
6	3, 4, 5	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (^◡𝐺 “ 𝑗) ∈ II)
7		simplr 769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝑥 ∈ (0[,]1))
8		simprrl 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝐺‘𝑥) ∈ 𝑗)
9		iiuni 24847	. . . . . . . . . . . . . 14 ⊢ (0[,]1) = ∪ II
10		cvmliftlem.x	. . . . . . . . . . . . . 14 ⊢ 𝑋 = ∪ 𝐽
11	9, 10	cnf 23207	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶𝑋)
12	2, 11	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺:(0[,]1)⟶𝑋)
13	12	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝐺:(0[,]1)⟶𝑋)
14		ffn 6672	. . . . . . . . . . 11 ⊢ (𝐺:(0[,]1)⟶𝑋 → 𝐺 Fn (0[,]1))
15		elpreima 7014	. . . . . . . . . . 11 ⊢ (𝐺 Fn (0[,]1) → (𝑥 ∈ (^◡𝐺 “ 𝑗) ↔ (𝑥 ∈ (0[,]1) ∧ (𝐺‘𝑥) ∈ 𝑗)))
16	13, 14, 15	3syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝑥 ∈ (^◡𝐺 “ 𝑗) ↔ (𝑥 ∈ (0[,]1) ∧ (𝐺‘𝑥) ∈ 𝑗)))
17	7, 8, 16	mpbir2and 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → 𝑥 ∈ (^◡𝐺 “ 𝑗))
18		simprrr 782	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝑆‘𝑗) ≠ ∅)
19		ffun 6675	. . . . . . . . . . . . 13 ⊢ (𝐺:(0[,]1)⟶𝑋 → Fun 𝐺)
20		funimacnv 6583	. . . . . . . . . . . . 13 ⊢ (Fun 𝐺 → (𝐺 “ (^◡𝐺 “ 𝑗)) = (𝑗 ∩ ran 𝐺))
21	13, 19, 20	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝐺 “ (^◡𝐺 “ 𝑗)) = (𝑗 ∩ ran 𝐺))
22		inss1 4191	. . . . . . . . . . . 12 ⊢ (𝑗 ∩ ran 𝐺) ⊆ 𝑗
23	21, 22	eqsstrdi 3980	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → (𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
24	23	ralrimivw 3134	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → ∀𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
25		r19.2z 4454	. . . . . . . . . 10 ⊢ (((𝑆‘𝑗) ≠ ∅ ∧ ∀𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗) → ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
26	18, 24, 25	syl2anc 585	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)
27		eleq2 2826	. . . . . . . . . . 11 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → (𝑥 ∈ 𝑢 ↔ 𝑥 ∈ (^◡𝐺 “ 𝑗)))
28		imaeq2 6025	. . . . . . . . . . . . 13 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → (𝐺 “ 𝑢) = (𝐺 “ (^◡𝐺 “ 𝑗)))
29	28	sseq1d 3967	. . . . . . . . . . . 12 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → ((𝐺 “ 𝑢) ⊆ 𝑗 ↔ (𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗))
30	29	rexbidv 3162	. . . . . . . . . . 11 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → (∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗 ↔ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗))
31	27, 30	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑢 = (^◡𝐺 “ 𝑗) → ((𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ (𝑥 ∈ (^◡𝐺 “ 𝑗) ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)))
32	31	rspcev 3578	. . . . . . . . 9 ⊢ (((^◡𝐺 “ 𝑗) ∈ II ∧ (𝑥 ∈ (^◡𝐺 “ 𝑗) ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ (^◡𝐺 “ 𝑗)) ⊆ 𝑗)) → ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
33	6, 17, 26, 32	syl12anc 837	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (0[,]1)) ∧ (𝑗 ∈ 𝐽 ∧ ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))) → ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
34		cvmliftlem.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
35	34	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
36	12	ffvelcdmda 7040	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → (𝐺‘𝑥) ∈ 𝑋)
37		cvmliftlem.1	. . . . . . . . . 10 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
38	37, 10	cvmcov 35485	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺‘𝑥) ∈ 𝑋) → ∃𝑗 ∈ 𝐽 ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))
39	35, 36, 38	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ∃𝑗 ∈ 𝐽 ((𝐺‘𝑥) ∈ 𝑗 ∧ (𝑆‘𝑗) ≠ ∅))
40	33, 39	reximddv 3154	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → ∃𝑗 ∈ 𝐽 ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
41		r19.42v 3170	. . . . . . . . 9 ⊢ (∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ (𝑥 ∈ 𝑢 ∧ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
42	41	rexbii 3085	. . . . . . . 8 ⊢ (∃𝑢 ∈ II ∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
43		rexcom 3267	. . . . . . . 8 ⊢ (∃𝑗 ∈ 𝐽 ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ ∃𝑢 ∈ II ∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
44		elunirab 4880	. . . . . . . 8 ⊢ (𝑥 ∈ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ↔ ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗))
45	42, 43, 44	3bitr4i 303	. . . . . . 7 ⊢ (∃𝑗 ∈ 𝐽 ∃𝑢 ∈ II (𝑥 ∈ 𝑢 ∧ ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗) ↔ 𝑥 ∈ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
46	40, 45	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]1)) → 𝑥 ∈ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
47	46	ex 412	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (0[,]1) → 𝑥 ∈ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗}))
48	47	ssrdv 3941	. . . 4 ⊢ (𝜑 → (0[,]1) ⊆ ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
49		uniss 4873	. . . . . 6 ⊢ ({𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ II → ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ ∪ II)
50	1, 49	mp1i 13	. . . . 5 ⊢ (𝜑 → ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ ∪ II)
51	50, 9	sseqtrrdi 3977	. . . 4 ⊢ (𝜑 → ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ (0[,]1))
52	48, 51	eqssd 3953	. . 3 ⊢ (𝜑 → (0[,]1) = ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗})
53		lebnumii 24938	. . 3 ⊢ (({𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} ⊆ II ∧ (0[,]1) = ∪ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗}) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣)
54	1, 52, 53	sylancr 588	. 2 ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣)
55		fzfi 13909	. . . . 5 ⊢ (1...𝑛) ∈ Fin
56		imaeq2 6025	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (𝐺 “ 𝑢) = (𝐺 “ 𝑣))
57	56	sseq1d 3967	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → ((𝐺 “ 𝑢) ⊆ 𝑗 ↔ (𝐺 “ 𝑣) ⊆ 𝑗))
58	57	2rexbidv 3203	. . . . . . . 8 ⊢ (𝑢 = 𝑣 → (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗 ↔ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗))
59	58	rexrab 3656	. . . . . . 7 ⊢ (∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 ↔ ∃𝑣 ∈ II (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣))
60		vex 3446	. . . . . . . . . . . . 13 ⊢ 𝑗 ∈ V
61		vex 3446	. . . . . . . . . . . . 13 ⊢ 𝑠 ∈ V
62	60, 61	op1std 7955	. . . . . . . . . . . 12 ⊢ (𝑢 = ⟨𝑗, 𝑠⟩ → (1^st ‘𝑢) = 𝑗)
63	62	sseq2d 3968	. . . . . . . . . . 11 ⊢ (𝑢 = ⟨𝑗, 𝑠⟩ → ((𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) ↔ (𝐺 “ 𝑣) ⊆ 𝑗))
64	63	rexiunxp 5799	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) ↔ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗)
65		imass2 6071	. . . . . . . . . . . 12 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (𝐺 “ 𝑣))
66		sstr2 3942	. . . . . . . . . . . 12 ⊢ ((𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (𝐺 “ 𝑣) → ((𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
67	65, 66	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ((𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) → (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
68	67	reximdv 3153	. . . . . . . . . 10 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ 𝑣) ⊆ (1^st ‘𝑢) → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
69	64, 68	biimtrrid 243	. . . . . . . . 9 ⊢ ((((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)))
70	69	impcom 407	. . . . . . . 8 ⊢ ((∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣) → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
71	70	rexlimivw 3135	. . . . . . 7 ⊢ (∃𝑣 ∈ II (∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑣) ⊆ 𝑗 ∧ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣) → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
72	59, 71	sylbi 217	. . . . . 6 ⊢ (∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
73	72	ralimi 3075	. . . . 5 ⊢ (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢))
74		fveq2 6844	. . . . . . 7 ⊢ (𝑢 = (𝑔‘𝑘) → (1^st ‘𝑢) = (1^st ‘(𝑔‘𝑘)))
75	74	sseq2d 3968	. . . . . 6 ⊢ (𝑢 = (𝑔‘𝑘) → ((𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢) ↔ (𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))))
76	75	ac6sfi 9198	. . . . 5 ⊢ (((1...𝑛) ∈ Fin ∧ ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗))(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘𝑢)) → ∃𝑔(𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))))
77	55, 73, 76	sylancr 588	. . . 4 ⊢ (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃𝑔(𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))))
78		cvmliftlem.b	. . . . . . 7 ⊢ 𝐵 = ∪ 𝐶
79	34	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝐹 ∈ (𝐶 CovMap 𝐽))
80	2	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝐺 ∈ (II Cn 𝐽))
81		cvmliftlem.p	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
82	81	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝑃 ∈ 𝐵)
83		cvmliftlem.e	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))
84	83	ad2antrr 727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → (𝐹‘𝑃) = (𝐺‘0))
85		simplr 769	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝑛 ∈ ℕ)
86		simprl 771	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
87		sneq 4592	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑎 → {𝑗} = {𝑎})
88		fveq2 6844	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑎 → (𝑆‘𝑗) = (𝑆‘𝑎))
89	87, 88	xpeq12d 5665	. . . . . . . . . 10 ⊢ (𝑗 = 𝑎 → ({𝑗} × (𝑆‘𝑗)) = ({𝑎} × (𝑆‘𝑎)))
90	89	cbviunv 4996	. . . . . . . . 9 ⊢ ∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) = ∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎))
91		feq3 6652	. . . . . . . . 9 ⊢ (∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) = ∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎)) → (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ↔ 𝑔:(1...𝑛)⟶∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎))))
92	90, 91	ax-mp 5	. . . . . . . 8 ⊢ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ↔ 𝑔:(1...𝑛)⟶∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎)))
93	86, 92	sylib 218	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → 𝑔:(1...𝑛)⟶∪ 𝑎 ∈ 𝐽 ({𝑎} × (𝑆‘𝑎)))
94		simprr 773	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))
95		eqid 2737	. . . . . . 7 ⊢ (topGen‘ran (,)) = (topGen‘ran (,))
96		2fveq3 6849	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑧 → (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)) = (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧)))
97	96	cbvmptv 5204	. . . . . . . . . 10 ⊢ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧)))
98		eleq2 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑏 → ((𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐 ↔ (𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
99	98	cbvriotavw 7337	. . . . . . . . . . . . . . 15 ⊢ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)
100		fveq1 6843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑥 → (𝑦‘((𝑤 − 1) / 𝑛)) = (𝑥‘((𝑤 − 1) / 𝑛)))
101	100	eleq1d 2822	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏 ↔ (𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
102	101	riotabidv 7329	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑏) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
103	99, 102	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))
104	103	reseq2d 5948	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐)) = (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)))
105	104	cnveqd 5834	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐)) = ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)))
106	105	fveq1d 6846	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧)) = (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))
107	106	mpteq2dv 5194	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑧))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
108	97, 107	eqtrid 2784	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡))) = (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
109		oveq1 7377	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑚 → (𝑤 − 1) = (𝑚 − 1))
110	109	oveq1d 7385	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑚 → ((𝑤 − 1) / 𝑛) = ((𝑚 − 1) / 𝑛))
111		oveq1 7377	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑚 → (𝑤 / 𝑛) = (𝑚 / 𝑛))
112	110, 111	oveq12d 7388	. . . . . . . . . 10 ⊢ (𝑤 = 𝑚 → (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) = (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)))
113		2fveq3 6849	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑚 → (2^nd ‘(𝑔‘𝑤)) = (2^nd ‘(𝑔‘𝑚)))
114	110	fveq2d 6848	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑚 → (𝑥‘((𝑤 − 1) / 𝑛)) = (𝑥‘((𝑚 − 1) / 𝑛)))
115	114	eleq1d 2822	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑚 → ((𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏 ↔ (𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))
116	113, 115	riotaeqbidv 7330	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑚 → (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏) = (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))
117	116	reseq2d 5948	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑚 → (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)) = (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏)))
118	117	cnveqd 5834	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑚 → ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏)) = ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏)))
119	118	fveq1d 6846	. . . . . . . . . 10 ⊢ (𝑤 = 𝑚 → (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)) = (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))
120	112, 119	mpteq12dv 5187	. . . . . . . . 9 ⊢ (𝑤 = 𝑚 → (𝑧 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑤))(𝑥‘((𝑤 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))) = (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
121	108, 120	cbvmpov 7465	. . . . . . . 8 ⊢ (𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))) = (𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧))))
122		seqeq2 13942	. . . . . . . 8 ⊢ ((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))) = (𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))) → seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})) = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})))
123	121, 122	ax-mp 5	. . . . . . 7 ⊢ seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩})) = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑛)[,](𝑚 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑔‘𝑚))(𝑥‘((𝑚 − 1) / 𝑛)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
124		eqid 2737	. . . . . . 7 ⊢ ∪ 𝑘 ∈ (1...𝑛)(seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))‘𝑘) = ∪ 𝑘 ∈ (1...𝑛)(seq0((𝑦 ∈ V, 𝑤 ∈ ℕ ↦ (𝑡 ∈ (((𝑤 − 1) / 𝑛)[,](𝑤 / 𝑛)) ↦ (^◡(𝐹 ↾ (℩𝑐 ∈ (2^nd ‘(𝑔‘𝑤))(𝑦‘((𝑤 − 1) / 𝑛)) ∈ 𝑐))‘(𝐺‘𝑡)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))‘𝑘)
125	37, 78, 10, 79, 80, 82, 84, 85, 93, 94, 95, 123, 124	cvmliftlem14 35519	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ (𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘)))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
126	125	ex 412	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
127	126	exlimdv 1935	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑔(𝑔:(1...𝑛)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)) ∧ ∀𝑘 ∈ (1...𝑛)(𝐺 “ (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛))) ⊆ (1^st ‘(𝑔‘𝑘))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
128	77, 127	syl5 34	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
129	128	rexlimdva 3139	. 2 ⊢ (𝜑 → (∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑣 ∈ {𝑢 ∈ II ∣ ∃𝑗 ∈ 𝐽 ∃𝑠 ∈ (𝑆‘𝑗)(𝐺 “ 𝑢) ⊆ 𝑗} (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑣 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)))
130	54, 129	mpd 15	1 ⊢ (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 ∃!wreu 3350 {crab 3401 Vcvv 3442 ∖ cdif 3900 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ∅c0 4287 𝒫 cpw 4556 {csn 4582 ⟨cop 4588 ∪ cuni 4865 ∪ ciun 4948 ↦ cmpt 5181 I cid 5528 × cxp 5632 ^◡ccnv 5633 ran crn 5635 ↾ cres 5636 “ cima 5637 ∘ ccom 5638 Fun wfun 6496 Fn wfn 6497 ⟶wf 6498 ‘cfv 6502 ℩crio 7326 (class class class)co 7370 ∈ cmpo 7372 1^st c1st 7943 2^nd c2nd 7944 Fincfn 8897 0cc0 11040 1c1 11041 − cmin 11378 / cdiv 11808 ℕcn 12159 (,)cioo 13275 [,]cicc 13278 ...cfz 13437 seqcseq 13938 ↾_t crest 17354 topGenctg 17371 Cn ccn 23185 Homeochmeo 23714 IIcii 24841 CovMap ccvm 35477

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-inf2 9564 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117 ax-pre-sup 11118 ax-addf 11119

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-se 5588 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-isom 6511 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-of 7634 df-om 7821 df-1st 7945 df-2nd 7946 df-supp 8115 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-1o 8409 df-2o 8410 df-er 8647 df-ec 8649 df-map 8779 df-ixp 8850 df-en 8898 df-dom 8899 df-sdom 8900 df-fin 8901 df-fsupp 9279 df-fi 9328 df-sup 9359 df-inf 9360 df-oi 9429 df-card 9865 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-div 11809 df-nn 12160 df-2 12222 df-3 12223 df-4 12224 df-5 12225 df-6 12226 df-7 12227 df-8 12228 df-9 12229 df-n0 12416 df-z 12503 df-dec 12622 df-uz 12766 df-q 12876 df-rp 12920 df-xneg 13040 df-xadd 13041 df-xmul 13042 df-ioo 13279 df-ico 13281 df-icc 13282 df-fz 13438 df-fzo 13585 df-fl 13726 df-seq 13939 df-exp 13999 df-hash 14268 df-cj 15036 df-re 15037 df-im 15038 df-sqrt 15172 df-abs 15173 df-clim 15425 df-sum 15624 df-struct 17088 df-sets 17105 df-slot 17123 df-ndx 17135 df-base 17151 df-ress 17172 df-plusg 17204 df-mulr 17205 df-starv 17206 df-sca 17207 df-vsca 17208 df-ip 17209 df-tset 17210 df-ple 17211 df-ds 17213 df-unif 17214 df-hom 17215 df-cco 17216 df-rest 17356 df-topn 17357 df-0g 17375 df-gsum 17376 df-topgen 17377 df-pt 17378 df-prds 17381 df-xrs 17437 df-qtop 17442 df-imas 17443 df-xps 17445 df-mre 17519 df-mrc 17520 df-acs 17522 df-mgm 18579 df-sgrp 18658 df-mnd 18674 df-submnd 18723 df-mulg 19015 df-cntz 19263 df-cmn 19728 df-psmet 21318 df-xmet 21319 df-met 21320 df-bl 21321 df-mopn 21322 df-cnfld 21327 df-top 22855 df-topon 22872 df-topsp 22894 df-bases 22907 df-cld 22980 df-ntr 22981 df-cls 22982 df-nei 23059 df-cn 23188 df-cnp 23189 df-cmp 23348 df-conn 23373 df-lly 23427 df-nlly 23428 df-tx 23523 df-hmeo 23716 df-xms 24281 df-ms 24282 df-tms 24283 df-ii 24843 df-cncf 24844 df-htpy 24942 df-phtpy 24943 df-phtpc 24964 df-pconn 35443 df-sconn 35444 df-cvm 35478

This theorem is referenced by: cvmlift 35521

W3C validator