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 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
isphtpy.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
Assertion isphtpy ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ↔ ( 𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∧ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
2 isphtpy.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
3 cntop2 ⊢ ( 𝐹 ∈ ( II Cn 𝐽 ) → 𝐽 ∈ Top )
4 oveq2 ⊢ ( 𝑗 = 𝐽 → ( II Cn 𝑗 ) = ( II Cn 𝐽 ) )
5 oveq2 ⊢ ( 𝑗 = 𝐽 → ( II Htpy 𝑗 ) = ( II Htpy 𝐽 ) )
6 5 oveqd ⊢ ( 𝑗 = 𝐽 → ( 𝑓 ( II Htpy 𝑗 ) 𝑔 ) = ( 𝑓 ( II Htpy 𝐽 ) 𝑔 ) )
7 6 rabeqdv ⊢ ( 𝑗 = 𝐽 → { ℎ ∈ ( 𝑓 ( II Htpy 𝑗 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } = { ℎ ∈ ( 𝑓 ( II Htpy 𝐽 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } )
8 4 4 7 mpoeq123dv ⊢ ( 𝑗 = 𝐽 → ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝑗 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } ) = ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝐽 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } ) )
9 df-phtpy ⊢ PHtpy = ( 𝑗 ∈ Top ↦ ( 𝑓 ∈ ( II Cn 𝑗 ) , 𝑔 ∈ ( II Cn 𝑗 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝑗 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } ) )
10 ovex ⊢ ( II Cn 𝐽 ) ∈ V
11 10 10 mpoex ⊢ ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝐽 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } ) ∈ V
12 8 9 11 fvmpt ⊢ ( 𝐽 ∈ Top → ( PHtpy ‘ 𝐽 ) = ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝐽 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } ) )
13 1 3 12 3syl ⊢ ( 𝜑 → ( PHtpy ‘ 𝐽 ) = ( 𝑓 ∈ ( II Cn 𝐽 ) , 𝑔 ∈ ( II Cn 𝐽 ) ↦ { ℎ ∈ ( 𝑓 ( II Htpy 𝐽 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } ) )
14 oveq12 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ( II Htpy 𝐽 ) 𝑔 ) = ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
15 simpl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
16 15 fveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ 0 ) = ( 𝐹 ‘ 0 ) )
17 16 eqeq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ↔ ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ) )
18 15 fveq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( 𝑓 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
19 18 eqeq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ↔ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) )
20 17 19 anbi12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) ↔ ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) )
21 20 ralbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) )
22 14 21 rabeqbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → { ℎ ∈ ( 𝑓 ( II Htpy 𝐽 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } = { ℎ ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) } )
23 22 adantl ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → { ℎ ∈ ( 𝑓 ( II Htpy 𝐽 ) 𝑔 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝑓 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝑓 ‘ 1 ) ) } = { ℎ ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) } )
24 ovex ⊢ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∈ V
25 24 rabex ⊢ { ℎ ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) } ∈ V
26 25 a1i ⊢ ( 𝜑 → { ℎ ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) } ∈ V )
27 13 23 1 2 26 ovmpod ⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) = { ℎ ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) } )
28 27 eleq2d ⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ↔ 𝐻 ∈ { ℎ ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) } ) )
29 oveq ⊢ ( ℎ = 𝐻 → ( 0 ℎ 𝑠 ) = ( 0 𝐻 𝑠 ) )
30 29 eqeq1d ⊢ ( ℎ = 𝐻 → ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ↔ ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ) )
31 oveq ⊢ ( ℎ = 𝐻 → ( 1 ℎ 𝑠 ) = ( 1 𝐻 𝑠 ) )
32 31 eqeq1d ⊢ ( ℎ = 𝐻 → ( ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ↔ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) )
33 30 32 anbi12d ⊢ ( ℎ = 𝐻 → ( ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) ↔ ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) )
34 33 ralbidv ⊢ ( ℎ = 𝐻 → ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) ↔ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) )
35 34 elrab ⊢ ( 𝐻 ∈ { ℎ ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∣ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 ℎ 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 ℎ 𝑠 ) = ( 𝐹 ‘ 1 ) ) } ↔ ( 𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∧ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) )
36 28 35 bitrdi ⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ↔ ( 𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∧ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) ) )