Definition df-htpy

Description: Define the function which takes topological spaces X , Y and two continuous functions F , G : X --> Y and returns the class of homotopies from F to G . (Contributed by Mario Carneiro, 22-Feb-2015)

	Ref	Expression
Assertion	df-htpy	⊢ Htpy = ( 𝑥 ∈ Top , 𝑦 ∈ Top ↦ ( 𝑓 ∈ ( 𝑥 Cn 𝑦 ) , 𝑔 ∈ ( 𝑥 Cn 𝑦 ) ↦ { ℎ ∈ ( ( 𝑥 ×t II ) Cn 𝑦 ) ∣ ∀ 𝑠 ∈ ∪ 𝑥 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chtpy	⊢ Htpy
1		vx	⊢ 𝑥
2		ctop	⊢ Top
3		vy	⊢ 𝑦
4		vf	⊢ 𝑓
5	1	cv	⊢ 𝑥
6		ccn	⊢ Cn
7	3	cv	⊢ 𝑦
8	5 7 6	co	⊢ ( 𝑥 Cn 𝑦 )
9		vg	⊢ 𝑔
10		vh	⊢ ℎ
11		ctx	⊢ ×t
12		cii	⊢ II
13	5 12 11	co	⊢ ( 𝑥 ×t II )
14	13 7 6	co	⊢ ( ( 𝑥 ×t II ) Cn 𝑦 )
15		vs	⊢ 𝑠
16	5	cuni	⊢ ∪ 𝑥
17	15	cv	⊢ 𝑠
18	10	cv	⊢ ℎ
19		cc0	⊢ 0
20	17 19 18	co	⊢ ( 𝑠 ℎ 0 )
21	4	cv	⊢ 𝑓
22	17 21	cfv	⊢ ( 𝑓 ‘ 𝑠 )
23	20 22	wceq	⊢ ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 )
24		c1	⊢ 1
25	17 24 18	co	⊢ ( 𝑠 ℎ 1 )
26	9	cv	⊢ 𝑔
27	17 26	cfv	⊢ ( 𝑔 ‘ 𝑠 )
28	25 27	wceq	⊢ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 )
29	23 28	wa	⊢ ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) )
30	29 15 16	wral	⊢ ∀ 𝑠 ∈ ∪ 𝑥 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) )
31	30 10 14	crab	⊢ { ℎ ∈ ( ( 𝑥 ×t II ) Cn 𝑦 ) ∣ ∀ 𝑠 ∈ ∪ 𝑥 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) }
32	4 9 8 8 31	cmpo	⊢ ( 𝑓 ∈ ( 𝑥 Cn 𝑦 ) , 𝑔 ∈ ( 𝑥 Cn 𝑦 ) ↦ { ℎ ∈ ( ( 𝑥 ×t II ) Cn 𝑦 ) ∣ ∀ 𝑠 ∈ ∪ 𝑥 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } )
33	1 3 2 2 32	cmpo	⊢ ( 𝑥 ∈ Top , 𝑦 ∈ Top ↦ ( 𝑓 ∈ ( 𝑥 Cn 𝑦 ) , 𝑔 ∈ ( 𝑥 Cn 𝑦 ) ↦ { ℎ ∈ ( ( 𝑥 ×t II ) Cn 𝑦 ) ∣ ∀ 𝑠 ∈ ∪ 𝑥 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) )
34	0 33	wceq	⊢ Htpy = ( 𝑥 ∈ Top , 𝑦 ∈ Top ↦ ( 𝑓 ∈ ( 𝑥 Cn 𝑦 ) , 𝑔 ∈ ( 𝑥 Cn 𝑦 ) ↦ { ℎ ∈ ( ( 𝑥 ×t II ) Cn 𝑦 ) ∣ ∀ 𝑠 ∈ ∪ 𝑥 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) )