cvmlift3lem6 - Mathbox for Mario Carneiro

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

Theorem cvmlift3lem6 31306

Description: Lemma for cvmlift3 31310. (Contributed by Mario Carneiro, 9-Jul-2015.)

**Hypotheses**
Ref	Expression
cvmlift3.b	⊢ 𝐵 = ∪ 𝐶
cvmlift3.y	⊢ 𝑌 = ∪ 𝐾
cvmlift3.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
cvmlift3.k	⊢ (𝜑 → 𝐾 ∈ SConn)
cvmlift3.l	⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)
cvmlift3.o	⊢ (𝜑 → 𝑂 ∈ 𝑌)
cvmlift3.g	⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))
cvmlift3.p	⊢ (𝜑 → 𝑃 ∈ 𝐵)
cvmlift3.e	⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))
cvmlift3.h	⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))
cvmlift3lem7.s	⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))})
cvmlift3lem7.1	⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴)
cvmlift3lem7.2	⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴))
cvmlift3lem7.3	⊢ (𝜑 → 𝑀 ⊆ (^◡𝐺 “ 𝐴))
cvmlift3lem7.w	⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝐻‘𝑋) ∈ 𝑏)
cvmlift3lem6.x	⊢ (𝜑 → 𝑋 ∈ 𝑀)
cvmlift3lem6.z	⊢ (𝜑 → 𝑍 ∈ 𝑀)
cvmlift3lem6.q	⊢ (𝜑 → 𝑄 ∈ (II Cn 𝐾))
cvmlift3lem6.r	⊢ 𝑅 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑄) ∧ (𝑔‘0) = 𝑃))
cvmlift3lem6.1	⊢ (𝜑 → ((𝑄‘0) = 𝑂 ∧ (𝑄‘1) = 𝑋 ∧ (𝑅‘1) = (𝐻‘𝑋)))
cvmlift3lem6.n	⊢ (𝜑 → 𝑁 ∈ (II Cn (𝐾 ↾_t 𝑀)))
cvmlift3lem6.2	⊢ (𝜑 → ((𝑁‘0) = 𝑋 ∧ (𝑁‘1) = 𝑍))
cvmlift3lem6.i	⊢ 𝐼 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑁) ∧ (𝑔‘0) = (𝐻‘𝑋)))

**Assertion**
Ref	Expression
cvmlift3lem6	⊢ (𝜑 → (𝐻‘𝑍) ∈ 𝑊)

Distinct variable groups: 𝑏,𝑐,𝑑,𝑓,𝑘,𝑠,𝑧,𝐴 𝑓,𝑔,𝐼,𝑧 𝑔,𝑏,𝑥,𝐽,𝑐,𝑑,𝑓,𝑘,𝑠 𝐹,𝑏,𝑐,𝑑,𝑓,𝑔,𝑘,𝑠 𝑥,𝑧,𝐹 𝑓,𝑀,𝑔,𝑥 𝑓,𝑁,𝑔 𝐻,𝑏,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧 𝑄,𝑓,𝑔 𝑆,𝑏,𝑓,𝑥 𝐵,𝑏,𝑑,𝑓,𝑔,𝑥,𝑧 𝑅,𝑔 𝑋,𝑏,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧 𝐺,𝑏,𝑐,𝑑,𝑓,𝑔,𝑘,𝑥,𝑧 𝑇,𝑏,𝑐,𝑑,𝑠 𝑓,𝑍,𝑔,𝑥,𝑧 𝐶,𝑏,𝑐,𝑑,𝑓,𝑔,𝑘,𝑠,𝑥,𝑧 𝜑,𝑓,𝑥 𝐾,𝑏,𝑐,𝑓,𝑔,𝑥,𝑧 𝑃,𝑏,𝑐,𝑑,𝑓,𝑔,𝑥,𝑧 𝑂,𝑏,𝑐,𝑓,𝑔,𝑥,𝑧 𝑓,𝑌,𝑔,𝑥,𝑧 𝑊,𝑐,𝑑,𝑓,𝑥 Allowed substitution hints: 𝜑(𝑧,𝑔,𝑘,𝑠,𝑏,𝑐,𝑑) 𝐴(𝑥,𝑔) 𝐵(𝑘,𝑠,𝑐) 𝑃(𝑘,𝑠) 𝑄(𝑥,𝑧,𝑘,𝑠,𝑏,𝑐,𝑑) 𝑅(𝑥,𝑧,𝑓,𝑘,𝑠,𝑏,𝑐,𝑑) 𝑆(𝑧,𝑔,𝑘,𝑠,𝑐,𝑑) 𝑇(𝑥,𝑧,𝑓,𝑔,𝑘) 𝐺(𝑠) 𝐻(𝑘,𝑠) 𝐼(𝑥,𝑘,𝑠,𝑏,𝑐,𝑑) 𝐽(𝑧) 𝐾(𝑘,𝑠,𝑑) 𝑀(𝑧,𝑘,𝑠,𝑏,𝑐,𝑑) 𝑁(𝑥,𝑧,𝑘,𝑠,𝑏,𝑐,𝑑) 𝑂(𝑘,𝑠,𝑑) 𝑊(𝑧,𝑔,𝑘,𝑠,𝑏) 𝑋(𝑘,𝑠) 𝑌(𝑘,𝑠,𝑏,𝑐,𝑑) 𝑍(𝑘,𝑠,𝑏,𝑐,𝑑)

