Metamath Proof Explorer

Theorem ishtpy

Description: Membership in the class of homotopies between two continuous functions. (Contributed by Mario Carneiro, 22-Feb-2015) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses ishtpy.1 
|- ( ph -> J e. ( TopOn ` X ) )
ishtpy.3 
|- ( ph -> F e. ( J Cn K ) )
ishtpy.4 
|- ( ph -> G e. ( J Cn K ) )
Assertion ishtpy 
|- ( ph -> ( H e. ( F ( J Htpy K ) G ) <-> ( H e. ( ( J tX II ) Cn K ) /\ A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ishtpy.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 ishtpy.3 
 |-  ( ph -> F e. ( J Cn K ) )
3 ishtpy.4 
 |-  ( ph -> G e. ( J Cn K ) )
4 df-htpy 
 |-  Htpy = ( j e. Top , k e. Top |-> ( f e. ( j Cn k ) , g e. ( j Cn k ) |-> { h e. ( ( j tX II ) Cn k ) | A. s e. U. j ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) )
5 4 a1i 
 |-  ( ph -> Htpy = ( j e. Top , k e. Top |-> ( f e. ( j Cn k ) , g e. ( j Cn k ) |-> { h e. ( ( j tX II ) Cn k ) | A. s e. U. j ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) ) )
6 simprl 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> j = J )
7 simprr 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> k = K )
8 6 7 oveq12d 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> ( j Cn k ) = ( J Cn K ) )
9 6 oveq1d 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> ( j tX II ) = ( J tX II ) )
10 9 7 oveq12d 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> ( ( j tX II ) Cn k ) = ( ( J tX II ) Cn K ) )
11 6 unieqd 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> U. j = U. J )
12 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
13 1 12 syl 
 |-  ( ph -> X = U. J )
14 13 adantr 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> X = U. J )
15 11 14 eqtr4d 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> U. j = X )
16 15 raleqdv 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> ( A. s e. U. j ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) <-> A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) ) )
17 10 16 rabeqbidv 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> { h e. ( ( j tX II ) Cn k ) | A. s e. U. j ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } = { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } )
18 8 8 17 mpoeq123dv 
 |-  ( ( ph /\ ( j = J /\ k = K ) ) -> ( f e. ( j Cn k ) , g e. ( j Cn k ) |-> { h e. ( ( j tX II ) Cn k ) | A. s e. U. j ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) = ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) )
19 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
20 1 19 syl 
 |-  ( ph -> J e. Top )
21 cntop2 
 |-  ( F e. ( J Cn K ) -> K e. Top )
22 2 21 syl 
 |-  ( ph -> K e. Top )
23 ovex 
 |-  ( ( J tX II ) Cn K ) e. _V
24 ssrab2 
 |-  { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } C_ ( ( J tX II ) Cn K )
25 23 24 elpwi2 
 |-  { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } e. ~P ( ( J tX II ) Cn K )
26 25 rgen2w 
 |-  A. f e. ( J Cn K ) A. g e. ( J Cn K ) { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } e. ~P ( ( J tX II ) Cn K )
27 eqid 
 |-  ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) = ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } )
28 27 fmpo 
 |-  ( A. f e. ( J Cn K ) A. g e. ( J Cn K ) { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } e. ~P ( ( J tX II ) Cn K ) <-> ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) : ( ( J Cn K ) X. ( J Cn K ) ) --> ~P ( ( J tX II ) Cn K ) )
29 26 28 mpbi 
 |-  ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) : ( ( J Cn K ) X. ( J Cn K ) ) --> ~P ( ( J tX II ) Cn K )
30 ovex 
 |-  ( J Cn K ) e. _V
31 30 30 xpex 
 |-  ( ( J Cn K ) X. ( J Cn K ) ) e. _V
32 23 pwex 
 |-  ~P ( ( J tX II ) Cn K ) e. _V
33 fex2 
 |-  ( ( ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) : ( ( J Cn K ) X. ( J Cn K ) ) --> ~P ( ( J tX II ) Cn K ) /\ ( ( J Cn K ) X. ( J Cn K ) ) e. _V /\ ~P ( ( J tX II ) Cn K ) e. _V ) -> ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) e. _V )
34 29 31 32 33 mp3an 
 |-  ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) e. _V
35 34 a1i 
 |-  ( ph -> ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) e. _V )
36 5 18 20 22 35 ovmpod 
 |-  ( ph -> ( J Htpy K ) = ( f e. ( J Cn K ) , g e. ( J Cn K ) |-> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } ) )
37 fveq1 
 |-  ( f = F -> ( f ` s ) = ( F ` s ) )
38 37 eqeq2d 
 |-  ( f = F -> ( ( s h 0 ) = ( f ` s ) <-> ( s h 0 ) = ( F ` s ) ) )
39 fveq1 
 |-  ( g = G -> ( g ` s ) = ( G ` s ) )
40 39 eqeq2d 
 |-  ( g = G -> ( ( s h 1 ) = ( g ` s ) <-> ( s h 1 ) = ( G ` s ) ) )
41 38 40 bi2anan9 
 |-  ( ( f = F /\ g = G ) -> ( ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) <-> ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) ) )
42 41 adantl 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> ( ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) <-> ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) ) )
43 42 ralbidv 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> ( A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) <-> A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) ) )
44 43 rabbidv 
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( f ` s ) /\ ( s h 1 ) = ( g ` s ) ) } = { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) } )
45 23 rabex 
 |-  { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) } e. _V
46 45 a1i 
 |-  ( ph -> { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) } e. _V )
47 36 44 2 3 46 ovmpod 
 |-  ( ph -> ( F ( J Htpy K ) G ) = { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) } )
48 47 eleq2d 
 |-  ( ph -> ( H e. ( F ( J Htpy K ) G ) <-> H e. { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) } ) )
49 oveq 
 |-  ( h = H -> ( s h 0 ) = ( s H 0 ) )
50 49 eqeq1d 
 |-  ( h = H -> ( ( s h 0 ) = ( F ` s ) <-> ( s H 0 ) = ( F ` s ) ) )
51 oveq 
 |-  ( h = H -> ( s h 1 ) = ( s H 1 ) )
52 51 eqeq1d 
 |-  ( h = H -> ( ( s h 1 ) = ( G ` s ) <-> ( s H 1 ) = ( G ` s ) ) )
53 50 52 anbi12d 
 |-  ( h = H -> ( ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) <-> ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) ) )
54 53 ralbidv 
 |-  ( h = H -> ( A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) <-> A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) ) )
55 54 elrab 
 |-  ( H e. { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) } <-> ( H e. ( ( J tX II ) Cn K ) /\ A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) ) )
56 48 55 bitrdi 
 |-  ( ph -> ( H e. ( F ( J Htpy K ) G ) <-> ( H e. ( ( J tX II ) Cn K ) /\ A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) ) ) )