cvmliftlem6 - Mathbox for Mario Carneiro

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

Theorem cvmliftlem6 34350

Description: Lemma for cvmlift 34359. Induction step for cvmliftlem7 34351. Assuming that 𝑄(𝑀 − 1) is defined at (𝑀 − 1) / 𝑁 and is a preimage of 𝐺((𝑀 − 1) / 𝑁), the next segment 𝑄(𝑀) is also defined and is a function on 𝑊 which is a lift 𝐺 for this segment. This follows explicitly from the definition 𝑄(𝑀) = ^◡(𝐹 ↾ 𝐼) ∘ 𝐺 since 𝐺 is in 1^st ‘(𝐹‘𝑀) for the entire interval so that ^◡(𝐹 ↾ 𝐼) maps this into 𝐼 and 𝐹 ∘ 𝑄 maps back to 𝐺. (Contributed by Mario Carneiro, 16-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, 𝑃⟩}⟩}))
cvmliftlem5.3	⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))
cvmliftlem6.1	⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁))
cvmliftlem6.2	⊢ ((𝜑 ∧ 𝜓) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))

**Assertion**
Ref	Expression
cvmliftlem6	⊢ ((𝜑 ∧ 𝜓) → ((𝑄‘𝑀):𝑊⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑀)) = (𝐺 ↾ 𝑊)))

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

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