**Proof of Theorem cvmlift3lem6**
Step	Hyp	Ref	Expression
1		cvmlift3lem6.q	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ (II Cn 𝐾))
2		cvmlift3.k	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ SConn)
3		sconntop 31210	. . . . . . . 8 ⊢ (𝐾 ∈ SConn → 𝐾 ∈ Top)
4	2, 3	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Top)
5		cnrest2r 21091	. . . . . . 7 ⊢ (𝐾 ∈ Top → (II Cn (𝐾 ↾_t 𝑀)) ⊆ (II Cn 𝐾))
6	4, 5	syl 17	. . . . . 6 ⊢ (𝜑 → (II Cn (𝐾 ↾_t 𝑀)) ⊆ (II Cn 𝐾))
7		cvmlift3lem6.n	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (II Cn (𝐾 ↾_t 𝑀)))
8	6, 7	sseldd 3604	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ (II Cn 𝐾))
9		cvmlift3lem6.1	. . . . . . 7 ⊢ (𝜑 → ((𝑄‘0) = 𝑂 ∧ (𝑄‘1) = 𝑋 ∧ (𝑅‘1) = (𝐻‘𝑋)))
10	9	simp2d 1074	. . . . . 6 ⊢ (𝜑 → (𝑄‘1) = 𝑋)
11		cvmlift3lem6.2	. . . . . . 7 ⊢ (𝜑 → ((𝑁‘0) = 𝑋 ∧ (𝑁‘1) = 𝑍))
12	11	simpld 475	. . . . . 6 ⊢ (𝜑 → (𝑁‘0) = 𝑋)
13	10, 12	eqtr4d 2659	. . . . 5 ⊢ (𝜑 → (𝑄‘1) = (𝑁‘0))
14	1, 8, 13	pcocn 22817	. . . 4 ⊢ (𝜑 → (𝑄(*_𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾))
15	1, 8	pco0 22814	. . . . 5 ⊢ (𝜑 → ((𝑄(*_𝑝‘𝐾)𝑁)‘0) = (𝑄‘0))
16	9	simp1d 1073	. . . . 5 ⊢ (𝜑 → (𝑄‘0) = 𝑂)
17	15, 16	eqtrd 2656	. . . 4 ⊢ (𝜑 → ((𝑄(*_𝑝‘𝐾)𝑁)‘0) = 𝑂)
18	1, 8	pco1 22815	. . . . 5 ⊢ (𝜑 → ((𝑄(*_𝑝‘𝐾)𝑁)‘1) = (𝑁‘1))
19	11	simprd 479	. . . . 5 ⊢ (𝜑 → (𝑁‘1) = 𝑍)
20	18, 19	eqtrd 2656	. . . 4 ⊢ (𝜑 → ((𝑄(*_𝑝‘𝐾)𝑁)‘1) = 𝑍)
21		cvmlift3.b	. . . . . . . . . . 11 ⊢ 𝐵 = ∪ 𝐶
22		cvmlift3lem6.r	. . . . . . . . . . 11 ⊢ 𝑅 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑄) ∧ (𝑔‘0) = 𝑃))
23		cvmlift3.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (𝐶 CovMap 𝐽))
24		cvmlift3.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))
25		cnco 21070	. . . . . . . . . . . 12 ⊢ ((𝑄 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ 𝑄) ∈ (II Cn 𝐽))
26	1, 24, 25	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 ∘ 𝑄) ∈ (II Cn 𝐽))
27		cvmlift3.p	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
28	16	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺‘(𝑄‘0)) = (𝐺‘𝑂))
29		iiuni 22684	. . . . . . . . . . . . . . 15 ⊢ (0[,]1) = ∪ II
30		cvmlift3.y	. . . . . . . . . . . . . . 15 ⊢ 𝑌 = ∪ 𝐾
31	29, 30	cnf 21050	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ (II Cn 𝐾) → 𝑄:(0[,]1)⟶𝑌)
32	1, 31	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑄:(0[,]1)⟶𝑌)
33		0elunit 12290	. . . . . . . . . . . . 13 ⊢ 0 ∈ (0[,]1)
34		fvco3 6275	. . . . . . . . . . . . 13 ⊢ ((𝑄:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) → ((𝐺 ∘ 𝑄)‘0) = (𝐺‘(𝑄‘0)))
35	32, 33, 34	sylancl 694	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺 ∘ 𝑄)‘0) = (𝐺‘(𝑄‘0)))
36		cvmlift3.e	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘𝑃) = (𝐺‘𝑂))
37	28, 35, 36	3eqtr4rd 2667	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ 𝑄)‘0))
38	21, 22, 23, 26, 27, 37	cvmliftiota 31283	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝑅) = (𝐺 ∘ 𝑄) ∧ (𝑅‘0) = 𝑃))
39	38	simp2d 1074	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∘ 𝑅) = (𝐺 ∘ 𝑄))
40		cvmlift3lem6.i	. . . . . . . . . . 11 ⊢ 𝐼 = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑁) ∧ (𝑔‘0) = (𝐻‘𝑋)))
41		cnco 21070	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ 𝑁) ∈ (II Cn 𝐽))
42	8, 24, 41	syl2anc 693	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 ∘ 𝑁) ∈ (II Cn 𝐽))
43		cvmlift3.l	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally PConn)
44		cvmlift3.o	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑂 ∈ 𝑌)
45		cvmlift3.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ 𝑌 ↦ (℩𝑧 ∈ 𝐵 ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑥 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = 𝑧)))
46	21, 30, 23, 2, 43, 44, 24, 27, 36, 45	cvmlift3lem3 31303	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻:𝑌⟶𝐵)
47		cvmlift3lem7.3	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ⊆ (^◡𝐺 “ 𝐴))
48		cnvimass 5485	. . . . . . . . . . . . . . 15 ⊢ (^◡𝐺 “ 𝐴) ⊆ dom 𝐺
49		eqid 2622	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝐽 = ∪ 𝐽
50	30, 49	cnf 21050	. . . . . . . . . . . . . . . . 17 ⊢ (𝐺 ∈ (𝐾 Cn 𝐽) → 𝐺:𝑌⟶∪ 𝐽)
51	24, 50	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝐽)
52		fdm 6051	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:𝑌⟶∪ 𝐽 → dom 𝐺 = 𝑌)
53	51, 52	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → dom 𝐺 = 𝑌)
54	48, 53	syl5sseq 3653	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡𝐺 “ 𝐴) ⊆ 𝑌)
55	47, 54	sstrd 3613	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ⊆ 𝑌)
56		cvmlift3lem6.x	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ 𝑀)
57	55, 56	sseldd 3604	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝑌)
58	46, 57	ffvelrnd 6360	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐻‘𝑋) ∈ 𝐵)
59	12	fveq2d 6195	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺‘(𝑁‘0)) = (𝐺‘𝑋))
60	29, 30	cnf 21050	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (II Cn 𝐾) → 𝑁:(0[,]1)⟶𝑌)
61	8, 60	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁:(0[,]1)⟶𝑌)
62		fvco3 6275	. . . . . . . . . . . . 13 ⊢ ((𝑁:(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) → ((𝐺 ∘ 𝑁)‘0) = (𝐺‘(𝑁‘0)))
63	61, 33, 62	sylancl 694	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐺 ∘ 𝑁)‘0) = (𝐺‘(𝑁‘0)))
64		fvco3 6275	. . . . . . . . . . . . . 14 ⊢ ((𝐻:𝑌⟶𝐵 ∧ 𝑋 ∈ 𝑌) → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋)))
65	46, 57, 64	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐹‘(𝐻‘𝑋)))
66	21, 30, 23, 2, 43, 44, 24, 27, 36, 45	cvmlift3lem5 31305	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∘ 𝐻) = 𝐺)
67	66	fveq1d 6193	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹 ∘ 𝐻)‘𝑋) = (𝐺‘𝑋))
68	65, 67	eqtr3d 2658	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) = (𝐺‘𝑋))
69	59, 63, 68	3eqtr4rd 2667	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) = ((𝐺 ∘ 𝑁)‘0))
70	21, 40, 23, 42, 58, 69	cvmliftiota 31283	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐶) ∧ (𝐹 ∘ 𝐼) = (𝐺 ∘ 𝑁) ∧ (𝐼‘0) = (𝐻‘𝑋)))
71	70	simp2d 1074	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∘ 𝐼) = (𝐺 ∘ 𝑁))
72	39, 71	oveq12d 6668	. . . . . . . 8 ⊢ (𝜑 → ((𝐹 ∘ 𝑅)(_𝑝‘𝐽)(𝐹 ∘ 𝐼)) = ((𝐺 ∘ 𝑄)(_𝑝‘𝐽)(𝐺 ∘ 𝑁)))
73	38	simp1d 1073	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ∈ (II Cn 𝐶))
74	70	simp1d 1073	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ (II Cn 𝐶))
75	9	simp3d 1075	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅‘1) = (𝐻‘𝑋))
76	70	simp3d 1075	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼‘0) = (𝐻‘𝑋))
77	75, 76	eqtr4d 2659	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘1) = (𝐼‘0))
78		cvmcn 31244	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
79	23, 78	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Cn 𝐽))
80	73, 74, 77, 79	copco 22818	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∘ (𝑅(_𝑝‘𝐶)𝐼)) = ((𝐹 ∘ 𝑅)(_𝑝‘𝐽)(𝐹 ∘ 𝐼)))
81	1, 8, 13, 24	copco 22818	. . . . . . . 8 ⊢ (𝜑 → (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) = ((𝐺 ∘ 𝑄)(_𝑝‘𝐽)(𝐺 ∘ 𝑁)))
82	72, 80, 81	3eqtr4d 2666	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘ (𝑅(_𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)))
83	73, 74	pco0 22814	. . . . . . . 8 ⊢ (𝜑 → ((𝑅(*_𝑝‘𝐶)𝐼)‘0) = (𝑅‘0))
84	38	simp3d 1075	. . . . . . . 8 ⊢ (𝜑 → (𝑅‘0) = 𝑃)
85	83, 84	eqtrd 2656	. . . . . . 7 ⊢ (𝜑 → ((𝑅(*_𝑝‘𝐶)𝐼)‘0) = 𝑃)
86	73, 74, 77	pcocn 22817	. . . . . . . 8 ⊢ (𝜑 → (𝑅(*_𝑝‘𝐶)𝐼) ∈ (II Cn 𝐶))
87		cnco 21070	. . . . . . . . . 10 ⊢ (((𝑄(_𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐽)) → (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽))
88	14, 24, 87	syl2anc 693	. . . . . . . . 9 ⊢ (𝜑 → (𝐺 ∘ (𝑄(*_𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽))
89	17	fveq2d 6195	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘((𝑄(*_𝑝‘𝐾)𝑁)‘0)) = (𝐺‘𝑂))
90	29, 30	cnf 21050	. . . . . . . . . . . 12 ⊢ ((𝑄(_𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) → (𝑄(_𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌)
91	14, 90	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄(*_𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌)
92		fvco3 6275	. . . . . . . . . . 11 ⊢ (((𝑄(_𝑝‘𝐾)𝑁):(0[,]1)⟶𝑌 ∧ 0 ∈ (0[,]1)) → ((𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁))‘0) = (𝐺‘((𝑄(*_𝑝‘𝐾)𝑁)‘0)))
93	91, 33, 92	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁))‘0) = (𝐺‘((𝑄(_𝑝‘𝐾)𝑁)‘0)))
94	89, 93, 36	3eqtr4rd 2667	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑃) = ((𝐺 ∘ (𝑄(*_𝑝‘𝐾)𝑁))‘0))
95	21	cvmlift 31281	. . . . . . . . 9 ⊢ (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∈ (II Cn 𝐽)) ∧ (𝑃 ∈ 𝐵 ∧ (𝐹‘𝑃) = ((𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁))‘0))) → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))
96	23, 88, 27, 94, 95	syl22anc 1327	. . . . . . . 8 ⊢ (𝜑 → ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))
97		coeq2 5280	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑅(_𝑝‘𝐶)𝐼) → (𝐹 ∘ 𝑔) = (𝐹 ∘ (𝑅(_𝑝‘𝐶)𝐼)))
98	97	eqeq1d 2624	. . . . . . . . . 10 ⊢ (𝑔 = (𝑅(_𝑝‘𝐶)𝐼) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ↔ (𝐹 ∘ (𝑅(_𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁))))
99		fveq1 6190	. . . . . . . . . . 11 ⊢ (𝑔 = (𝑅(_𝑝‘𝐶)𝐼) → (𝑔‘0) = ((𝑅(_𝑝‘𝐶)𝐼)‘0))
100	99	eqeq1d 2624	. . . . . . . . . 10 ⊢ (𝑔 = (𝑅(_𝑝‘𝐶)𝐼) → ((𝑔‘0) = 𝑃 ↔ ((𝑅(_𝑝‘𝐶)𝐼)‘0) = 𝑃))
101	98, 100	anbi12d 747	. . . . . . . . 9 ⊢ (𝑔 = (𝑅(_𝑝‘𝐶)𝐼) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ (𝑅(_𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ ((𝑅(*_𝑝‘𝐶)𝐼)‘0) = 𝑃)))
102	101	riota2 6633	. . . . . . . 8 ⊢ (((𝑅(_𝑝‘𝐶)𝐼) ∈ (II Cn 𝐶) ∧ ∃!𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) → (((𝐹 ∘ (𝑅(_𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ ((𝑅(_𝑝‘𝐶)𝐼)‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*_𝑝‘𝐶)𝐼)))
103	86, 96, 102	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → (((𝐹 ∘ (𝑅(_𝑝‘𝐶)𝐼)) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ ((𝑅(_𝑝‘𝐶)𝐼)‘0) = 𝑃) ↔ (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(*_𝑝‘𝐶)𝐼)))
104	82, 85, 103	mpbi2and 956	. . . . . 6 ⊢ (𝜑 → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)) = (𝑅(_𝑝‘𝐶)𝐼))
105	104	fveq1d 6193	. . . . 5 ⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = ((𝑅(_𝑝‘𝐶)𝐼)‘1))
106	73, 74	pco1 22815	. . . . 5 ⊢ (𝜑 → ((𝑅(*_𝑝‘𝐶)𝐼)‘1) = (𝐼‘1))
107	105, 106	eqtrd 2656	. . . 4 ⊢ (𝜑 → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(*_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))
108		fveq1 6190	. . . . . . 7 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → (𝑓‘0) = ((𝑄(_𝑝‘𝐾)𝑁)‘0))
109	108	eqeq1d 2624	. . . . . 6 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → ((𝑓‘0) = 𝑂 ↔ ((𝑄(_𝑝‘𝐾)𝑁)‘0) = 𝑂))
110		fveq1 6190	. . . . . . 7 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → (𝑓‘1) = ((𝑄(_𝑝‘𝐾)𝑁)‘1))
111	110	eqeq1d 2624	. . . . . 6 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → ((𝑓‘1) = 𝑍 ↔ ((𝑄(_𝑝‘𝐾)𝑁)‘1) = 𝑍))
112		coeq2 5280	. . . . . . . . . . 11 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → (𝐺 ∘ 𝑓) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)))
113	112	eqeq2d 2632	. . . . . . . . . 10 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → ((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ↔ (𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁))))
114	113	anbi1d 741	. . . . . . . . 9 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → (((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃) ↔ ((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)))
115	114	riotabidv 6613	. . . . . . . 8 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃)) = (℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃)))
116	115	fveq1d 6193	. . . . . . 7 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1))
117	116	eqeq1d 2624	. . . . . 6 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → (((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1) ↔ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))
118	109, 111, 117	3anbi123d 1399	. . . . 5 ⊢ (𝑓 = (𝑄(_𝑝‘𝐾)𝑁) → (((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)) ↔ (((𝑄(_𝑝‘𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(_𝑝‘𝐾)𝑁)‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))))
119	118	rspcev 3309	. . . 4 ⊢ (((𝑄(_𝑝‘𝐾)𝑁) ∈ (II Cn 𝐾) ∧ (((𝑄(_𝑝‘𝐾)𝑁)‘0) = 𝑂 ∧ ((𝑄(_𝑝‘𝐾)𝑁)‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ (𝑄(_𝑝‘𝐾)𝑁)) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))) → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))
120	14, 17, 20, 107, 119	syl13anc 1328	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1)))
121		cvmlift3lem6.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑀)
122	55, 121	sseldd 3604	. . . 4 ⊢ (𝜑 → 𝑍 ∈ 𝑌)
123	21, 30, 23, 2, 43, 44, 24, 27, 36, 45	cvmlift3lem4 31304	. . . 4 ⊢ ((𝜑 ∧ 𝑍 ∈ 𝑌) → ((𝐻‘𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))))
124	122, 123	mpdan 702	. . 3 ⊢ (𝜑 → ((𝐻‘𝑍) = (𝐼‘1) ↔ ∃𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = 𝑂 ∧ (𝑓‘1) = 𝑍 ∧ ((℩𝑔 ∈ (II Cn 𝐶)((𝐹 ∘ 𝑔) = (𝐺 ∘ 𝑓) ∧ (𝑔‘0) = 𝑃))‘1) = (𝐼‘1))))
125	120, 124	mpbird 247	. 2 ⊢ (𝜑 → (𝐻‘𝑍) = (𝐼‘1))
126		iiconn 22690	. . . . 5 ⊢ II ∈ Conn
127	126	a1i 11	. . . 4 ⊢ (𝜑 → II ∈ Conn)
128		cvmtop1 31242	. . . . . . . 8 ⊢ (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
129	23, 128	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ Top)
130	21	toptopon 20722	. . . . . . 7 ⊢ (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
131	129, 130	sylib 208	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ (TopOn‘𝐵))
132	71	rneqd 5353	. . . . . . . . 9 ⊢ (𝜑 → ran (𝐹 ∘ 𝐼) = ran (𝐺 ∘ 𝑁))
133		rnco2 5642	. . . . . . . . 9 ⊢ ran (𝐹 ∘ 𝐼) = (𝐹 “ ran 𝐼)
134		rnco2 5642	. . . . . . . . 9 ⊢ ran (𝐺 ∘ 𝑁) = (𝐺 “ ran 𝑁)
135	132, 133, 134	3eqtr3g 2679	. . . . . . . 8 ⊢ (𝜑 → (𝐹 “ ran 𝐼) = (𝐺 “ ran 𝑁))
136		iitopon 22682	. . . . . . . . . . . . 13 ⊢ II ∈ (TopOn‘(0[,]1))
137	136	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → II ∈ (TopOn‘(0[,]1)))
138	30	toptopon 20722	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
139	4, 138	sylib 208	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
140		resttopon 20965	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑀 ⊆ 𝑌) → (𝐾 ↾_t 𝑀) ∈ (TopOn‘𝑀))
141	139, 55, 140	syl2anc 693	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾 ↾_t 𝑀) ∈ (TopOn‘𝑀))
142		cnf2 21053	. . . . . . . . . . . 12 ⊢ ((II ∈ (TopOn‘(0[,]1)) ∧ (𝐾 ↾_t 𝑀) ∈ (TopOn‘𝑀) ∧ 𝑁 ∈ (II Cn (𝐾 ↾_t 𝑀))) → 𝑁:(0[,]1)⟶𝑀)
143	137, 141, 7, 142	syl3anc 1326	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁:(0[,]1)⟶𝑀)
144		frn 6053	. . . . . . . . . . 11 ⊢ (𝑁:(0[,]1)⟶𝑀 → ran 𝑁 ⊆ 𝑀)
145	143, 144	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑁 ⊆ 𝑀)
146	145, 47	sstrd 3613	. . . . . . . . 9 ⊢ (𝜑 → ran 𝑁 ⊆ (^◡𝐺 “ 𝐴))
147		ffun 6048	. . . . . . . . . . 11 ⊢ (𝐺:𝑌⟶∪ 𝐽 → Fun 𝐺)
148	51, 147	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐺)
149	146, 48	syl6ss 3615	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑁 ⊆ dom 𝐺)
150		funimass3 6333	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ ran 𝑁 ⊆ dom 𝐺) → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (^◡𝐺 “ 𝐴)))
151	148, 149, 150	syl2anc 693	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 “ ran 𝑁) ⊆ 𝐴 ↔ ran 𝑁 ⊆ (^◡𝐺 “ 𝐴)))
152	146, 151	mpbird 247	. . . . . . . 8 ⊢ (𝜑 → (𝐺 “ ran 𝑁) ⊆ 𝐴)
153	135, 152	eqsstrd 3639	. . . . . . 7 ⊢ (𝜑 → (𝐹 “ ran 𝐼) ⊆ 𝐴)
154	21, 49	cnf 21050	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵⟶∪ 𝐽)
155	79, 154	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐵⟶∪ 𝐽)
156		ffun 6048	. . . . . . . . 9 ⊢ (𝐹:𝐵⟶∪ 𝐽 → Fun 𝐹)
157	155, 156	syl 17	. . . . . . . 8 ⊢ (𝜑 → Fun 𝐹)
158	29, 21	cnf 21050	. . . . . . . . . . 11 ⊢ (𝐼 ∈ (II Cn 𝐶) → 𝐼:(0[,]1)⟶𝐵)
159	74, 158	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼:(0[,]1)⟶𝐵)
160		frn 6053	. . . . . . . . . 10 ⊢ (𝐼:(0[,]1)⟶𝐵 → ran 𝐼 ⊆ 𝐵)
161	159, 160	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐼 ⊆ 𝐵)
162		fdm 6051	. . . . . . . . . 10 ⊢ (𝐹:𝐵⟶∪ 𝐽 → dom 𝐹 = 𝐵)
163	155, 162	syl 17	. . . . . . . . 9 ⊢ (𝜑 → dom 𝐹 = 𝐵)
164	161, 163	sseqtr4d 3642	. . . . . . . 8 ⊢ (𝜑 → ran 𝐼 ⊆ dom 𝐹)
165		funimass3 6333	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ ran 𝐼 ⊆ dom 𝐹) → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (^◡𝐹 “ 𝐴)))
166	157, 164, 165	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → ((𝐹 “ ran 𝐼) ⊆ 𝐴 ↔ ran 𝐼 ⊆ (^◡𝐹 “ 𝐴)))
167	153, 166	mpbid 222	. . . . . 6 ⊢ (𝜑 → ran 𝐼 ⊆ (^◡𝐹 “ 𝐴))
168		cnvimass 5485	. . . . . . 7 ⊢ (^◡𝐹 “ 𝐴) ⊆ dom 𝐹
169	168, 163	syl5sseq 3653	. . . . . 6 ⊢ (𝜑 → (^◡𝐹 “ 𝐴) ⊆ 𝐵)
170		cnrest2 21090	. . . . . 6 ⊢ ((𝐶 ∈ (TopOn‘𝐵) ∧ ran 𝐼 ⊆ (^◡𝐹 “ 𝐴) ∧ (^◡𝐹 “ 𝐴) ⊆ 𝐵) → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶 ↾_t (^◡𝐹 “ 𝐴)))))
171	131, 167, 169, 170	syl3anc 1326	. . . . 5 ⊢ (𝜑 → (𝐼 ∈ (II Cn 𝐶) ↔ 𝐼 ∈ (II Cn (𝐶 ↾_t (^◡𝐹 “ 𝐴)))))
172	74, 171	mpbid 222	. . . 4 ⊢ (𝜑 → 𝐼 ∈ (II Cn (𝐶 ↾_t (^◡𝐹 “ 𝐴))))
173		cvmlift3lem7.2	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ (𝑆‘𝐴))
174		cvmlift3lem7.s	. . . . . . . 8 ⊢ 𝑆 = (𝑘 ∈ 𝐽 ↦ {𝑠 ∈ (𝒫 𝐶 ∖ {∅}) ∣ (∪ 𝑠 = (^◡𝐹 “ 𝑘) ∧ ∀𝑐 ∈ 𝑠 (∀𝑑 ∈ (𝑠 ∖ {𝑐})(𝑐 ∩ 𝑑) = ∅ ∧ (𝐹 ↾ 𝑐) ∈ ((𝐶 ↾_t 𝑐)Homeo(𝐽 ↾_t 𝑘))))})
175	174	cvmsss 31249	. . . . . . 7 ⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝑇 ⊆ 𝐶)
176	173, 175	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑇 ⊆ 𝐶)
177		cvmlift3lem7.1	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴)
178	68, 177	eqeltrd 2701	. . . . . . . 8 ⊢ (𝜑 → (𝐹‘(𝐻‘𝑋)) ∈ 𝐴)
179		cvmlift3lem7.w	. . . . . . . . 9 ⊢ 𝑊 = (℩𝑏 ∈ 𝑇 (𝐻‘𝑋) ∈ 𝑏)
180	174, 21, 179	cvmsiota 31259	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ (𝑇 ∈ (𝑆‘𝐴) ∧ (𝐻‘𝑋) ∈ 𝐵 ∧ (𝐹‘(𝐻‘𝑋)) ∈ 𝐴)) → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊))
181	23, 173, 58, 178, 180	syl13anc 1328	. . . . . . 7 ⊢ (𝜑 → (𝑊 ∈ 𝑇 ∧ (𝐻‘𝑋) ∈ 𝑊))
182	181	simpld 475	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ 𝑇)
183	176, 182	sseldd 3604	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ 𝐶)
184		elssuni 4467	. . . . . . 7 ⊢ (𝑊 ∈ 𝑇 → 𝑊 ⊆ ∪ 𝑇)
185	182, 184	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑊 ⊆ ∪ 𝑇)
186	174	cvmsuni 31251	. . . . . . 7 ⊢ (𝑇 ∈ (𝑆‘𝐴) → ∪ 𝑇 = (^◡𝐹 “ 𝐴))
187	173, 186	syl 17	. . . . . 6 ⊢ (𝜑 → ∪ 𝑇 = (^◡𝐹 “ 𝐴))
188	185, 187	sseqtrd 3641	. . . . 5 ⊢ (𝜑 → 𝑊 ⊆ (^◡𝐹 “ 𝐴))
189	174	cvmsrcl 31246	. . . . . . . 8 ⊢ (𝑇 ∈ (𝑆‘𝐴) → 𝐴 ∈ 𝐽)
190	173, 189	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝐽)
191		cnima 21069	. . . . . . 7 ⊢ ((𝐹 ∈ (𝐶 Cn 𝐽) ∧ 𝐴 ∈ 𝐽) → (^◡𝐹 “ 𝐴) ∈ 𝐶)
192	79, 190, 191	syl2anc 693	. . . . . 6 ⊢ (𝜑 → (^◡𝐹 “ 𝐴) ∈ 𝐶)
193		restopn2 20981	. . . . . 6 ⊢ ((𝐶 ∈ Top ∧ (^◡𝐹 “ 𝐴) ∈ 𝐶) → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝐴)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝐴))))
194	129, 192, 193	syl2anc 693	. . . . 5 ⊢ (𝜑 → (𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝐴)) ↔ (𝑊 ∈ 𝐶 ∧ 𝑊 ⊆ (^◡𝐹 “ 𝐴))))
195	183, 188, 194	mpbir2and 957	. . . 4 ⊢ (𝜑 → 𝑊 ∈ (𝐶 ↾_t (^◡𝐹 “ 𝐴)))
196	174	cvmscld 31255	. . . . 5 ⊢ ((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝑇 ∈ (𝑆‘𝐴) ∧ 𝑊 ∈ 𝑇) → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝐴))))
197	23, 173, 182, 196	syl3anc 1326	. . . 4 ⊢ (𝜑 → 𝑊 ∈ (Clsd‘(𝐶 ↾_t (^◡𝐹 “ 𝐴))))
198	33	a1i 11	. . . 4 ⊢ (𝜑 → 0 ∈ (0[,]1))
199	181	simprd 479	. . . . 5 ⊢ (𝜑 → (𝐻‘𝑋) ∈ 𝑊)
200	76, 199	eqeltrd 2701	. . . 4 ⊢ (𝜑 → (𝐼‘0) ∈ 𝑊)
201	29, 127, 172, 195, 197, 198, 200	conncn 21229	. . 3 ⊢ (𝜑 → 𝐼:(0[,]1)⟶𝑊)
202		1elunit 12291	. . 3 ⊢ 1 ∈ (0[,]1)
203		ffvelrn 6357	. . 3 ⊢ ((𝐼:(0[,]1)⟶𝑊 ∧ 1 ∈ (0[,]1)) → (𝐼‘1) ∈ 𝑊)
204	201, 202, 203	sylancl 694	. 2 ⊢ (𝜑 → (𝐼‘1) ∈ 𝑊)
205	125, 204	eqeltrd 2701	1 ⊢ (𝜑 → (𝐻‘𝑍) ∈ 𝑊)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 ∃!wreu 2914 {crab 2916 ∖ cdif 3571 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 𝒫 cpw 4158 {csn 4177 ∪ cuni 4436 ↦ cmpt 4729 ^◡ccnv 5113 dom cdm 5114 ran crn 5115 ↾ cres 5116 “ cima 5117 ∘ ccom 5118 Fun wfun 5882 ⟶wf 5884 ‘cfv 5888 ℩crio 6610 (class class class)co 6650 0cc0 9936 1c1 9937 [,]cicc 12178 ↾_t crest 16081 Topctop 20698 TopOnctopon 20715 Clsdccld 20820 Cn ccn 21028 Conncconn 21214 𝑛-Locally cnlly 21268 Homeochmeo 21556 IIcii 22678 *_𝑝cpco 22800 PConncpconn 31201 SConncsconn 31202 CovMap ccvm 31237

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-ec 7744 df-map 7859 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-cn 21031 df-cnp 21032 df-cmp 21190 df-conn 21215 df-lly 21269 df-nlly 21270 df-tx 21365 df-hmeo 21558 df-xms 22125 df-ms 22126 df-tms 22127 df-ii 22680 df-htpy 22769 df-phtpy 22770 df-phtpc 22791 df-pco 22805 df-pconn 31203 df-sconn 31204 df-cvm 31238

This theorem is referenced by: cvmlift3lem7 31307

W3C validator