cvmliftphtlem

	Ref	Expression
Hypotheses	cvmliftpht.b	$⊢ B = ⋃ C$
	cvmliftpht.m	$⊢ M = (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P))$
	cvmliftpht.n	$⊢ N = (ι f \in (II Cn C) \| (F \circ f = H \land f (0) = P))$
	cvmliftpht.f	$⊢ φ \to F \in (C CovMap J)$
	cvmliftpht.p	$⊢ φ \to P \in B$
	cvmliftpht.e	$⊢ φ \to F (P) = G (0)$
	cvmliftphtlem.g	$⊢ φ \to G \in (II Cn J)$
	cvmliftphtlem.h	$⊢ φ \to H \in (II Cn J)$
	cvmliftphtlem.k	$⊢ φ \to K \in (G PHtpy (J) H)$
	cvmliftphtlem.a	$⊢ φ \to A \in ((II \times_{t} II) Cn C)$
	cvmliftphtlem.c	$⊢ φ \to F \circ A = K$
	cvmliftphtlem.0	$⊢ φ \to 0 A 0 = P$
Assertion	cvmliftphtlem	$⊢ φ \to A \in (M PHtpy (C) N)$

Proof

Step	Hyp	Ref	Expression
1		cvmliftpht.b	$⊢ B = ⋃ C$
2		cvmliftpht.m	$⊢ M = (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P))$
3		cvmliftpht.n	$⊢ N = (ι f \in (II Cn C) \| (F \circ f = H \land f (0) = P))$
4		cvmliftpht.f	$⊢ φ \to F \in (C CovMap J)$
5		cvmliftpht.p	$⊢ φ \to P \in B$
6		cvmliftpht.e	$⊢ φ \to F (P) = G (0)$
7		cvmliftphtlem.g	$⊢ φ \to G \in (II Cn J)$
8		cvmliftphtlem.h	$⊢ φ \to H \in (II Cn J)$
9		cvmliftphtlem.k	$⊢ φ \to K \in (G PHtpy (J) H)$
10		cvmliftphtlem.a	$⊢ φ \to A \in ((II \times_{t} II) Cn C)$
11		cvmliftphtlem.c	$⊢ φ \to F \circ A = K$
12		cvmliftphtlem.0	$⊢ φ \to 0 A 0 = P$
13	1 2 4 7 5 6	cvmliftiota	$⊢ φ \to (M \in (II Cn C) \land F \circ M = G \land M (0) = P)$
14	13	simp1d	$⊢ φ \to M \in (II Cn C)$
15	7 8 9	phtpy01	$⊢ φ \to (G (0) = H (0) \land G (1) = H (1))$
16	15	simpld	$⊢ φ \to G (0) = H (0)$
17	6 16	eqtrd	$⊢ φ \to F (P) = H (0)$
18	1 3 4 8 5 17	cvmliftiota	$⊢ φ \to (N \in (II Cn C) \land F \circ N = H \land N (0) = P)$
19	18	simp1d	$⊢ φ \to N \in (II Cn C)$
20		iitop	$⊢ II \in Top$
21		iiuni	$⊢ [0, 1] = ⋃ II$
22	20 20 21 21	txunii	$⊢ [0, 1] \times [0, 1] = ⋃ (II \times_{t} II)$
23	22 1	cnf	$⊢ A \in ((II \times_{t} II) Cn C) \to A : [0, 1] \times [0, 1] ⟶ B$
24	10 23	syl	$⊢ φ \to A : [0, 1] \times [0, 1] ⟶ B$
25		0elunit	$⊢ 0 \in [0, 1]$
26		opelxpi	$⊢ (s \in [0, 1] \land 0 \in [0, 1]) \to ⟨s, 0⟩ \in ([0, 1] \times [0, 1])$
27	25 26	mpan2	$⊢ s \in [0, 1] \to ⟨s, 0⟩ \in ([0, 1] \times [0, 1])$
28		fvco3	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land ⟨s, 0⟩ \in ([0, 1] \times [0, 1])) \to (F \circ A) (⟨s, 0⟩) = F (A (⟨s, 0⟩))$
29	24 27 28	syl2an	$⊢ (φ \land s \in [0, 1]) \to (F \circ A) (⟨s, 0⟩) = F (A (⟨s, 0⟩))$
30	11	adantr	$⊢ (φ \land s \in [0, 1]) \to F \circ A = K$
31	30	fveq1d	$⊢ (φ \land s \in [0, 1]) \to (F \circ A) (⟨s, 0⟩) = K (⟨s, 0⟩)$
32	29 31	eqtr3d	$⊢ (φ \land s \in [0, 1]) \to F (A (⟨s, 0⟩)) = K (⟨s, 0⟩)$
33		df-ov	$⊢ s A 0 = A (⟨s, 0⟩)$
34	33	fveq2i	$⊢ F (s A 0) = F (A (⟨s, 0⟩))$
35		df-ov	$⊢ s K 0 = K (⟨s, 0⟩)$
36	32 34 35	3eqtr4g	$⊢ (φ \land s \in [0, 1]) \to F (s A 0) = s K 0$
37		iitopon	$⊢ II \in TopOn ([0, 1])$
38	37	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
39	7 8	phtpyhtpy	$⊢ φ \to G PHtpy (J) H \subseteq G (II Htpy J) H$
40	39 9	sseldd	$⊢ φ \to K \in (G (II Htpy J) H)$
41	38 7 8 40	htpyi	$⊢ (φ \land s \in [0, 1]) \to (s K 0 = G (s) \land s K 1 = H (s))$
42	41	simpld	$⊢ (φ \land s \in [0, 1]) \to s K 0 = G (s)$
43	36 42	eqtrd	$⊢ (φ \land s \in [0, 1]) \to F (s A 0) = G (s)$
44	43	mpteq2dva	$⊢ φ \to (s \in [0, 1] ⟼ F (s A 0)) = (s \in [0, 1] ⟼ G (s))$
45		fovrn	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land s \in [0, 1] \land 0 \in [0, 1]) \to s A 0 \in B$
46	25 45	mp3an3	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land s \in [0, 1]) \to s A 0 \in B$
47	24 46	sylan	$⊢ (φ \land s \in [0, 1]) \to s A 0 \in B$
48		eqidd	$⊢ φ \to (s \in [0, 1] ⟼ s A 0) = (s \in [0, 1] ⟼ s A 0)$
49		cvmcn	$⊢ F \in (C CovMap J) \to F \in (C Cn J)$
50	4 49	syl	$⊢ φ \to F \in (C Cn J)$
51		eqid	$⊢ ⋃ J = ⋃ J$
52	1 51	cnf	$⊢ F \in (C Cn J) \to F : B ⟶ ⋃ J$
53	50 52	syl	$⊢ φ \to F : B ⟶ ⋃ J$
54	53	feqmptd	$⊢ φ \to F = (x \in B ⟼ F (x))$
55		fveq2	$⊢ x = s A 0 \to F (x) = F (s A 0)$
56	47 48 54 55	fmptco	$⊢ φ \to F \circ (s \in [0, 1] ⟼ s A 0) = (s \in [0, 1] ⟼ F (s A 0))$
57	21 51	cnf	$⊢ G \in (II Cn J) \to G : [0, 1] ⟶ ⋃ J$
58	7 57	syl	$⊢ φ \to G : [0, 1] ⟶ ⋃ J$
59	58	feqmptd	$⊢ φ \to G = (s \in [0, 1] ⟼ G (s))$
60	44 56 59	3eqtr4d	$⊢ φ \to F \circ (s \in [0, 1] ⟼ s A 0) = G$
61	38	cnmptid	$⊢ φ \to (s \in [0, 1] ⟼ s) \in (II Cn II)$
62	25	a1i	$⊢ φ \to 0 \in [0, 1]$
63	38 38 62	cnmptc	$⊢ φ \to (s \in [0, 1] ⟼ 0) \in (II Cn II)$
64	38 61 63 10	cnmpt12f	$⊢ φ \to (s \in [0, 1] ⟼ s A 0) \in (II Cn C)$
65	1	cvmlift	$⊢ ((F \in (C CovMap J) \land G \in (II Cn J)) \land (P \in B \land F (P) = G (0))) \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P)$
66	4 7 5 6 65	syl22anc	$⊢ φ \to \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P)$
67		coeq2	$⊢ f = (s \in [0, 1] ⟼ s A 0) \to F \circ f = F \circ (s \in [0, 1] ⟼ s A 0)$
68	67	eqeq1d	$⊢ f = (s \in [0, 1] ⟼ s A 0) \to (F \circ f = G \leftrightarrow F \circ (s \in [0, 1] ⟼ s A 0) = G)$
69		fveq1	$⊢ f = (s \in [0, 1] ⟼ s A 0) \to f (0) = (s \in [0, 1] ⟼ s A 0) (0)$
70		oveq1	$⊢ s = 0 \to s A 0 = 0 A 0$
71		eqid	$⊢ (s \in [0, 1] ⟼ s A 0) = (s \in [0, 1] ⟼ s A 0)$
72		ovex	$⊢ 0 A 0 \in V$
73	70 71 72	fvmpt	$⊢ 0 \in [0, 1] \to (s \in [0, 1] ⟼ s A 0) (0) = 0 A 0$
74	25 73	ax-mp	$⊢ (s \in [0, 1] ⟼ s A 0) (0) = 0 A 0$
75	69 74	eqtrdi	$⊢ f = (s \in [0, 1] ⟼ s A 0) \to f (0) = 0 A 0$
76	75	eqeq1d	$⊢ f = (s \in [0, 1] ⟼ s A 0) \to (f (0) = P \leftrightarrow 0 A 0 = P)$
77	68 76	anbi12d	$⊢ f = (s \in [0, 1] ⟼ s A 0) \to ((F \circ f = G \land f (0) = P) \leftrightarrow (F \circ (s \in [0, 1] ⟼ s A 0) = G \land 0 A 0 = P))$
78	77	riota2	$⊢ ((s \in [0, 1] ⟼ s A 0) \in (II Cn C) \land \exists! f \in (II Cn C) (F \circ f = G \land f (0) = P)) \to ((F \circ (s \in [0, 1] ⟼ s A 0) = G \land 0 A 0 = P) \leftrightarrow (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P)) = (s \in [0, 1] ⟼ s A 0))$
79	64 66 78	syl2anc	$⊢ φ \to ((F \circ (s \in [0, 1] ⟼ s A 0) = G \land 0 A 0 = P) \leftrightarrow (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P)) = (s \in [0, 1] ⟼ s A 0))$
80	60 12 79	mpbi2and	$⊢ φ \to (ι f \in (II Cn C) \| (F \circ f = G \land f (0) = P)) = (s \in [0, 1] ⟼ s A 0)$
81	2 80	syl5eq	$⊢ φ \to M = (s \in [0, 1] ⟼ s A 0)$
82	21 1	cnf	$⊢ M \in (II Cn C) \to M : [0, 1] ⟶ B$
83	14 82	syl	$⊢ φ \to M : [0, 1] ⟶ B$
84	83	feqmptd	$⊢ φ \to M = (s \in [0, 1] ⟼ M (s))$
85	81 84	eqtr3d	$⊢ φ \to (s \in [0, 1] ⟼ s A 0) = (s \in [0, 1] ⟼ M (s))$
86		mpteqb	$⊢ \forall s \in [0, 1] s A 0 \in V \to ((s \in [0, 1] ⟼ s A 0) = (s \in [0, 1] ⟼ M (s)) \leftrightarrow \forall s \in [0, 1] s A 0 = M (s))$
87		ovexd	$⊢ s \in [0, 1] \to s A 0 \in V$
88	86 87	mprg	$⊢ (s \in [0, 1] ⟼ s A 0) = (s \in [0, 1] ⟼ M (s)) \leftrightarrow \forall s \in [0, 1] s A 0 = M (s)$
89	85 88	sylib	$⊢ φ \to \forall s \in [0, 1] s A 0 = M (s)$
90	89	r19.21bi	$⊢ (φ \land s \in [0, 1]) \to s A 0 = M (s)$
91		1elunit	$⊢ 1 \in [0, 1]$
92		opelxpi	$⊢ (s \in [0, 1] \land 1 \in [0, 1]) \to ⟨s, 1⟩ \in ([0, 1] \times [0, 1])$
93	91 92	mpan2	$⊢ s \in [0, 1] \to ⟨s, 1⟩ \in ([0, 1] \times [0, 1])$
94		fvco3	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land ⟨s, 1⟩ \in ([0, 1] \times [0, 1])) \to (F \circ A) (⟨s, 1⟩) = F (A (⟨s, 1⟩))$
95	24 93 94	syl2an	$⊢ (φ \land s \in [0, 1]) \to (F \circ A) (⟨s, 1⟩) = F (A (⟨s, 1⟩))$
96	30	fveq1d	$⊢ (φ \land s \in [0, 1]) \to (F \circ A) (⟨s, 1⟩) = K (⟨s, 1⟩)$
97	95 96	eqtr3d	$⊢ (φ \land s \in [0, 1]) \to F (A (⟨s, 1⟩)) = K (⟨s, 1⟩)$
98		df-ov	$⊢ s A 1 = A (⟨s, 1⟩)$
99	98	fveq2i	$⊢ F (s A 1) = F (A (⟨s, 1⟩))$
100		df-ov	$⊢ s K 1 = K (⟨s, 1⟩)$
101	97 99 100	3eqtr4g	$⊢ (φ \land s \in [0, 1]) \to F (s A 1) = s K 1$
102	41	simprd	$⊢ (φ \land s \in [0, 1]) \to s K 1 = H (s)$
103	101 102	eqtrd	$⊢ (φ \land s \in [0, 1]) \to F (s A 1) = H (s)$
104	103	mpteq2dva	$⊢ φ \to (s \in [0, 1] ⟼ F (s A 1)) = (s \in [0, 1] ⟼ H (s))$
105		fovrn	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land s \in [0, 1] \land 1 \in [0, 1]) \to s A 1 \in B$
106	91 105	mp3an3	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land s \in [0, 1]) \to s A 1 \in B$
107	24 106	sylan	$⊢ (φ \land s \in [0, 1]) \to s A 1 \in B$
108		eqidd	$⊢ φ \to (s \in [0, 1] ⟼ s A 1) = (s \in [0, 1] ⟼ s A 1)$
109		fveq2	$⊢ x = s A 1 \to F (x) = F (s A 1)$
110	107 108 54 109	fmptco	$⊢ φ \to F \circ (s \in [0, 1] ⟼ s A 1) = (s \in [0, 1] ⟼ F (s A 1))$
111	21 51	cnf	$⊢ H \in (II Cn J) \to H : [0, 1] ⟶ ⋃ J$
112	8 111	syl	$⊢ φ \to H : [0, 1] ⟶ ⋃ J$
113	112	feqmptd	$⊢ φ \to H = (s \in [0, 1] ⟼ H (s))$
114	104 110 113	3eqtr4d	$⊢ φ \to F \circ (s \in [0, 1] ⟼ s A 1) = H$
115		iiconn	$⊢ II \in Conn$
116	115	a1i	$⊢ φ \to II \in Conn$
117		iinllyconn	$⊢ II \in N-LocallyConn$
118	117	a1i	$⊢ φ \to II \in N-LocallyConn$
119	38 63 61 10	cnmpt12f	$⊢ φ \to (s \in [0, 1] ⟼ 0 A s) \in (II Cn C)$
120		cvmtop1	$⊢ F \in (C CovMap J) \to C \in Top$
121	4 120	syl	$⊢ φ \to C \in Top$
122	1	toptopon	$⊢ C \in Top \leftrightarrow C \in TopOn (B)$
123	121 122	sylib	$⊢ φ \to C \in TopOn (B)$
124		ffvelrn	$⊢ (M : [0, 1] ⟶ B \land 0 \in [0, 1]) \to M (0) \in B$
125	83 25 124	sylancl	$⊢ φ \to M (0) \in B$
126		cnconst2	$⊢ (II \in TopOn ([0, 1]) \land C \in TopOn (B) \land M (0) \in B) \to [0, 1] \times \{M (0)\} \in (II Cn C)$
127	38 123 125 126	syl3anc	$⊢ φ \to [0, 1] \times \{M (0)\} \in (II Cn C)$
128	7 8 9	phtpyi	$⊢ (φ \land s \in [0, 1]) \to (0 K s = G (0) \land 1 K s = G (1))$
129	128	simpld	$⊢ (φ \land s \in [0, 1]) \to 0 K s = G (0)$
130		opelxpi	$⊢ (0 \in [0, 1] \land s \in [0, 1]) \to ⟨0, s⟩ \in ([0, 1] \times [0, 1])$
131	25 130	mpan	$⊢ s \in [0, 1] \to ⟨0, s⟩ \in ([0, 1] \times [0, 1])$
132		fvco3	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land ⟨0, s⟩ \in ([0, 1] \times [0, 1])) \to (F \circ A) (⟨0, s⟩) = F (A (⟨0, s⟩))$
133	24 131 132	syl2an	$⊢ (φ \land s \in [0, 1]) \to (F \circ A) (⟨0, s⟩) = F (A (⟨0, s⟩))$
134	30	fveq1d	$⊢ (φ \land s \in [0, 1]) \to (F \circ A) (⟨0, s⟩) = K (⟨0, s⟩)$
135	133 134	eqtr3d	$⊢ (φ \land s \in [0, 1]) \to F (A (⟨0, s⟩)) = K (⟨0, s⟩)$
136		df-ov	$⊢ 0 A s = A (⟨0, s⟩)$
137	136	fveq2i	$⊢ F (0 A s) = F (A (⟨0, s⟩))$
138		df-ov	$⊢ 0 K s = K (⟨0, s⟩)$
139	135 137 138	3eqtr4g	$⊢ (φ \land s \in [0, 1]) \to F (0 A s) = 0 K s$
140	13	simp3d	$⊢ φ \to M (0) = P$
141	140	adantr	$⊢ (φ \land s \in [0, 1]) \to M (0) = P$
142	141	fveq2d	$⊢ (φ \land s \in [0, 1]) \to F (M (0)) = F (P)$
143	6	adantr	$⊢ (φ \land s \in [0, 1]) \to F (P) = G (0)$
144	142 143	eqtrd	$⊢ (φ \land s \in [0, 1]) \to F (M (0)) = G (0)$
145	129 139 144	3eqtr4d	$⊢ (φ \land s \in [0, 1]) \to F (0 A s) = F (M (0))$
146	145	mpteq2dva	$⊢ φ \to (s \in [0, 1] ⟼ F (0 A s)) = (s \in [0, 1] ⟼ F (M (0)))$
147		fconstmpt	$⊢ [0, 1] \times \{F (M (0))\} = (s \in [0, 1] ⟼ F (M (0)))$
148	146 147	eqtr4di	$⊢ φ \to (s \in [0, 1] ⟼ F (0 A s)) = [0, 1] \times \{F (M (0))\}$
149		fovrn	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land 0 \in [0, 1] \land s \in [0, 1]) \to 0 A s \in B$
150	25 149	mp3an2	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land s \in [0, 1]) \to 0 A s \in B$
151	24 150	sylan	$⊢ (φ \land s \in [0, 1]) \to 0 A s \in B$
152		eqidd	$⊢ φ \to (s \in [0, 1] ⟼ 0 A s) = (s \in [0, 1] ⟼ 0 A s)$
153		fveq2	$⊢ x = 0 A s \to F (x) = F (0 A s)$
154	151 152 54 153	fmptco	$⊢ φ \to F \circ (s \in [0, 1] ⟼ 0 A s) = (s \in [0, 1] ⟼ F (0 A s))$
155	53	ffnd	$⊢ φ \to F Fn B$
156		fcoconst	$⊢ (F Fn B \land M (0) \in B) \to F \circ ([0, 1] \times \{M (0)\}) = [0, 1] \times \{F (M (0))\}$
157	155 125 156	syl2anc	$⊢ φ \to F \circ ([0, 1] \times \{M (0)\}) = [0, 1] \times \{F (M (0))\}$
158	148 154 157	3eqtr4d	$⊢ φ \to F \circ (s \in [0, 1] ⟼ 0 A s) = F \circ ([0, 1] \times \{M (0)\})$
159	12 140	eqtr4d	$⊢ φ \to 0 A 0 = M (0)$
160		oveq2	$⊢ s = 0 \to 0 A s = 0 A 0$
161		eqid	$⊢ (s \in [0, 1] ⟼ 0 A s) = (s \in [0, 1] ⟼ 0 A s)$
162	160 161 72	fvmpt	$⊢ 0 \in [0, 1] \to (s \in [0, 1] ⟼ 0 A s) (0) = 0 A 0$
163	25 162	ax-mp	$⊢ (s \in [0, 1] ⟼ 0 A s) (0) = 0 A 0$
164		fvex	$⊢ M (0) \in V$
165	164	fvconst2	$⊢ 0 \in [0, 1] \to ([0, 1] \times \{M (0)\}) (0) = M (0)$
166	25 165	ax-mp	$⊢ ([0, 1] \times \{M (0)\}) (0) = M (0)$
167	159 163 166	3eqtr4g	$⊢ φ \to (s \in [0, 1] ⟼ 0 A s) (0) = ([0, 1] \times \{M (0)\}) (0)$
168	1 21 4 116 118 62 119 127 158 167	cvmliftmoi	$⊢ φ \to (s \in [0, 1] ⟼ 0 A s) = [0, 1] \times \{M (0)\}$
169		fconstmpt	$⊢ [0, 1] \times \{M (0)\} = (s \in [0, 1] ⟼ M (0))$
170	168 169	eqtrdi	$⊢ φ \to (s \in [0, 1] ⟼ 0 A s) = (s \in [0, 1] ⟼ M (0))$
171		mpteqb	$⊢ \forall s \in [0, 1] 0 A s \in V \to ((s \in [0, 1] ⟼ 0 A s) = (s \in [0, 1] ⟼ M (0)) \leftrightarrow \forall s \in [0, 1] 0 A s = M (0))$
172		ovexd	$⊢ s \in [0, 1] \to 0 A s \in V$
173	171 172	mprg	$⊢ (s \in [0, 1] ⟼ 0 A s) = (s \in [0, 1] ⟼ M (0)) \leftrightarrow \forall s \in [0, 1] 0 A s = M (0)$
174	170 173	sylib	$⊢ φ \to \forall s \in [0, 1] 0 A s = M (0)$
175		oveq2	$⊢ s = 1 \to 0 A s = 0 A 1$
176	175	eqeq1d	$⊢ s = 1 \to (0 A s = M (0) \leftrightarrow 0 A 1 = M (0))$
177	176	rspcv	$⊢ 1 \in [0, 1] \to (\forall s \in [0, 1] 0 A s = M (0) \to 0 A 1 = M (0))$
178	91 174 177	mpsyl	$⊢ φ \to 0 A 1 = M (0)$
179	178 140	eqtrd	$⊢ φ \to 0 A 1 = P$
180	91	a1i	$⊢ φ \to 1 \in [0, 1]$
181	38 38 180	cnmptc	$⊢ φ \to (s \in [0, 1] ⟼ 1) \in (II Cn II)$
182	38 61 181 10	cnmpt12f	$⊢ φ \to (s \in [0, 1] ⟼ s A 1) \in (II Cn C)$
183	1	cvmlift	$⊢ ((F \in (C CovMap J) \land H \in (II Cn J)) \land (P \in B \land F (P) = H (0))) \to \exists! f \in (II Cn C) (F \circ f = H \land f (0) = P)$
184	4 8 5 17 183	syl22anc	$⊢ φ \to \exists! f \in (II Cn C) (F \circ f = H \land f (0) = P)$
185		coeq2	$⊢ f = (s \in [0, 1] ⟼ s A 1) \to F \circ f = F \circ (s \in [0, 1] ⟼ s A 1)$
186	185	eqeq1d	$⊢ f = (s \in [0, 1] ⟼ s A 1) \to (F \circ f = H \leftrightarrow F \circ (s \in [0, 1] ⟼ s A 1) = H)$
187		fveq1	$⊢ f = (s \in [0, 1] ⟼ s A 1) \to f (0) = (s \in [0, 1] ⟼ s A 1) (0)$
188		oveq1	$⊢ s = 0 \to s A 1 = 0 A 1$
189		eqid	$⊢ (s \in [0, 1] ⟼ s A 1) = (s \in [0, 1] ⟼ s A 1)$
190		ovex	$⊢ 0 A 1 \in V$
191	188 189 190	fvmpt	$⊢ 0 \in [0, 1] \to (s \in [0, 1] ⟼ s A 1) (0) = 0 A 1$
192	25 191	ax-mp	$⊢ (s \in [0, 1] ⟼ s A 1) (0) = 0 A 1$
193	187 192	eqtrdi	$⊢ f = (s \in [0, 1] ⟼ s A 1) \to f (0) = 0 A 1$
194	193	eqeq1d	$⊢ f = (s \in [0, 1] ⟼ s A 1) \to (f (0) = P \leftrightarrow 0 A 1 = P)$
195	186 194	anbi12d	$⊢ f = (s \in [0, 1] ⟼ s A 1) \to ((F \circ f = H \land f (0) = P) \leftrightarrow (F \circ (s \in [0, 1] ⟼ s A 1) = H \land 0 A 1 = P))$
196	195	riota2	$⊢ ((s \in [0, 1] ⟼ s A 1) \in (II Cn C) \land \exists! f \in (II Cn C) (F \circ f = H \land f (0) = P)) \to ((F \circ (s \in [0, 1] ⟼ s A 1) = H \land 0 A 1 = P) \leftrightarrow (ι f \in (II Cn C) \| (F \circ f = H \land f (0) = P)) = (s \in [0, 1] ⟼ s A 1))$
197	182 184 196	syl2anc	$⊢ φ \to ((F \circ (s \in [0, 1] ⟼ s A 1) = H \land 0 A 1 = P) \leftrightarrow (ι f \in (II Cn C) \| (F \circ f = H \land f (0) = P)) = (s \in [0, 1] ⟼ s A 1))$
198	114 179 197	mpbi2and	$⊢ φ \to (ι f \in (II Cn C) \| (F \circ f = H \land f (0) = P)) = (s \in [0, 1] ⟼ s A 1)$
199	3 198	syl5eq	$⊢ φ \to N = (s \in [0, 1] ⟼ s A 1)$
200	21 1	cnf	$⊢ N \in (II Cn C) \to N : [0, 1] ⟶ B$
201	19 200	syl	$⊢ φ \to N : [0, 1] ⟶ B$
202	201	feqmptd	$⊢ φ \to N = (s \in [0, 1] ⟼ N (s))$
203	199 202	eqtr3d	$⊢ φ \to (s \in [0, 1] ⟼ s A 1) = (s \in [0, 1] ⟼ N (s))$
204		mpteqb	$⊢ \forall s \in [0, 1] s A 1 \in V \to ((s \in [0, 1] ⟼ s A 1) = (s \in [0, 1] ⟼ N (s)) \leftrightarrow \forall s \in [0, 1] s A 1 = N (s))$
205		ovexd	$⊢ s \in [0, 1] \to s A 1 \in V$
206	204 205	mprg	$⊢ (s \in [0, 1] ⟼ s A 1) = (s \in [0, 1] ⟼ N (s)) \leftrightarrow \forall s \in [0, 1] s A 1 = N (s)$
207	203 206	sylib	$⊢ φ \to \forall s \in [0, 1] s A 1 = N (s)$
208	207	r19.21bi	$⊢ (φ \land s \in [0, 1]) \to s A 1 = N (s)$
209	174	r19.21bi	$⊢ (φ \land s \in [0, 1]) \to 0 A s = M (0)$
210	38 181 61 10	cnmpt12f	$⊢ φ \to (s \in [0, 1] ⟼ 1 A s) \in (II Cn C)$
211		ffvelrn	$⊢ (M : [0, 1] ⟶ B \land 1 \in [0, 1]) \to M (1) \in B$
212	83 91 211	sylancl	$⊢ φ \to M (1) \in B$
213		cnconst2	$⊢ (II \in TopOn ([0, 1]) \land C \in TopOn (B) \land M (1) \in B) \to [0, 1] \times \{M (1)\} \in (II Cn C)$
214	38 123 212 213	syl3anc	$⊢ φ \to [0, 1] \times \{M (1)\} \in (II Cn C)$
215		opelxpi	$⊢ (1 \in [0, 1] \land s \in [0, 1]) \to ⟨1, s⟩ \in ([0, 1] \times [0, 1])$
216	91 215	mpan	$⊢ s \in [0, 1] \to ⟨1, s⟩ \in ([0, 1] \times [0, 1])$
217		fvco3	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land ⟨1, s⟩ \in ([0, 1] \times [0, 1])) \to (F \circ A) (⟨1, s⟩) = F (A (⟨1, s⟩))$
218	24 216 217	syl2an	$⊢ (φ \land s \in [0, 1]) \to (F \circ A) (⟨1, s⟩) = F (A (⟨1, s⟩))$
219	30	fveq1d	$⊢ (φ \land s \in [0, 1]) \to (F \circ A) (⟨1, s⟩) = K (⟨1, s⟩)$
220	218 219	eqtr3d	$⊢ (φ \land s \in [0, 1]) \to F (A (⟨1, s⟩)) = K (⟨1, s⟩)$
221		df-ov	$⊢ 1 A s = A (⟨1, s⟩)$
222	221	fveq2i	$⊢ F (1 A s) = F (A (⟨1, s⟩))$
223		df-ov	$⊢ 1 K s = K (⟨1, s⟩)$
224	220 222 223	3eqtr4g	$⊢ (φ \land s \in [0, 1]) \to F (1 A s) = 1 K s$
225	128	simprd	$⊢ (φ \land s \in [0, 1]) \to 1 K s = G (1)$
226	13	simp2d	$⊢ φ \to F \circ M = G$
227	226	adantr	$⊢ (φ \land s \in [0, 1]) \to F \circ M = G$
228	227	fveq1d	$⊢ (φ \land s \in [0, 1]) \to (F \circ M) (1) = G (1)$
229	83	adantr	$⊢ (φ \land s \in [0, 1]) \to M : [0, 1] ⟶ B$
230		fvco3	$⊢ (M : [0, 1] ⟶ B \land 1 \in [0, 1]) \to (F \circ M) (1) = F (M (1))$
231	229 91 230	sylancl	$⊢ (φ \land s \in [0, 1]) \to (F \circ M) (1) = F (M (1))$
232	228 231	eqtr3d	$⊢ (φ \land s \in [0, 1]) \to G (1) = F (M (1))$
233	224 225 232	3eqtrd	$⊢ (φ \land s \in [0, 1]) \to F (1 A s) = F (M (1))$
234	233	mpteq2dva	$⊢ φ \to (s \in [0, 1] ⟼ F (1 A s)) = (s \in [0, 1] ⟼ F (M (1)))$
235		fconstmpt	$⊢ [0, 1] \times \{F (M (1))\} = (s \in [0, 1] ⟼ F (M (1)))$
236	234 235	eqtr4di	$⊢ φ \to (s \in [0, 1] ⟼ F (1 A s)) = [0, 1] \times \{F (M (1))\}$
237		fovrn	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land 1 \in [0, 1] \land s \in [0, 1]) \to 1 A s \in B$
238	91 237	mp3an2	$⊢ (A : [0, 1] \times [0, 1] ⟶ B \land s \in [0, 1]) \to 1 A s \in B$
239	24 238	sylan	$⊢ (φ \land s \in [0, 1]) \to 1 A s \in B$
240		eqidd	$⊢ φ \to (s \in [0, 1] ⟼ 1 A s) = (s \in [0, 1] ⟼ 1 A s)$
241		fveq2	$⊢ x = 1 A s \to F (x) = F (1 A s)$
242	239 240 54 241	fmptco	$⊢ φ \to F \circ (s \in [0, 1] ⟼ 1 A s) = (s \in [0, 1] ⟼ F (1 A s))$
243		fcoconst	$⊢ (F Fn B \land M (1) \in B) \to F \circ ([0, 1] \times \{M (1)\}) = [0, 1] \times \{F (M (1))\}$
244	155 212 243	syl2anc	$⊢ φ \to F \circ ([0, 1] \times \{M (1)\}) = [0, 1] \times \{F (M (1))\}$
245	236 242 244	3eqtr4d	$⊢ φ \to F \circ (s \in [0, 1] ⟼ 1 A s) = F \circ ([0, 1] \times \{M (1)\})$
246		oveq1	$⊢ s = 1 \to s A 0 = 1 A 0$
247		fveq2	$⊢ s = 1 \to M (s) = M (1)$
248	246 247	eqeq12d	$⊢ s = 1 \to (s A 0 = M (s) \leftrightarrow 1 A 0 = M (1))$
249	248	rspcv	$⊢ 1 \in [0, 1] \to (\forall s \in [0, 1] s A 0 = M (s) \to 1 A 0 = M (1))$
250	91 89 249	mpsyl	$⊢ φ \to 1 A 0 = M (1)$
251		oveq2	$⊢ s = 0 \to 1 A s = 1 A 0$
252		eqid	$⊢ (s \in [0, 1] ⟼ 1 A s) = (s \in [0, 1] ⟼ 1 A s)$
253		ovex	$⊢ 1 A 0 \in V$
254	251 252 253	fvmpt	$⊢ 0 \in [0, 1] \to (s \in [0, 1] ⟼ 1 A s) (0) = 1 A 0$
255	25 254	ax-mp	$⊢ (s \in [0, 1] ⟼ 1 A s) (0) = 1 A 0$
256		fvex	$⊢ M (1) \in V$
257	256	fvconst2	$⊢ 0 \in [0, 1] \to ([0, 1] \times \{M (1)\}) (0) = M (1)$
258	25 257	ax-mp	$⊢ ([0, 1] \times \{M (1)\}) (0) = M (1)$
259	250 255 258	3eqtr4g	$⊢ φ \to (s \in [0, 1] ⟼ 1 A s) (0) = ([0, 1] \times \{M (1)\}) (0)$
260	1 21 4 116 118 62 210 214 245 259	cvmliftmoi	$⊢ φ \to (s \in [0, 1] ⟼ 1 A s) = [0, 1] \times \{M (1)\}$
261		fconstmpt	$⊢ [0, 1] \times \{M (1)\} = (s \in [0, 1] ⟼ M (1))$
262	260 261	eqtrdi	$⊢ φ \to (s \in [0, 1] ⟼ 1 A s) = (s \in [0, 1] ⟼ M (1))$
263		mpteqb	$⊢ \forall s \in [0, 1] 1 A s \in V \to ((s \in [0, 1] ⟼ 1 A s) = (s \in [0, 1] ⟼ M (1)) \leftrightarrow \forall s \in [0, 1] 1 A s = M (1))$
264		ovexd	$⊢ s \in [0, 1] \to 1 A s \in V$
265	263 264	mprg	$⊢ (s \in [0, 1] ⟼ 1 A s) = (s \in [0, 1] ⟼ M (1)) \leftrightarrow \forall s \in [0, 1] 1 A s = M (1)$
266	262 265	sylib	$⊢ φ \to \forall s \in [0, 1] 1 A s = M (1)$
267	266	r19.21bi	$⊢ (φ \land s \in [0, 1]) \to 1 A s = M (1)$
268	14 19 10 90 208 209 267	isphtpy2d	$⊢ φ \to A \in (M PHtpy (C) N)$

Metamath Proof Explorer

Theorem cvmliftphtlem

Proof