Theorem ishtpyd

Description: Deduction for membership in the class of homotopies. (Contributed by Mario Carneiro, 22-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ishtpy.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		ishtpy.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3		ishtpy.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
4		ishtpyd.1	⊢ ( 𝜑 → 𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
5		ishtpyd.2	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) )
6		ishtpyd.3	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) )
7	5 6	jca	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑋 ) → ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) )
8	7	ralrimiva	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) )
9	1 2 3	ishtpy	⊢ ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ↔ ( 𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) ∧ ∀ 𝑠 ∈ 𝑋 ( ( 𝑠 𝐻 0 ) = ( 𝐹 ‘ 𝑠 ) ∧ ( 𝑠 𝐻 1 ) = ( 𝐺 ‘ 𝑠 ) ) ) ) )
10	4 8 9	mpbir2and	⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )