MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ishtpy Structured version   Unicode version

Theorem ishtpy 20513
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.)
Hypotheses
Ref Expression
ishtpy.1  |-  ( ph  ->  J  e.  (TopOn `  X ) )
ishtpy.3  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
ishtpy.4  |-  ( ph  ->  G  e.  ( J  Cn  K ) )
Assertion
Ref Expression
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 ) ) ) ) )
Distinct variable groups:    F, s    G, s    H, s    J, s    ph, s    X, s
Allowed substitution hint:    K( s)

Proof of Theorem ishtpy
Dummy variables  f 
g  h  j  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-htpy 20511 . . . . . 6  |- 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
) ) } ) )
21a1i 11 . . . . 5  |-  ( 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 ) ) } ) ) )
3 simprl 755 . . . . . . 7  |-  ( (
ph  /\  ( j  =  J  /\  k  =  K ) )  -> 
j  =  J )
4 simprr 756 . . . . . . 7  |-  ( (
ph  /\  ( j  =  J  /\  k  =  K ) )  -> 
k  =  K )
53, 4oveq12d 6104 . . . . . 6  |-  ( (
ph  /\  ( j  =  J  /\  k  =  K ) )  -> 
( j  Cn  k
)  =  ( J  Cn  K ) )
63oveq1d 6101 . . . . . . . 8  |-  ( (
ph  /\  ( j  =  J  /\  k  =  K ) )  -> 
( j  tX  II )  =  ( J  tX  II ) )
76, 4oveq12d 6104 . . . . . . 7  |-  ( (
ph  /\  ( j  =  J  /\  k  =  K ) )  -> 
( ( j  tX  II )  Cn  k
)  =  ( ( J  tX  II )  Cn  K ) )
83unieqd 4094 . . . . . . . . 9  |-  ( (
ph  /\  ( j  =  J  /\  k  =  K ) )  ->  U. j  =  U. J )
9 ishtpy.1 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  (TopOn `  X ) )
10 toponuni 18501 . . . . . . . . . . 11  |-  ( J  e.  (TopOn `  X
)  ->  X  =  U. J )
119, 10syl 16 . . . . . . . . . 10  |-  ( ph  ->  X  =  U. J
)
1211adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( j  =  J  /\  k  =  K ) )  ->  X  =  U. J )
138, 12eqtr4d 2472 . . . . . . . 8  |-  ( (
ph  /\  ( j  =  J  /\  k  =  K ) )  ->  U. j  =  X
)
1413raleqdv 2917 . . . . . . 7  |-  ( (
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 ) ) ) )
157, 14rabeqbidv 2961 . . . . . 6  |-  ( (
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 ) ) } )
165, 5, 15mpt2eq123dv 6143 . . . . 5  |-  ( (
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 ) ) } ) )
17 topontop 18500 . . . . . 6  |-  ( J  e.  (TopOn `  X
)  ->  J  e.  Top )
189, 17syl 16 . . . . 5  |-  ( ph  ->  J  e.  Top )
19 ishtpy.3 . . . . . 6  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
20 cntop2 18814 . . . . . 6  |-  ( F  e.  ( J  Cn  K )  ->  K  e.  Top )
2119, 20syl 16 . . . . 5  |-  ( ph  ->  K  e.  Top )
22 ssrab2 3430 . . . . . . . . . 10  |-  { 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 )
23 ovex 6111 . . . . . . . . . . 11  |-  ( ( J  tX  II )  Cn  K )  e. 
_V
2423elpw2 4449 . . . . . . . . . 10  |-  ( { 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
)  <->  { 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 ) )
2522, 24mpbir 209 . . . . . . . . 9  |-  { 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 )
2625rgen2w 2778 . . . . . . . 8  |-  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 2437 . . . . . . . . 9  |-  ( 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 ) ) } )
2827fmpt2 6636 . . . . . . . 8  |-  ( 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
) )
2926, 28mpbi 208 . . . . . . 7  |-  ( 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 6111 . . . . . . . 8  |-  ( J  Cn  K )  e. 
_V
3130, 30xpex 6503 . . . . . . 7  |-  ( ( J  Cn  K )  X.  ( J  Cn  K ) )  e. 
_V
3223pwex 4468 . . . . . . 7  |-  ~P (
( J  tX  II )  Cn  K )  e. 
_V
33 fex2 6527 . . . . . . 7  |-  ( ( ( 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 )
3429, 31, 32, 33mp3an 1314 . . . . . 6  |-  ( 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
3534a1i 11 . . . . 5  |-  ( 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 )
362, 16, 18, 21, 35ovmpt2d 6213 . . . 4  |-  ( 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 5683 . . . . . . . . 9  |-  ( f  =  F  ->  (
f `  s )  =  ( F `  s ) )
3837eqeq2d 2448 . . . . . . . 8  |-  ( f  =  F  ->  (
( s h 0 )  =  ( f `
 s )  <->  ( s
h 0 )  =  ( F `  s
) ) )
39 fveq1 5683 . . . . . . . . 9  |-  ( g  =  G  ->  (
g `  s )  =  ( G `  s ) )
4039eqeq2d 2448 . . . . . . . 8  |-  ( g  =  G  ->  (
( s h 1 )  =  ( g `
 s )  <->  ( s
h 1 )  =  ( G `  s
) ) )
4138, 40bi2anan9 868 . . . . . . 7  |-  ( ( f  =  F  /\  g  =  G )  ->  ( ( ( s h 0 )  =  ( f `  s
)  /\  ( s
h 1 )  =  ( g `  s
) )  <->  ( (
s h 0 )  =  ( F `  s )  /\  (
s h 1 )  =  ( G `  s ) ) ) )
4241adantl 466 . . . . . 6  |-  ( (
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 ) ) ) )
4342ralbidv 2729 . . . . 5  |-  ( (
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 ) ) ) )
4443rabbidv 2958 . . . 4  |-  ( (
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 ishtpy.4 . . . 4  |-  ( ph  ->  G  e.  ( J  Cn  K ) )
4623rabex 4436 . . . . 5  |-  { h  e.  ( ( J  tX  II )  Cn  K
)  |  A. s  e.  X  ( (
s h 0 )  =  ( F `  s )  /\  (
s h 1 )  =  ( G `  s ) ) }  e.  _V
4746a1i 11 . . . 4  |-  ( ph  ->  { h  e.  ( ( J  tX  II )  Cn  K )  | 
A. s  e.  X  ( ( s h 0 )  =  ( F `  s )  /\  ( s h 1 )  =  ( G `  s ) ) }  e.  _V )
4836, 44, 19, 45, 47ovmpt2d 6213 . . 3  |-  ( 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 ) ) } )
4948eleq2d 2504 . 2  |-  ( 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 ) ) } ) )
50 oveq 6092 . . . . . 6  |-  ( h  =  H  ->  (
s h 0 )  =  ( s H 0 ) )
5150eqeq1d 2445 . . . . 5  |-  ( h  =  H  ->  (
( s h 0 )  =  ( F `
 s )  <->  ( s H 0 )  =  ( F `  s
) ) )
52 oveq 6092 . . . . . 6  |-  ( h  =  H  ->  (
s h 1 )  =  ( s H 1 ) )
5352eqeq1d 2445 . . . . 5  |-  ( h  =  H  ->  (
( s h 1 )  =  ( G `
 s )  <->  ( s H 1 )  =  ( G `  s
) ) )
5451, 53anbi12d 710 . . . 4  |-  ( h  =  H  ->  (
( ( s h 0 )  =  ( F `  s )  /\  ( s h 1 )  =  ( G `  s ) )  <->  ( ( s H 0 )  =  ( F `  s
)  /\  ( s H 1 )  =  ( G `  s
) ) ) )
5554ralbidv 2729 . . 3  |-  ( 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 ) ) ) )
5655elrab 3110 . 2  |-  ( 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 ) ) ) )
5749, 56syl6bb 261 1  |-  ( 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 ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2709   {crab 2713   _Vcvv 2966    C_ wss 3321   ~Pcpw 3853   U.cuni 4084    X. cxp 4830   -->wf 5407   ` cfv 5411  (class class class)co 6086    e. cmpt2 6088   0cc0 9274   1c1 9275   Topctop 18467  TopOnctopon 18468    Cn ccn 18797    tX ctx 19102   IIcii 20420   Htpy chtpy 20508
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-fv 5419  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-1st 6572  df-2nd 6573  df-map 7208  df-top 18472  df-topon 18475  df-cn 18800  df-htpy 20511
This theorem is referenced by:  htpycn  20514  htpyi  20515  ishtpyd  20516
  Copyright terms: Public domain W3C validator