Theorem ishtpy 20547

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.

Step	Hyp	Ref	Expression
1		df-htpy 20545	. . . . . 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 ) ) } ) )
2	1	a1i 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 )
5	3, 4	oveq12d 6112	. . . . . 6 |- ( ( ph /\ ( j = J /\ k = K ) ) -> ( j Cn k ) = ( J Cn K ) )
6	3	oveq1d 6109	. . . . . . . 8 |- ( ( ph /\ ( j = J /\ k = K ) ) -> ( j tX II ) = ( J tX II ) )
7	6, 4	oveq12d 6112	. . . . . . 7 |- ( ( ph /\ ( j = J /\ k = K ) ) -> ( ( j tX II ) Cn k ) = ( ( J tX II ) Cn K ) )
8	3	unieqd 4104	. . . . . . . . 9 |- ( ( ph /\ ( j = J /\ k = K ) ) -> U. j = U. J )
9		ishtpy.1	. . . . . . . . . . 11 |- ( ph -> J e. (TopOn ` X ) )
10		toponuni 18535	. . . . . . . . . . 11 |- ( J e. (TopOn ` X ) -> X = U. J )
11	9, 10	syl 16	. . . . . . . . . 10 |- ( ph -> X = U. J )
12	11	adantr 465	. . . . . . . . 9 |- ( ( ph /\ ( j = J /\ k = K ) ) -> X = U. J )
13	8, 12	eqtr4d 2478	. . . . . . . 8 |- ( ( ph /\ ( j = J /\ k = K ) ) -> U. j = X )
14	13	raleqdv 2926	. . . . . . 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 ) ) ) )
15	7, 14	rabeqbidv 2970	. . . . . 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 ) ) } )
16	5, 5, 15	mpt2eq123dv 6151	. . . . 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 18534	. . . . . 6 |- ( J e. (TopOn ` X ) -> J e. Top )
18	9, 17	syl 16	. . . . 5 |- ( ph -> J e. Top )
19		ishtpy.3	. . . . . 6 |- ( ph -> F e. ( J Cn K ) )
20		cntop2 18848	. . . . . 6 |- ( F e. ( J Cn K ) -> K e. Top )
21	19, 20	syl 16	. . . . 5 |- ( ph -> K e. Top )
22		ssrab2 3440	. . . . . . . . . 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 6119	. . . . . . . . . . 11 |- ( ( J tX II ) Cn K ) e. _V
24	23	elpw2 4459	. . . . . . . . . 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 ) )
25	22, 24	mpbir 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 )
26	25	rgen2w 2787	. . . . . . . 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 2443	. . . . . . . . 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 ) ) } )
28	27	fmpt2 6644	. . . . . . . 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 ) )
29	26, 28	mpbi 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 6119	. . . . . . . 8 |- ( J Cn K ) e. _V
31	30, 30	xpex 6511	. . . . . . 7 |- ( ( J Cn K ) X. ( J Cn K ) ) e. _V
32	23	pwex 4478	. . . . . . 7 |- ~P ( ( J tX II ) Cn K ) e. _V
33		fex2 6535	. . . . . . 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 )
34	29, 31, 32, 33	mp3an 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
35	34	a1i 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 )
36	2, 16, 18, 21, 35	ovmpt2d 6221	. . . 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 5693	. . . . . . . . 9 |- ( f = F -> ( f ` s ) = ( F ` s ) )
38	37	eqeq2d 2454	. . . . . . . 8 |- ( f = F -> ( ( s h 0 ) = ( f ` s ) <-> ( s h 0 ) = ( F ` s ) ) )
39		fveq1 5693	. . . . . . . . 9 |- ( g = G -> ( g ` s ) = ( G ` s ) )
40	39	eqeq2d 2454	. . . . . . . 8 |- ( g = G -> ( ( s h 1 ) = ( g ` s ) <-> ( s h 1 ) = ( G ` s ) ) )
41	38, 40	bi2anan9 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 ) ) ) )
42	41	adantl 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 ) ) ) )
43	42	ralbidv 2738	. . . . 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 ) ) ) )
44	43	rabbidv 2967	. . . 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 ) )
46	23	rabex 4446	. . . . 5 |- { h e. ( ( J tX II ) Cn K ) | A. s e. X ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) } e. _V
47	46	a1i 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 )
48	36, 44, 19, 45, 47	ovmpt2d 6221	. . 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 ) ) } )
49	48	eleq2d 2510	. 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 6100	. . . . . 6 |- ( h = H -> ( s h 0 ) = ( s H 0 ) )
51	50	eqeq1d 2451	. . . . 5 |- ( h = H -> ( ( s h 0 ) = ( F ` s ) <-> ( s H 0 ) = ( F ` s ) ) )
52		oveq 6100	. . . . . 6 |- ( h = H -> ( s h 1 ) = ( s H 1 ) )
53	52	eqeq1d 2451	. . . . 5 |- ( h = H -> ( ( s h 1 ) = ( G ` s ) <-> ( s H 1 ) = ( G ` s ) ) )
54	51, 53	anbi12d 710	. . . 4 |- ( h = H -> ( ( ( s h 0 ) = ( F ` s ) /\ ( s h 1 ) = ( G ` s ) ) <-> ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) ) )
55	54	ralbidv 2738	. . 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 ) ) ) )
56	55	elrab 3120	. 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 ) ) ) )
57	49, 56	syl6bb 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 ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   A.wral 2718   {crab 2722   _Vcvv 2975   C_ wss 3331   ~Pcpw 3863   U.cuni 4094   X. cxp 4841   -->wf 5417   ` cfv 5421  (class class class)co 6094   e. cmpt2 6096   0cc0 9285   1c1 9286   Topctop 18501  TopOnctopon 18502   Cn ccn 18831   tX ctx 19136   IIcii 20454   Htpy chtpy 20542

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 2423  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375

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 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-csb 3292  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-iun 4176  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-ima 4856  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-1st 6580  df-2nd 6581  df-map 7219  df-top 18506  df-topon 18509  df-cn 18834  df-htpy 20545

This theorem is referenced by:  htpycn  20548  htpyi  20549  ishtpyd  20550