cvmlift3lem6

	Ref	Expression
Hypotheses	cvmlift3.b	$⊢ B = ⋃ C$
	cvmlift3.y	$⊢ Y = ⋃ K$
	cvmlift3.f	$⊢ φ \to F \in (C CovMap J)$
	cvmlift3.k	$⊢ φ \to K \in SConn$
	cvmlift3.l	$⊢ φ \to K \in N-LocallyPConn$
	cvmlift3.o	$⊢ φ \to O \in Y$
	cvmlift3.g	$⊢ φ \to G \in (K Cn J)$
	cvmlift3.p	$⊢ φ \to P \in B$
	cvmlift3.e	$⊢ φ \to F (P) = G (O)$
	cvmlift3.h	$⊢ H = (x \in Y ⟼ (ι z \in B \| \exists f \in (II Cn K) (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z)))$
	cvmlift3lem7.s	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall c \in s (\forall d \in (s ∖ \{c\}) c \cap d = \emptyset \land {F ↾}_{c} \in ((C ↾_{𝑡} c) Homeo (J ↾_{𝑡} k))))\})$
	cvmlift3lem7.1	$⊢ φ \to G (X) \in A$
	cvmlift3lem7.2	$⊢ φ \to T \in S (A)$
	cvmlift3lem7.3	$⊢ φ \to M \subseteq G^{-1} [A]$
	cvmlift3lem7.w	$⊢ W = (ι b \in T \| H (X) \in b)$
	cvmlift3lem6.x	$⊢ φ \to X \in M$
	cvmlift3lem6.z	$⊢ φ \to Z \in M$
	cvmlift3lem6.q	$⊢ φ \to Q \in (II Cn K)$
	cvmlift3lem6.r	$⊢ R = (ι g \in (II Cn C) \| (F \circ g = G \circ Q \land g (0) = P))$
	cvmlift3lem6.1	$⊢ φ \to (Q (0) = O \land Q (1) = X \land R (1) = H (X))$
	cvmlift3lem6.n	$⊢ φ \to N \in (II Cn (K ↾_{𝑡} M))$
	cvmlift3lem6.2	$⊢ φ \to (N (0) = X \land N (1) = Z)$
	cvmlift3lem6.i	$⊢ I = (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = H (X)))$
Assertion	cvmlift3lem6	$⊢ φ \to H (Z) \in W$

Proof

