Metamath Proof Explorer

Theorem cvmliftphtlem

Description: Lemma for cvmliftpht . (Contributed by Mario Carneiro, 6-Jul-2015)

Ref Expression
Hypotheses cvmliftpht.b 
|- B = U. C
cvmliftpht.m 
|- M = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )
cvmliftpht.n 
|- N = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = H /\ ( f ` 0 ) = P ) )
cvmliftpht.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmliftpht.p 
|- ( ph -> P e. B )
cvmliftpht.e 
|- ( ph -> ( F ` P ) = ( G ` 0 ) )
cvmliftphtlem.g 
|- ( ph -> G e. ( II Cn J ) )
cvmliftphtlem.h 
|- ( ph -> H e. ( II Cn J ) )
cvmliftphtlem.k 
|- ( ph -> K e. ( G ( PHtpy ` J ) H ) )
cvmliftphtlem.a 
|- ( ph -> A e. ( ( II tX II ) Cn C ) )
cvmliftphtlem.c 
|- ( ph -> ( F o. A ) = K )
cvmliftphtlem.0 
|- ( ph -> ( 0 A 0 ) = P )
Assertion cvmliftphtlem 
|- ( ph -> A e. ( M ( PHtpy ` C ) N ) )

Proof

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