Metamath Proof Explorer

Theorem isphtpy

Description: Membership in the class of path homotopies between two continuous functions. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses isphtpy.2 ⊢ φ → F ∈ II Cn J
isphtpy.3 ⊢ φ → G ∈ II Cn J
Assertion isphtpy ⊢ φ → H ∈ F PHtpy ⁡ J G ↔ H ∈ F II Htpy J G ∧ ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢ φ → F ∈ II Cn J
2 isphtpy.3 ⊢ φ → G ∈ II Cn J
3 cntop2 ⊢ F ∈ II Cn J → J ∈ Top
4 oveq2 ⊢ j = J → II Cn j = II Cn J
5 oveq2 ⊢ j = J → II Htpy j = II Htpy J
6 5 oveqd ⊢ j = J → f II Htpy j g = f II Htpy J g
7 6 rabeqdv ⊢ j = J → h ∈ f II Htpy j g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1 = h ∈ f II Htpy J g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
8 4 4 7 mpoeq123dv ⊢ j = J → f ∈ II Cn j , g ∈ II Cn j ⟼ h ∈ f II Htpy j g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1 = f ∈ II Cn J , g ∈ II Cn J ⟼ h ∈ f II Htpy J g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
9 df-phtpy ⊢ PHtpy = j ∈ Top ⟼ f ∈ II Cn j , g ∈ II Cn j ⟼ h ∈ f II Htpy j g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
10 ovex ⊢ II Cn J ∈ V
11 10 10 mpoex ⊢ f ∈ II Cn J , g ∈ II Cn J ⟼ h ∈ f II Htpy J g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1 ∈ V
12 8 9 11 fvmpt ⊢ J ∈ Top → PHtpy ⁡ J = f ∈ II Cn J , g ∈ II Cn J ⟼ h ∈ f II Htpy J g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
13 1 3 12 3syl ⊢ φ → PHtpy ⁡ J = f ∈ II Cn J , g ∈ II Cn J ⟼ h ∈ f II Htpy J g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1
14 oveq12 ⊢ f = F ∧ g = G → f II Htpy J g = F II Htpy J G
15 simpl ⊢ f = F ∧ g = G → f = F
16 15 fveq1d ⊢ f = F ∧ g = G → f ⁡ 0 = F ⁡ 0
17 16 eqeq2d ⊢ f = F ∧ g = G → 0 h s = f ⁡ 0 ↔ 0 h s = F ⁡ 0
18 15 fveq1d ⊢ f = F ∧ g = G → f ⁡ 1 = F ⁡ 1
19 18 eqeq2d ⊢ f = F ∧ g = G → 1 h s = f ⁡ 1 ↔ 1 h s = F ⁡ 1
20 17 19 anbi12d ⊢ f = F ∧ g = G → 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1 ↔ 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1
21 20 ralbidv ⊢ f = F ∧ g = G → ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1 ↔ ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1
22 14 21 rabeqbidv ⊢ f = F ∧ g = G → h ∈ f II Htpy J g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1 = h ∈ F II Htpy J G | ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1
23 22 adantl ⊢ φ ∧ f = F ∧ g = G → h ∈ f II Htpy J g | ∀ s ∈ 0 1 0 h s = f ⁡ 0 ∧ 1 h s = f ⁡ 1 = h ∈ F II Htpy J G | ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1
24 ovex ⊢ F II Htpy J G ∈ V
25 24 rabex ⊢ h ∈ F II Htpy J G | ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1 ∈ V
26 25 a1i ⊢ φ → h ∈ F II Htpy J G | ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1 ∈ V
27 13 23 1 2 26 ovmpod ⊢ φ → F PHtpy ⁡ J G = h ∈ F II Htpy J G | ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1
28 27 eleq2d ⊢ φ → H ∈ F PHtpy ⁡ J G ↔ H ∈ h ∈ F II Htpy J G | ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1
29 oveq ⊢ h = H → 0 h s = 0 H s
30 29 eqeq1d ⊢ h = H → 0 h s = F ⁡ 0 ↔ 0 H s = F ⁡ 0
31 oveq ⊢ h = H → 1 h s = 1 H s
32 31 eqeq1d ⊢ h = H → 1 h s = F ⁡ 1 ↔ 1 H s = F ⁡ 1
33 30 32 anbi12d ⊢ h = H → 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1 ↔ 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
34 33 ralbidv ⊢ h = H → ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1 ↔ ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
35 34 elrab ⊢ H ∈ h ∈ F II Htpy J G | ∀ s ∈ 0 1 0 h s = F ⁡ 0 ∧ 1 h s = F ⁡ 1 ↔ H ∈ F II Htpy J G ∧ ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1
36 28 35 bitrdi ⊢ φ → H ∈ F PHtpy ⁡ J G ↔ H ∈ F II Htpy J G ∧ ∀ s ∈ 0 1 0 H s = F ⁡ 0 ∧ 1 H s = F ⁡ 1