Metamath Proof Explorer

Theorem ishtpy

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)

Ref Expression
Hypotheses ishtpy.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
ishtpy.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
ishtpy.4 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion ishtpy ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ↔ ( 𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∧ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ishtpy.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 ishtpy.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3 ishtpy.4 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
4 df-htpy ⊢ Htpy = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑓 ∈ ( 𝑗 Cn 𝑘 ) , 𝑔 ∈ ( 𝑗 Cn 𝑘 ) ↦ { ℎ ∈ ( ( 𝑗 ×t II ) Cn 𝑘 ) ∣ ∀ 𝑠 ∈ ∪ 𝑗 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) )
5 4 a1i ⊢ ( 𝜑 → Htpy = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑓 ∈ ( 𝑗 Cn 𝑘 ) , 𝑔 ∈ ( 𝑗 Cn 𝑘 ) ↦ { ℎ ∈ ( ( 𝑗 ×t II ) Cn 𝑘 ) ∣ ∀ 𝑠 ∈ ∪ 𝑗 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) ) )
6 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑗 = 𝐽 )
7 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑘 = 𝐾 )
8 6 7 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( 𝑗 Cn 𝑘 ) = ( 𝐽 Cn 𝐾 ) )
9 6 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( 𝑗 ×t II ) = ( 𝐽 ×t II ) )
10 9 7 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( ( 𝑗 ×t II ) Cn 𝑘 ) = ( ( 𝐽 ×t II ) Cn 𝐾 ) )
11 6 unieqd ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑗 = ∪ 𝐽 )
12 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
13 1 12 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑋 = ∪ 𝐽 )
15 11 14 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑗 = 𝑋 )
16 15 raleqdv ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( ∀ 𝑠 ∈ ∪ 𝑗 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) ↔ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) ) )
17 10 16 rabeqbidv ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → { ℎ ∈ ( ( 𝑗 ×t II ) Cn 𝑘 ) ∣ ∀ 𝑠 ∈ ∪ 𝑗 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } = { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } )
18 8 8 17 mpoeq123dv ⊢ ( ( 𝜑 ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( 𝑓 ∈ ( 𝑗 Cn 𝑘 ) , 𝑔 ∈ ( 𝑗 Cn 𝑘 ) ↦ { ℎ ∈ ( ( 𝑗 ×t II ) Cn 𝑘 ) ∣ ∀ 𝑠 ∈ ∪ 𝑗 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) = ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) )
19 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
20 1 19 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
21 cntop2 ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
22 2 21 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
23 ovex ⊢ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∈ V
24 ssrab2 ⊢ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 )
25 23 24 elpwi2 ⊢ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ∈ 𝒫 ( ( 𝐽 ×t II ) Cn 𝐾 )
26 25 rgen2w ⊢ ∀ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∀ 𝑔 ∈ ( 𝐽 Cn 𝐾 ) { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ∈ 𝒫 ( ( 𝐽 ×t II ) Cn 𝐾 )
27 eqid ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) = ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } )
28 27 fmpo ⊢ ( ∀ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∀ 𝑔 ∈ ( 𝐽 Cn 𝐾 ) { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ∈ 𝒫 ( ( 𝐽 ×t II ) Cn 𝐾 ) ↔ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) : ( ( 𝐽 Cn 𝐾 ) × ( 𝐽 Cn 𝐾 ) ) ⟶ 𝒫 ( ( 𝐽 ×t II ) Cn 𝐾 ) )
29 26 28 mpbi ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) : ( ( 𝐽 Cn 𝐾 ) × ( 𝐽 Cn 𝐾 ) ) ⟶ 𝒫 ( ( 𝐽 ×t II ) Cn 𝐾 )
30 ovex ⊢ ( 𝐽 Cn 𝐾 ) ∈ V
31 30 30 xpex ⊢ ( ( 𝐽 Cn 𝐾 ) × ( 𝐽 Cn 𝐾 ) ) ∈ V
32 23 pwex ⊢ 𝒫 ( ( 𝐽 ×t II ) Cn 𝐾 ) ∈ V
33 fex2 ⊢ ( ( ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) : ( ( 𝐽 Cn 𝐾 ) × ( 𝐽 Cn 𝐾 ) ) ⟶ 𝒫 ( ( 𝐽 ×t II ) Cn 𝐾 ) ∧ ( ( 𝐽 Cn 𝐾 ) × ( 𝐽 Cn 𝐾 ) ) ∈ V ∧ 𝒫 ( ( 𝐽 ×t II ) Cn 𝐾 ) ∈ V ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) ∈ V )
34 29 31 32 33 mp3an ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) ∈ V
35 34 a1i ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) ∈ V )
36 5 18 20 22 35 ovmpod ⊢ ( 𝜑 → ( 𝐽 Htpy 𝐾 ) = ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) , 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ↦ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } ) )
37 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑠 ) )
38 37 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ↔ ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ) )
39 fveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑠 ) )
40 39 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ↔ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) )
41 38 40 bi2anan9 ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) ↔ ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) )
42 41 adantl ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) ↔ ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) )
43 42 ralbidv ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → ( ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) ↔ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) )
44 43 rabbidv ⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) ) → { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝑓 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝑔 ‘ 𝑠 ) ) } = { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) } )
45 23 rabex ⊢ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) } ∈ V
46 45 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) } ∈ V )
47 36 44 2 3 46 ovmpod ⊢ ( 𝜑 → ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) = { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) } )
48 47 eleq2d ⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ↔ 𝐻 ∈ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) } ) )
49 oveq ⊢ ( ℎ = 𝐻 → ( 𝑠 ℎ 0 ) = ( 𝑠 𝐻 0 ) )
50 49 eqeq1d ⊢ ( ℎ = 𝐻 → ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ↔ ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ) )
51 oveq ⊢ ( ℎ = 𝐻 → ( 𝑠 ℎ 1 ) = ( 𝑠 𝐻 1 ) )
52 51 eqeq1d ⊢ ( ℎ = 𝐻 → ( ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ↔ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) )
53 50 52 anbi12d ⊢ ( ℎ = 𝐻 → ( ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) ↔ ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) )
54 53 ralbidv ⊢ ( ℎ = 𝐻 → ( ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) ↔ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) )
55 54 elrab ⊢ ( 𝐻 ∈ { ℎ ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∣ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 ℎ 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 ℎ 1 ) = ( 𝐺 ‘ 𝑠 ) ) } ↔ ( 𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∧ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) )
56 48 55 bitrdi ⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ↔ ( 𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∧ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) ) )