Step	Hyp	Ref	Expression
1		cvmliftlem.1	. . . . . . . . . . 11 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑢 ∈ 𝑠 (∀𝑣 ∈ (𝑠 ∖ {𝑢})(𝑢 ∩ 𝑣) = ∅ ∧ (𝐹 ↾ 𝑢) ∈ ((𝐶 ↾_t 𝑢)Homeo(𝐽 ↾_t 𝑘))))})
2		cvmliftlem.b	. . . . . . . . . . 11 ⊢ 𝐵 = ∪ 𝐶
3		cvmliftlem.x	. . . . . . . . . . 11 ⊢ 𝑋 = ∪ 𝐽
4		cvmliftlem.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
5		cvmliftlem.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽))
6		cvmliftlem.p	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
7		cvmliftlem.e	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘0))
8		cvmliftlem.n	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		cvmliftlem.t	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶∪ 𝑗 ∈ 𝐽 ({𝑗} × (𝑆‘𝑗)))
10		cvmliftlem.a	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐺 “ (((𝑘 − 1) / 𝑁)[,](𝑘 / 𝑁))) ⊆ (1^st ‘(𝑇‘𝑘)))
11		cvmliftlem.l	. . . . . . . . . . 11 ⊢ 𝐿 = (topGen‘ran (,))
12		cvmliftlem6.1	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ (1...𝑁))
13	12	adantrr 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → 𝑀 ∈ (1...𝑁))
14	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13	cvmliftlem1 34345	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (2^nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1^st ‘(𝑇‘𝑀))))
15	1	cvmsss 34327	. . . . . . . . . 10 ⊢ ((2^nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1^st ‘(𝑇‘𝑀))) → (2^nd ‘(𝑇‘𝑀)) ⊆ 𝐶)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (2^nd ‘(𝑇‘𝑀)) ⊆ 𝐶)
17	4	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → 𝐹 ∈ (𝐶 CovMap 𝐽))
18		cvmliftlem6.2	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝜓) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
19	18	adantrr 715	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}))
20		cvmcn 34322	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
21	2, 3	cnf 22757	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶𝑋)
22	17, 20, 21	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → 𝐹:𝐵⟶𝑋)
23		ffn 6717	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝐵⟶𝑋 → 𝐹 Fn 𝐵)
24		fniniseg 7061	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝐵 → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}) ↔ (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁)))))
25	22, 23, 24	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (^◡𝐹 “ {(𝐺‘((𝑀 − 1) / 𝑁))}) ↔ (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁)))))
26	19, 25	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁))))
27	26	simpld 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵)
28	26	simprd 496	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) = (𝐺‘((𝑀 − 1) / 𝑁)))
29		cvmliftlem5.3	. . . . . . . . . . . . 13 ⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))
30		elfznn 13532	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℕ)
31	13, 30	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → 𝑀 ∈ ℕ)
32	31	nnred 12229	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → 𝑀 ∈ ℝ)
33		peano2rem 11529	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ ℝ → (𝑀 − 1) ∈ ℝ)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝑀 − 1) ∈ ℝ)
35	8	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → 𝑁 ∈ ℕ)
36	34, 35	nndivred 12268	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝑀 − 1) / 𝑁) ∈ ℝ)
37	36	rexrd 11266	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝑀 − 1) / 𝑁) ∈ ℝ^*)
38	32, 35	nndivred 12268	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝑀 / 𝑁) ∈ ℝ)
39	38	rexrd 11266	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝑀 / 𝑁) ∈ ℝ^*)
40	32	ltm1d 12148	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝑀 − 1) < 𝑀)
41	35	nnred 12229	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → 𝑁 ∈ ℝ)
42	35	nngt0d 12263	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → 0 < 𝑁)
43		ltdiv1 12080	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 − 1) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑀 − 1) < 𝑀 ↔ ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁)))
44	34, 32, 41, 42, 43	syl112anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝑀 − 1) < 𝑀 ↔ ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁)))
45	40, 44	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝑀 − 1) / 𝑁) < (𝑀 / 𝑁))
46	36, 38, 45	ltled 11364	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝑀 − 1) / 𝑁) ≤ (𝑀 / 𝑁))
47		lbicc2 13443	. . . . . . . . . . . . . . 15 ⊢ ((((𝑀 − 1) / 𝑁) ∈ ℝ^* ∧ (𝑀 / 𝑁) ∈ ℝ^* ∧ ((𝑀 − 1) / 𝑁) ≤ (𝑀 / 𝑁)) → ((𝑀 − 1) / 𝑁) ∈ (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)))
48	37, 39, 46, 47	syl3anc 1371	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝑀 − 1) / 𝑁) ∈ (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)))
49	48, 29	eleqtrrdi 2844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝑀 − 1) / 𝑁) ∈ 𝑊)
50	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 29, 49	cvmliftlem3 34347	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝐺‘((𝑀 − 1) / 𝑁)) ∈ (1^st ‘(𝑇‘𝑀)))
51	28, 50	eqeltrd 2833	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) ∈ (1^st ‘(𝑇‘𝑀)))
52		eqid 2732	. . . . . . . . . . . 12 ⊢ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) = (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)
53	1, 2, 52	cvmsiota 34337	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ ((2^nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1^st ‘(𝑇‘𝑀))) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝐵 ∧ (𝐹‘((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) ∈ (1^st ‘(𝑇‘𝑀)))) → ((℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2^nd ‘(𝑇‘𝑀)) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)))
54	17, 14, 27, 51, 53	syl13anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2^nd ‘(𝑇‘𝑀)) ∧ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)))
55	54	simpld 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2^nd ‘(𝑇‘𝑀)))
56	16, 55	sseldd 3983	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ 𝐶)
57		elssuni 4941	. . . . . . . 8 ⊢ ((℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ 𝐶 → (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ⊆ ∪ 𝐶)
58	56, 57	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ⊆ ∪ 𝐶)
59	58, 2	sseqtrrdi 4033	. . . . . 6 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ⊆ 𝐵)
60	1	cvmsf1o 34332	. . . . . . . . 9 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (2^nd ‘(𝑇‘𝑀)) ∈ (𝑆‘(1^st ‘(𝑇‘𝑀))) ∧ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) ∈ (2^nd ‘(𝑇‘𝑀))) → (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)):(℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)–1-1-onto→(1^st ‘(𝑇‘𝑀)))
61	17, 14, 55, 60	syl3anc 1371	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)):(℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)–1-1-onto→(1^st ‘(𝑇‘𝑀)))
62		f1ocnv 6845	. . . . . . . 8 ⊢ ((𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)):(℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)–1-1-onto→(1^st ‘(𝑇‘𝑀)) → ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)):(1^st ‘(𝑇‘𝑀))–1-1-onto→(℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))
63		f1of 6833	. . . . . . . 8 ⊢ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)):(1^st ‘(𝑇‘𝑀))–1-1-onto→(℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) → ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)):(1^st ‘(𝑇‘𝑀))⟶(℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))
64	61, 62, 63	3syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)):(1^st ‘(𝑇‘𝑀))⟶(℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))
65		simprr 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → 𝑧 ∈ 𝑊)
66	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 29, 65	cvmliftlem3 34347	. . . . . . 7 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝐺‘𝑧) ∈ (1^st ‘(𝑇‘𝑀)))
67	64, 66	ffvelcdmd 7087	. . . . . 6 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)) ∈ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))
68	59, 67	sseldd 3983	. . . . 5 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)) ∈ 𝐵)
69	68	anassrs 468	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑧 ∈ 𝑊) → (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)) ∈ 𝐵)
70	69	fmpttd 7116	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝑊 ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))):𝑊⟶𝐵)
71	12, 30	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℕ)
72		cvmliftlem.q	. . . . . 6 ⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {⟨0, {⟨0, 𝑃⟩}⟩}))
73	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 72, 29	cvmliftlem5 34349	. . . . 5 ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑄‘𝑀) = (𝑧 ∈ 𝑊 ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))
74	71, 73	syldan 591	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝑄‘𝑀) = (𝑧 ∈ 𝑊 ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))
75	74	feq1d 6702	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝑄‘𝑀):𝑊⟶𝐵 ↔ (𝑧 ∈ 𝑊 ↦ (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))):𝑊⟶𝐵))
76	70, 75	mpbird 256	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝑄‘𝑀):𝑊⟶𝐵)
77		fvres 6910	. . . . . . 7 ⊢ (𝑧 ∈ 𝑊 → ((𝐺 ↾ 𝑊)‘𝑧) = (𝐺‘𝑧))
78	65, 77	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝐺 ↾ 𝑊)‘𝑧) = (𝐺‘𝑧))
79		f1ocnvfv2 7277	. . . . . . 7 ⊢ (((𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)):(℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)–1-1-onto→(1^st ‘(𝑇‘𝑀)) ∧ (𝐺‘𝑧) ∈ (1^st ‘(𝑇‘𝑀))) → ((𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) = (𝐺‘𝑧))
80	61, 66, 79	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) = (𝐺‘𝑧))
81		fvres 6910	. . . . . . 7 ⊢ ((^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)) ∈ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏) → ((𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) = (𝐹‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))
82	67, 81	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → ((𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) = (𝐹‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))
83	78, 80, 82	3eqtr2rd 2779	. . . . 5 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝑧 ∈ 𝑊)) → (𝐹‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) = ((𝐺 ↾ 𝑊)‘𝑧))
84	83	anassrs 468	. . . 4 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑧 ∈ 𝑊) → (𝐹‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) = ((𝐺 ↾ 𝑊)‘𝑧))
85	84	mpteq2dva 5248	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑧 ∈ 𝑊 ↦ (𝐹‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) = (𝑧 ∈ 𝑊 ↦ ((𝐺 ↾ 𝑊)‘𝑧)))
86	4, 20, 21	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝐹:𝐵⟶𝑋)
87	86	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐹:𝐵⟶𝑋)
88	87	feqmptd 6960	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝐹‘𝑦)))
89		fveq2 6891	. . . 4 ⊢ (𝑦 = (^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)) → (𝐹‘𝑦) = (𝐹‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))
90	69, 74, 88, 89	fmptco 7129	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ∘ (𝑄‘𝑀)) = (𝑧 ∈ 𝑊 ↦ (𝐹‘(^◡(𝐹 ↾ (℩𝑏 ∈ (2^nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))))
91		iiuni 24404	. . . . . . . 8 ⊢ (0[,]1) = ∪ II
92	91, 3	cnf 22757	. . . . . . 7 ⊢ (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶𝑋)
93	5, 92	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐺:(0[,]1)⟶𝑋)
94	93	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝐺:(0[,]1)⟶𝑋)
95	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 29	cvmliftlem2 34346	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ⊆ (0[,]1))
96	94, 95	fssresd 6758	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝐺 ↾ 𝑊):𝑊⟶𝑋)
97	96	feqmptd 6960	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝐺 ↾ 𝑊) = (𝑧 ∈ 𝑊 ↦ ((𝐺 ↾ 𝑊)‘𝑧)))
98	85, 90, 97	3eqtr4d 2782	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝐹 ∘ (𝑄‘𝑀)) = (𝐺 ↾ 𝑊))
99	76, 98	jca 512	1 ⊢ ((𝜑 ∧ 𝜓) → ((𝑄‘𝑀):𝑊⟶𝐵 ∧ (𝐹 ∘ (𝑄‘𝑀)) = (𝐺 ↾ 𝑊)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 {crab 3432 Vcvv 3474 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 𝒫 cpw 4602 {csn 4628 ⟨cop 4634 ∪ cuni 4908 ∪ ciun 4997 class class class wbr 5148 ↦ cmpt 5231 I cid 5573 × cxp 5674 ^◡ccnv 5675 ran crn 5677 ↾ cres 5678 “ cima 5679 ∘ ccom 5680 Fn wfn 6538 ⟶wf 6539 –1-1-onto→wf1o 6542 ‘cfv 6543 ℩crio 7366 (class class class)co 7411 ∈ cmpo 7413 1^st c1st 7975 2^nd c2nd 7976 ℝcr 11111 0cc0 11112 1c1 11113 ℝ^*cxr 11249 < clt 11250 ≤ cle 11251 − cmin 11446 / cdiv 11873 ℕcn 12214 (,)cioo 13326 [,]cicc 13329 ...cfz 13486 seqcseq 13968 ↾_t crest 17368 topGenctg 17385 Cn ccn 22735 Homeochmeo 23264 IIcii 24398 CovMap ccvm 34315

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7727 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-er 8705 df-map 8824 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fi 9408 df-sup 9439 df-inf 9440 df-pnf 11252 df-mnf 11253 df-xr 11254 df-ltxr 11255 df-le 11256 df-sub 11448 df-neg 11449 df-div 11874 df-nn 12215 df-2 12277 df-3 12278 df-n0 12475 df-z 12561 df-uz 12825 df-q 12935 df-rp 12977 df-xneg 13094 df-xadd 13095 df-xmul 13096 df-icc 13333 df-fz 13487 df-seq 13969 df-exp 14030 df-cj 15048 df-re 15049 df-im 15050 df-sqrt 15184 df-abs 15185 df-rest 17370 df-topgen 17391 df-psmet 20942 df-xmet 20943 df-met 20944 df-bl 20945 df-mopn 20946 df-top 22403 df-topon 22420 df-bases 22456 df-cn 22738 df-hmeo 23266 df-ii 24400 df-cvm 34316

This theorem is referenced by: cvmliftlem7 34351 cvmliftlem10 34354 cvmliftlem13 34356

W3C validator