Theorem isphtpc 22793

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

Assertion

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

Proof of Theorem isphtpc

Dummy variables f g j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-br 4654	. . 3 |- ( F ( ~=ph ` J ) G <-> <. F , G >. e. ( ~=ph ` J ) )
2		df-phtpc 22791	. . . . 5 |- ~=ph = ( j e. Top |-> { <. f , g >. | ( { f , g } C_ ( II Cn j ) /\ ( f ( PHtpy ` j ) g ) =/= (/) ) } )
3	2	dmmptss 5631	. . . 4 |- dom ~=ph C_ Top
4		elfvdm 6220	. . . 4 |- ( <. F , G >. e. ( ~=ph ` J ) -> J e. dom ~=ph )
5	3, 4	sseldi 3601	. . 3 |- ( <. F , G >. e. ( ~=ph ` J ) -> J e. Top )
6	1, 5	sylbi 207	. 2 |- ( F ( ~=ph ` J ) G -> J e. Top )
7		cntop2 21045	. . 3 |- ( F e. ( II Cn J ) -> J e. Top )
8	7	3ad2ant1 1082	. 2 |- ( ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) -> J e. Top )
9		oveq2 6658	. . . . . . . . 9 |- ( j = J -> ( II Cn j ) = ( II Cn J ) )
10	9	sseq2d 3633	. . . . . . . 8 |- ( j = J -> ( { f , g } C_ ( II Cn j ) <-> { f , g } C_ ( II Cn J ) ) )
11		vex 3203	. . . . . . . . 9 |- f e. _V
12		vex 3203	. . . . . . . . 9 |- g e. _V
13	11, 12	prss 4351	. . . . . . . 8 |- ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) <-> { f , g } C_ ( II Cn J ) )
14	10, 13	syl6bbr 278	. . . . . . 7 |- ( j = J -> ( { f , g } C_ ( II Cn j ) <-> ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) ) )
15		fveq2 6191	. . . . . . . . 9 |- ( j = J -> ( PHtpy ` j ) = ( PHtpy ` J ) )
16	15	oveqd 6667	. . . . . . . 8 |- ( j = J -> ( f ( PHtpy ` j ) g ) = ( f ( PHtpy ` J ) g ) )
17	16	neeq1d 2853	. . . . . . 7 |- ( j = J -> ( ( f ( PHtpy ` j ) g ) =/= (/) <-> ( f ( PHtpy ` J ) g ) =/= (/) ) )
18	14, 17	anbi12d 747	. . . . . 6 |- ( 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 ) =/= (/) ) ) )
19	18	opabbidv 4716	. . . . 5 |- ( 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 ) =/= (/) ) } )
20		ovex 6678	. . . . . . 7 |- ( II Cn J ) e. _V
21	20, 20	xpex 6962	. . . . . 6 |- ( ( II Cn J ) X. ( II Cn J ) ) e. _V
22		opabssxp 5193	. . . . . 6 |- { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } C_ ( ( II Cn J ) X. ( II Cn J ) )
23	21, 22	ssexi 4803	. . . . 5 |- { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } e. _V
24	19, 2, 23	fvmpt 6282	. . . 4 |- ( J e. Top -> ( ~=ph ` J ) = { <. f , g >. | ( ( f e. ( II Cn J ) /\ g e. ( II Cn J ) ) /\ ( f ( PHtpy ` J ) g ) =/= (/) ) } )
25	24	breqd 4664	. . 3 |- ( 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 ) )
26		oveq12 6659	. . . . . 6 |- ( ( f = F /\ g = G ) -> ( f ( PHtpy ` J ) g ) = ( F ( PHtpy ` J ) G ) )
27	26	neeq1d 2853	. . . . 5 |- ( ( f = F /\ g = G ) -> ( ( f ( PHtpy ` J ) g ) =/= (/) <-> ( F ( PHtpy ` J ) G ) =/= (/) ) )
28		eqid 2622	. . . . 5 |- { <. 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 ) =/= (/) ) }
29	27, 28	brab2a 5194	. . . 4 |- ( 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		df-3an 1039	. . . 4 |- ( ( 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 ) =/= (/) ) )
31	29, 30	bitr4i 267	. . 3 |- ( 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 ) =/= (/) ) )
32	25, 31	syl6bb 276	. 2 |- ( J e. Top -> ( F ( ~=ph ` J ) G <-> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) ) )
33	6, 8, 32	pm5.21nii 368	1 |- ( F ( ~=ph ` J ) G <-> ( F e. ( II Cn J ) /\ G e. ( II Cn J ) /\ ( F ( PHtpy ` J ) G ) =/= (/) ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   C_ wss 3574   (/)c0 3915   {cpr 4179   <.cop 4183   class class class wbr 4653   {copab 4712   X. cxp 5112   dom cdm 5114   ` cfv 5888  (class class class)co 6650   Topctop 20698   Cn ccn 21028   IIcii 22678   PHtpycphtpy 22767   ~=ph cphtpc 22768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-map 7859  df-top 20699  df-topon 20716  df-cn 21031  df-phtpc 22791

This theorem is referenced by:  phtpcer  22794  phtpcerOLD  22795  phtpc01  22796  reparpht  22798  phtpcco2  22799  pcohtpylem  22819  pcohtpy  22820  pcorevlem  22826  pi1blem  22839  txsconnlem  31222  txsconn  31223  cvxsconn  31225  cvmliftpht  31300