Metamath Proof Explorer

Theorem ishtpyd

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

Ref Expression
Hypotheses ishtpy.1 ⊢ φ → J ∈ TopOn ⁡ X
ishtpy.3 ⊢ φ → F ∈ J Cn K
ishtpy.4 ⊢ φ → G ∈ J Cn K
ishtpyd.1 ⊢ φ → H ∈ J × t II Cn K
ishtpyd.2 ⊢ φ ∧ s ∈ X → s H 0 = F ⁡ s
ishtpyd.3 ⊢ φ ∧ s ∈ X → s H 1 = G ⁡ s
Assertion ishtpyd ⊢ φ → H ∈ F J Htpy K G

Proof

Step Hyp Ref Expression
1 ishtpy.1 ⊢ φ → J ∈ TopOn ⁡ X
2 ishtpy.3 ⊢ φ → F ∈ J Cn K
3 ishtpy.4 ⊢ φ → G ∈ J Cn K
4 ishtpyd.1 ⊢ φ → H ∈ J × t II Cn K
5 ishtpyd.2 ⊢ φ ∧ s ∈ X → s H 0 = F ⁡ s
6 ishtpyd.3 ⊢ φ ∧ s ∈ X → s H 1 = G ⁡ s
7 5 6 jca ⊢ φ ∧ s ∈ X → s H 0 = F ⁡ s ∧ s H 1 = G ⁡ s
8 7 ralrimiva ⊢ φ → ∀ s ∈ X s H 0 = F ⁡ s ∧ s H 1 = G ⁡ s
9 1 2 3 ishtpy ⊢ φ → H ∈ F J Htpy K G ↔ H ∈ J × t II Cn K ∧ ∀ s ∈ X s H 0 = F ⁡ s ∧ s H 1 = G ⁡ s
10 4 8 9 mpbir2and ⊢ φ → H ∈ F J Htpy K G