Step	Hyp	Ref	Expression
1		cvmlift3.b	$⊢ B = ⋃ C$
2		cvmlift3.y	$⊢ Y = ⋃ K$
3		cvmlift3.f	$⊢ φ \to F \in (C CovMap J)$
4		cvmlift3.k	$⊢ φ \to K \in SConn$
5		cvmlift3.l	$⊢ φ \to K \in N-LocallyPConn$
6		cvmlift3.o	$⊢ φ \to O \in Y$
7		cvmlift3.g	$⊢ φ \to G \in (K Cn J)$
8		cvmlift3.p	$⊢ φ \to P \in B$
9		cvmlift3.e	$⊢ φ \to F (P) = G (O)$
10		cvmlift3.h	$⊢ H = (x \in Y ⟼ (ι z \in B \| \exists f \in (II Cn K) (f (0) = O \land f (1) = x \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = z)))$
11		cvmlift3lem7.s	$⊢ S = (k \in J ⟼ \{s \in (𝒫 C ∖ \{\emptyset\}) \| (⋃ s = F^{-1} [k] \land \forall c \in s (\forall d \in (s ∖ \{c\}) c \cap d = \emptyset \land {F ↾}_{c} \in ((C ↾_{𝑡} c) Homeo (J ↾_{𝑡} k))))\})$
12		cvmlift3lem7.1	$⊢ φ \to G (X) \in A$
13		cvmlift3lem7.2	$⊢ φ \to T \in S (A)$
14		cvmlift3lem7.3	$⊢ φ \to M \subseteq G^{-1} [A]$
15		cvmlift3lem7.w	$⊢ W = (ι b \in T \| H (X) \in b)$
16		cvmlift3lem6.x	$⊢ φ \to X \in M$
17		cvmlift3lem6.z	$⊢ φ \to Z \in M$
18		cvmlift3lem6.q	$⊢ φ \to Q \in (II Cn K)$
19		cvmlift3lem6.r	$⊢ R = (ι g \in (II Cn C) \| (F \circ g = G \circ Q \land g (0) = P))$
20		cvmlift3lem6.1	$⊢ φ \to (Q (0) = O \land Q (1) = X \land R (1) = H (X))$
21		cvmlift3lem6.n	$⊢ φ \to N \in (II Cn (K ↾_{𝑡} M))$
22		cvmlift3lem6.2	$⊢ φ \to (N (0) = X \land N (1) = Z)$
23		cvmlift3lem6.i	$⊢ I = (ι g \in (II Cn C) \| (F \circ g = G \circ N \land g (0) = H (X)))$
24		sconntop	$⊢ K \in SConn \to K \in Top$
25	4 24	syl	$⊢ φ \to K \in Top$
26		cnrest2r	$⊢ K \in Top \to II Cn (K ↾_{𝑡} M) \subseteq II Cn K$
27	25 26	syl	$⊢ φ \to II Cn (K ↾_{𝑡} M) \subseteq II Cn K$
28	27 21	sseldd	$⊢ φ \to N \in (II Cn K)$
29	20	simp2d	$⊢ φ \to Q (1) = X$
30	22	simpld	$⊢ φ \to N (0) = X$
31	29 30	eqtr4d	$⊢ φ \to Q (1) = N (0)$
32	18 28 31	pcocn	$⊢ φ \to Q *_{𝑝} (K) N \in (II Cn K)$
33	18 28	pco0	$⊢ φ \to (Q *_{𝑝} (K) N) (0) = Q (0)$
34	20	simp1d	$⊢ φ \to Q (0) = O$
35	33 34	eqtrd	$⊢ φ \to (Q *_{𝑝} (K) N) (0) = O$
36	18 28	pco1	$⊢ φ \to (Q *_{𝑝} (K) N) (1) = N (1)$
37	22	simprd	$⊢ φ \to N (1) = Z$
38	36 37	eqtrd	$⊢ φ \to (Q *_{𝑝} (K) N) (1) = Z$
39		cnco	$⊢ (Q \in (II Cn K) \land G \in (K Cn J)) \to G \circ Q \in (II Cn J)$
40	18 7 39	syl2anc	$⊢ φ \to G \circ Q \in (II Cn J)$
41	34	fveq2d	$⊢ φ \to G (Q (0)) = G (O)$
42		iiuni	$⊢ [0, 1] = ⋃ II$
43	42 2	cnf	$⊢ Q \in (II Cn K) \to Q : [0, 1] ⟶ Y$
44	18 43	syl	$⊢ φ \to Q : [0, 1] ⟶ Y$
45		0elunit	$⊢ 0 \in [0, 1]$
46		fvco3	$⊢ (Q : [0, 1] ⟶ Y \land 0 \in [0, 1]) \to (G \circ Q) (0) = G (Q (0))$
47	44 45 46	sylancl	$⊢ φ \to (G \circ Q) (0) = G (Q (0))$
48	41 47 9	3eqtr4rd	$⊢ φ \to F (P) = (G \circ Q) (0)$
49	1 19 3 40 8 48	cvmliftiota	$⊢ φ \to (R \in (II Cn C) \land F \circ R = G \circ Q \land R (0) = P)$
50	49	simp2d	$⊢ φ \to F \circ R = G \circ Q$
51		cnco	$⊢ (N \in (II Cn K) \land G \in (K Cn J)) \to G \circ N \in (II Cn J)$
52	28 7 51	syl2anc	$⊢ φ \to G \circ N \in (II Cn J)$
53	1 2 3 4 5 6 7 8 9 10	cvmlift3lem3	$⊢ φ \to H : Y ⟶ B$
54		cnvimass	$⊢ G^{-1} [A] \subseteq dom G$
55		eqid	$⊢ ⋃ J = ⋃ J$
56	2 55	cnf	$⊢ G \in (K Cn J) \to G : Y ⟶ ⋃ J$
57	7 56	syl	$⊢ φ \to G : Y ⟶ ⋃ J$
58	54 57	fssdm	$⊢ φ \to G^{-1} [A] \subseteq Y$
59	14 58	sstrd	$⊢ φ \to M \subseteq Y$
60	59 16	sseldd	$⊢ φ \to X \in Y$
61	53 60	ffvelrnd	$⊢ φ \to H (X) \in B$
62	30	fveq2d	$⊢ φ \to G (N (0)) = G (X)$
63	42 2	cnf	$⊢ N \in (II Cn K) \to N : [0, 1] ⟶ Y$
64	28 63	syl	$⊢ φ \to N : [0, 1] ⟶ Y$
65		fvco3	$⊢ (N : [0, 1] ⟶ Y \land 0 \in [0, 1]) \to (G \circ N) (0) = G (N (0))$
66	64 45 65	sylancl	$⊢ φ \to (G \circ N) (0) = G (N (0))$
67		fvco3	$⊢ (H : Y ⟶ B \land X \in Y) \to (F \circ H) (X) = F (H (X))$
68	53 60 67	syl2anc	$⊢ φ \to (F \circ H) (X) = F (H (X))$
69	1 2 3 4 5 6 7 8 9 10	cvmlift3lem5	$⊢ φ \to F \circ H = G$
70	69	fveq1d	$⊢ φ \to (F \circ H) (X) = G (X)$
71	68 70	eqtr3d	$⊢ φ \to F (H (X)) = G (X)$
72	62 66 71	3eqtr4rd	$⊢ φ \to F (H (X)) = (G \circ N) (0)$
73	1 23 3 52 61 72	cvmliftiota	$⊢ φ \to (I \in (II Cn C) \land F \circ I = G \circ N \land I (0) = H (X))$
74	73	simp2d	$⊢ φ \to F \circ I = G \circ N$
75	50 74	oveq12d	$⊢ φ \to (F \circ R) _{𝑝} (J) (F \circ I) = (G \circ Q) _{𝑝} (J) (G \circ N)$
76	49	simp1d	$⊢ φ \to R \in (II Cn C)$
77	73	simp1d	$⊢ φ \to I \in (II Cn C)$
78	20	simp3d	$⊢ φ \to R (1) = H (X)$
79	73	simp3d	$⊢ φ \to I (0) = H (X)$
80	78 79	eqtr4d	$⊢ φ \to R (1) = I (0)$
81		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
82	3 81	syl	$⊢ φ \to F \in (C Cn J)$
83	76 77 80 82	copco	$⊢ φ \to F \circ (R _{𝑝} (C) I) = (F \circ R) _{𝑝} (J) (F \circ I)$
84	18 28 31 7	copco	$⊢ φ \to G \circ (Q _{𝑝} (K) N) = (G \circ Q) _{𝑝} (J) (G \circ N)$
85	75 83 84	3eqtr4d	$⊢ φ \to F \circ (R _{𝑝} (C) I) = G \circ (Q _{𝑝} (K) N)$
86	76 77	pco0	$⊢ φ \to (R *_{𝑝} (C) I) (0) = R (0)$
87	49	simp3d	$⊢ φ \to R (0) = P$
88	86 87	eqtrd	$⊢ φ \to (R *_{𝑝} (C) I) (0) = P$
89	76 77 80	pcocn	$⊢ φ \to R *_{𝑝} (C) I \in (II Cn C)$
90		cnco	$⊢ (Q _{𝑝} (K) N \in (II Cn K) \land G \in (K Cn J)) \to G \circ (Q _{𝑝} (K) N) \in (II Cn J)$
91	32 7 90	syl2anc	$⊢ φ \to G \circ (Q *_{𝑝} (K) N) \in (II Cn J)$
92	35	fveq2d	$⊢ φ \to G ((Q *_{𝑝} (K) N) (0)) = G (O)$
93	42 2	cnf	$⊢ Q _{𝑝} (K) N \in (II Cn K) \to (Q _{𝑝} (K) N) : [0, 1] ⟶ Y$
94	32 93	syl	$⊢ φ \to (Q *_{𝑝} (K) N) : [0, 1] ⟶ Y$
95		fvco3	$⊢ ((Q _{𝑝} (K) N) : [0, 1] ⟶ Y \land 0 \in [0, 1]) \to (G \circ (Q _{𝑝} (K) N)) (0) = G ((Q *_{𝑝} (K) N) (0))$
96	94 45 95	sylancl	$⊢ φ \to (G \circ (Q _{𝑝} (K) N)) (0) = G ((Q _{𝑝} (K) N) (0))$
97	92 96 9	3eqtr4rd	$⊢ φ \to F (P) = (G \circ (Q *_{𝑝} (K) N)) (0)$
98	1	cvmlift	$⊢ ((F \in (C CovMap J) \land G \circ (Q _{𝑝} (K) N) \in (II Cn J)) \land (P \in B \land F (P) = (G \circ (Q _{𝑝} (K) N)) (0))) \to \exists! g \in (II Cn C) (F \circ g = G \circ (Q *_{𝑝} (K) N) \land g (0) = P)$
99	3 91 8 97 98	syl22anc	$⊢ φ \to \exists! g \in (II Cn C) (F \circ g = G \circ (Q *_{𝑝} (K) N) \land g (0) = P)$
100		coeq2	$⊢ g = R _{𝑝} (C) I \to F \circ g = F \circ (R _{𝑝} (C) I)$
101	100	eqeq1d	$⊢ g = R _{𝑝} (C) I \to (F \circ g = G \circ (Q _{𝑝} (K) N) \leftrightarrow F \circ (R _{𝑝} (C) I) = G \circ (Q _{𝑝} (K) N))$
102		fveq1	$⊢ g = R _{𝑝} (C) I \to g (0) = (R _{𝑝} (C) I) (0)$
103	102	eqeq1d	$⊢ g = R _{𝑝} (C) I \to (g (0) = P \leftrightarrow (R _{𝑝} (C) I) (0) = P)$
104	101 103	anbi12d	$⊢ g = R _{𝑝} (C) I \to ((F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P) \leftrightarrow (F \circ (R _{𝑝} (C) I) = G \circ (Q _{𝑝} (K) N) \land (R *_{𝑝} (C) I) (0) = P))$
105	104	riota2	$⊢ (R _{𝑝} (C) I \in (II Cn C) \land \exists! g \in (II Cn C) (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P)) \to ((F \circ (R _{𝑝} (C) I) = G \circ (Q _{𝑝} (K) N) \land (R _{𝑝} (C) I) (0) = P) \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P)) = R *_{𝑝} (C) I)$
106	89 99 105	syl2anc	$⊢ φ \to ((F \circ (R _{𝑝} (C) I) = G \circ (Q _{𝑝} (K) N) \land (R _{𝑝} (C) I) (0) = P) \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P)) = R *_{𝑝} (C) I)$
107	85 88 106	mpbi2and	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P)) = R _{𝑝} (C) I$
108	107	fveq1d	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P)) (1) = (R _{𝑝} (C) I) (1)$
109	76 77	pco1	$⊢ φ \to (R *_{𝑝} (C) I) (1) = I (1)$
110	108 109	eqtrd	$⊢ φ \to (ι g \in (II Cn C) \| (F \circ g = G \circ (Q *_{𝑝} (K) N) \land g (0) = P)) (1) = I (1)$
111		fveq1	$⊢ f = Q _{𝑝} (K) N \to f (0) = (Q _{𝑝} (K) N) (0)$
112	111	eqeq1d	$⊢ f = Q _{𝑝} (K) N \to (f (0) = O \leftrightarrow (Q _{𝑝} (K) N) (0) = O)$
113		fveq1	$⊢ f = Q _{𝑝} (K) N \to f (1) = (Q _{𝑝} (K) N) (1)$
114	113	eqeq1d	$⊢ f = Q _{𝑝} (K) N \to (f (1) = Z \leftrightarrow (Q _{𝑝} (K) N) (1) = Z)$
115		coeq2	$⊢ f = Q _{𝑝} (K) N \to G \circ f = G \circ (Q _{𝑝} (K) N)$
116	115	eqeq2d	$⊢ f = Q _{𝑝} (K) N \to (F \circ g = G \circ f \leftrightarrow F \circ g = G \circ (Q _{𝑝} (K) N))$
117	116	anbi1d	$⊢ f = Q _{𝑝} (K) N \to ((F \circ g = G \circ f \land g (0) = P) \leftrightarrow (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P))$
118	117	riotabidv	$⊢ f = Q _{𝑝} (K) N \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) = (ι g \in (II Cn C) \| (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P))$
119	118	fveq1d	$⊢ f = Q _{𝑝} (K) N \to (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = (ι g \in (II Cn C) \| (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P)) (1)$
120	119	eqeq1d	$⊢ f = Q _{𝑝} (K) N \to ((ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = I (1) \leftrightarrow (ι g \in (II Cn C) \| (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P)) (1) = I (1))$
121	112 114 120	3anbi123d	$⊢ f = Q _{𝑝} (K) N \to ((f (0) = O \land f (1) = Z \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = I (1)) \leftrightarrow ((Q _{𝑝} (K) N) (0) = O \land (Q _{𝑝} (K) N) (1) = Z \land (ι g \in (II Cn C) \| (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P)) (1) = I (1)))$
122	121	rspcev	$⊢ (Q _{𝑝} (K) N \in (II Cn K) \land ((Q _{𝑝} (K) N) (0) = O \land (Q _{𝑝} (K) N) (1) = Z \land (ι g \in (II Cn C) \| (F \circ g = G \circ (Q _{𝑝} (K) N) \land g (0) = P)) (1) = I (1))) \to \exists f \in (II Cn K) (f (0) = O \land f (1) = Z \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = I (1))$
123	32 35 38 110 122	syl13anc	$⊢ φ \to \exists f \in (II Cn K) (f (0) = O \land f (1) = Z \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = I (1))$
124	59 17	sseldd	$⊢ φ \to Z \in Y$
125	1 2 3 4 5 6 7 8 9 10	cvmlift3lem4	$⊢ (φ \land Z \in Y) \to (H (Z) = I (1) \leftrightarrow \exists f \in (II Cn K) (f (0) = O \land f (1) = Z \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = I (1)))$
126	124 125	mpdan	$⊢ φ \to (H (Z) = I (1) \leftrightarrow \exists f \in (II Cn K) (f (0) = O \land f (1) = Z \land (ι g \in (II Cn C) \| (F \circ g = G \circ f \land g (0) = P)) (1) = I (1)))$
127	123 126	mpbird	$⊢ φ \to H (Z) = I (1)$
128		iiconn	$⊢ II \in Conn$
129	128	a1i	$⊢ φ \to II \in Conn$
130		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
131	3 130	syl	$⊢ φ \to C \in Top$
132	1	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (B)$
133	131 132	sylib	$⊢ φ \to C \in TopOn (B)$
134	74	rneqd	$⊢ φ \to ran (F \circ I) = ran (G \circ N)$
135		rnco2	$⊢ ran (F \circ I) = F [ran I]$
136		rnco2	$⊢ ran (G \circ N) = G [ran N]$
137	134 135 136	3eqtr3g	$⊢ φ \to F [ran I] = G [ran N]$
138		iitopon	$⊢ II \in TopOn ([0, 1])$
139	138	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
140	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
141	25 140	sylib	$⊢ φ \to K \in TopOn (Y)$
142		resttopon	$⊢ (K \in TopOn (Y) \land M \subseteq Y) \to K ↾_{𝑡} M \in TopOn (M)$
143	141 59 142	syl2anc	$⊢ φ \to K ↾_{𝑡} M \in TopOn (M)$
144		cnf2	$⊢ (II \in TopOn ([0, 1]) \land K ↾_{𝑡} M \in TopOn (M) \land N \in (II Cn (K ↾_{𝑡} M))) \to N : [0, 1] ⟶ M$
145	139 143 21 144	syl3anc	$⊢ φ \to N : [0, 1] ⟶ M$
146	145	frnd	$⊢ φ \to ran N \subseteq M$
147	146 14	sstrd	$⊢ φ \to ran N \subseteq G^{-1} [A]$
148	57	ffund	$⊢ φ \to Fun G$
149	147 54	sstrdi	$⊢ φ \to ran N \subseteq dom G$
150		funimass3	$⊢ (Fun G \land ran N \subseteq dom G) \to (G [ran N] \subseteq A \leftrightarrow ran N \subseteq G^{-1} [A])$
151	148 149 150	syl2anc	$⊢ φ \to (G [ran N] \subseteq A \leftrightarrow ran N \subseteq G^{-1} [A])$
152	147 151	mpbird	$⊢ φ \to G [ran N] \subseteq A$
153	137 152	eqsstrd	$⊢ φ \to F [ran I] \subseteq A$
154	1 55	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ ⋃ J$
155	82 154	syl	$⊢ φ \to F : B ⟶ ⋃ J$
156	155	ffund	$⊢ φ \to Fun F$
157	42 1	cnf	$⊢ I \in (II Cn C) \to I : [0, 1] ⟶ B$
158	77 157	syl	$⊢ φ \to I : [0, 1] ⟶ B$
159	158	frnd	$⊢ φ \to ran I \subseteq B$
160	155	fdmd	$⊢ φ \to dom F = B$
161	159 160	sseqtrrd	$⊢ φ \to ran I \subseteq dom F$
162		funimass3	$⊢ (Fun F \land ran I \subseteq dom F) \to (F [ran I] \subseteq A \leftrightarrow ran I \subseteq F^{-1} [A])$
163	156 161 162	syl2anc	$⊢ φ \to (F [ran I] \subseteq A \leftrightarrow ran I \subseteq F^{-1} [A])$
164	153 163	mpbid	$⊢ φ \to ran I \subseteq F^{-1} [A]$
165		cnvimass	$⊢ F^{-1} [A] \subseteq dom F$
166	165 155	fssdm	$⊢ φ \to F^{-1} [A] \subseteq B$
167		cnrest2	$⊢ (C \in TopOn (B) \land ran I \subseteq F^{-1} [A] \land F^{-1} [A] \subseteq B) \to (I \in (II Cn C) \leftrightarrow I \in (II Cn (C ↾_{𝑡} F^{-1} [A])))$
168	133 164 166 167	syl3anc	$⊢ φ \to (I \in (II Cn C) \leftrightarrow I \in (II Cn (C ↾_{𝑡} F^{-1} [A])))$
169	77 168	mpbid	$⊢ φ \to I \in (II Cn (C ↾_{𝑡} F^{-1} [A]))$
170	11	cvmsss	$⊢ T \in S (A) \to T \subseteq C$
171	13 170	syl	$⊢ φ \to T \subseteq C$
172	71 12	eqeltrd	$⊢ φ \to F (H (X)) \in A$
173	11 1 15	cvmsiota	$⊢ (F \in (C CovMap J) \land (T \in S (A) \land H (X) \in B \land F (H (X)) \in A)) \to (W \in T \land H (X) \in W)$
174	3 13 61 172 173	syl13anc	$⊢ φ \to (W \in T \land H (X) \in W)$
175	174	simpld	$⊢ φ \to W \in T$
176	171 175	sseldd	$⊢ φ \to W \in C$
177		elssuni	$⊢ W \in T \to W \subseteq ⋃ T$
178	175 177	syl	$⊢ φ \to W \subseteq ⋃ T$
179	11	cvmsuni	$⊢ T \in S (A) \to ⋃ T = F^{-1} [A]$
180	13 179	syl	$⊢ φ \to ⋃ T = F^{-1} [A]$
181	178 180	sseqtrd	$⊢ φ \to W \subseteq F^{-1} [A]$
182	11	cvmsrcl	$⊢ T \in S (A) \to A \in J$
183	13 182	syl	$⊢ φ \to A \in J$
184		cnima	$⊢ (F \in (C Cn J) \land A \in J) \to F^{-1} [A] \in C$
185	82 183 184	syl2anc	$⊢ φ \to F^{-1} [A] \in C$
186		restopn2	$⊢ (C \in Top \land F^{-1} [A] \in C) \to (W \in (C ↾_{𝑡} F^{-1} [A]) \leftrightarrow (W \in C \land W \subseteq F^{-1} [A]))$
187	131 185 186	syl2anc	$⊢ φ \to (W \in (C ↾_{𝑡} F^{-1} [A]) \leftrightarrow (W \in C \land W \subseteq F^{-1} [A]))$
188	176 181 187	mpbir2and	$⊢ φ \to W \in (C ↾_{𝑡} F^{-1} [A])$
189	11	cvmscld	$⊢ (F \in (C CovMap J) \land T \in S (A) \land W \in T) \to W \in Clsd (C ↾_{𝑡} F^{-1} [A])$
190	3 13 175 189	syl3anc	$⊢ φ \to W \in Clsd (C ↾_{𝑡} F^{-1} [A])$
191	45	a1i	$⊢ φ \to 0 \in [0, 1]$
192	174	simprd	$⊢ φ \to H (X) \in W$
193	79 192	eqeltrd	$⊢ φ \to I (0) \in W$
194	42 129 169 188 190 191 193	conncn	$⊢ φ \to I : [0, 1] ⟶ W$
195		1elunit	$⊢ 1 \in [0, 1]$
196		ffvelrn	$⊢ (I : [0, 1] ⟶ W \land 1 \in [0, 1]) \to I (1) \in W$
197	194 195 196	sylancl	$⊢ φ \to I (1) \in W$
198	127 197	eqeltrd	$⊢ φ \to H (Z) \in W$

Metamath Proof Explorer

Theorem cvmlift3lem6

Proof