Metamath Proof Explorer

Theorem isphtpc

Description: The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Assertion isphtpc 
|- ( F ( ~=ph ` J ) G <-> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( F ( ~=ph ` J ) G <-> <. F , G >. e. ( ~=ph ` J ) )
2 df-phtpc 
 |-  ~=ph = ( j e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn j ) /\ ( f ( PHtpy ` j ) g ) =/= (/) ) } )
3 2 mptrcl 
 |-  ( <. F , G >. e. ( ~=ph ` J ) -> J e. Top )
4 1 3 sylbi 
 |-  ( F ( ~=ph ` J ) G -> J e. Top )
5 cntop2 
 |-  ( F e. ( II Cn J ) -> J e. Top )
6 5 3ad2ant1 
 |-  ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) -> J e. Top )
7 oveq2 
 |-  ( j = J -> ( II Cn j ) = ( II Cn J ) )
8 7 sseq2d 
 |-  ( j = J -> ( { f , g } C_ ( II Cn j ) <-> { f , g } C_ ( II Cn J ) ) )
9 vex 
 |-  f e. _V
10 vex 
 |-  g e. _V
11 9 10 prss 
 |-  ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) <-> { f , g } C_ ( II Cn J ) )
12 8 11 bitr4di 
 |-  ( j = J -> ( { f , g } C_ ( II Cn j ) <-> ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) ) )
13 fveq2 
 |-  ( j = J -> ( PHtpy ` j ) = ( PHtpy ` J ) )
14 13 oveqd 
 |-  ( j = J -> ( f ( PHtpy ` j ) g ) = ( f ( PHtpy ` J ) g ) )
15 14 neeq1d 
 |-  ( j = J -> ( ( f ( PHtpy ` j ) g ) =/= (/) <-> ( f ( PHtpy ` J ) g ) =/= (/) ) )
16 12 15 anbi12d 
 |-  ( j = J -> ( ( { f , g } C_ ( II Cn j ) /\ ( f ( PHtpy ` j ) g ) =/= (/) ) <-> ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) ) )
17 16 opabbidv 
 |-  ( j = J -> { <. f , g >. | ( { f , g } C_ ( II Cn j ) /\ ( f ( PHtpy ` j ) g ) =/= (/) ) } = { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } )
18 ovex 
 |-  ( II Cn J ) e. _V
19 18 18 xpex 
 |-  ( ( II Cn J ) X. ( II Cn J ) ) e. _V
20 opabssxp 
 |-  { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } C_ ( ( II Cn J ) X. ( II Cn J ) )
21 19 20 ssexi 
 |-  { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } e. _V
22 17 2 21 fvmpt 
 |-  ( J e. Top -> ( ~=ph ` J ) = { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } )
23 22 breqd 
 |-  ( J e. Top -> ( F ( ~=ph ` J ) G <-> F { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } G ) )
24 oveq12 
 |-  ( ( f = F /\ g = G ) -> ( f ( PHtpy ` J ) g ) = ( F ( PHtpy ` J ) G ) )
25 24 neeq1d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ( PHtpy ` J ) g ) =/= (/) <-> ( F ( PHtpy ` J ) G ) =/= (/) ) )
26 eqid 
 |-  { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } = { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) }
27 25 26 brab2a 
 |-  ( F { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } G <-> ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )
28 df-3an 
 |-  ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) <-> ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )
29 27 28 bitr4i 
 |-  ( F { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } G <-> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )
30 23 29 bitrdi 
 |-  ( J e. Top -> ( F ( ~=ph ` J ) G <-> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) ) )
31 4 6 30 pm5.21nii 
 |-  ( F ( ~=ph ` J ) G <-> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )