Metamath Proof Explorer

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 = x ∈ Top , y ∈ Top ⟼ f ∈ x Cn y , g ∈ x Cn y ⟼ h ∈ x × t II Cn y | ∀ s ∈ ⋃ x s h 0 = f ⁡ s ∧ s h 1 = g ⁡ s

Detailed syntax breakdown

Step Hyp Ref Expression
0 chtpy class Htpy
1 vx setvar x
2 ctop class Top
3 vy setvar y
4 vf setvar f
5 1 cv setvar x
6 ccn class Cn
7 3 cv setvar y
8 5 7 6 co class x Cn y
9 vg setvar g
10 vh setvar h
11 ctx class × t
12 cii class II
13 5 12 11 co class x × t II
14 13 7 6 co class x × t II Cn y
15 vs setvar s
16 5 cuni class ⋃ x
17 15 cv setvar s
18 10 cv setvar h
19 cc0 class 0
20 17 19 18 co class s h 0
21 4 cv setvar f
22 17 21 cfv class f ⁡ s
23 20 22 wceq wff s h 0 = f ⁡ s
24 c1 class 1
25 17 24 18 co class s h 1
26 9 cv setvar g
27 17 26 cfv class g ⁡ s
28 25 27 wceq wff s h 1 = g ⁡ s
29 23 28 wa wff s h 0 = f ⁡ s ∧ s h 1 = g ⁡ s
30 29 15 16 wral wff ∀ s ∈ ⋃ x s h 0 = f ⁡ s ∧ s h 1 = g ⁡ s
31 30 10 14 crab class h ∈ x × t II Cn y | ∀ s ∈ ⋃ x s h 0 = f ⁡ s ∧ s h 1 = g ⁡ s
32 4 9 8 8 31 cmpo class f ∈ x Cn y , g ∈ x Cn y ⟼ h ∈ x × t II Cn y | ∀ s ∈ ⋃ x s h 0 = f ⁡ s ∧ s h 1 = g ⁡ s
33 1 3 2 2 32 cmpo class x ∈ Top , y ∈ Top ⟼ f ∈ x Cn y , g ∈ x Cn y ⟼ h ∈ x × t II Cn y | ∀ s ∈ ⋃ x s h 0 = f ⁡ s ∧ s h 1 = g ⁡ s
34 0 33 wceq wff Htpy = x ∈ Top , y ∈ Top ⟼ f ∈ x Cn y , g ∈ x Cn y ⟼ h ∈ x × t II Cn y | ∀ s ∈ ⋃ x s h 0 = f ⁡ s ∧ s h 1 = g ⁡ s