Metamath Proof Explorer

Theorem pcoptcl

Description: A constant function is a path from Y to itself. (Contributed by Mario Carneiro, 12-Feb-2015) (Revised by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypothesis pcopt.1 ⊢ P = 0 1 × Y
Assertion pcoptcl ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → P ∈ II Cn J ∧ P ⁡ 0 = Y ∧ P ⁡ 1 = Y

Proof

Step Hyp Ref Expression
1 pcopt.1 ⊢ P = 0 1 × Y
2 iitopon ⊢ II ∈ TopOn ⁡ 0 1
3 cnconst2 ⊢ II ∈ TopOn ⁡ 0 1 ∧ J ∈ TopOn ⁡ X ∧ Y ∈ X → 0 1 × Y ∈ II Cn J
4 2 3 mp3an1 ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → 0 1 × Y ∈ II Cn J
5 1 4 eqeltrid ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → P ∈ II Cn J
6 1 fveq1i ⊢ P ⁡ 0 = 0 1 × Y ⁡ 0
7 simpr ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → Y ∈ X
8 0elunit ⊢ 0 ∈ 0 1
9 fvconst2g ⊢ Y ∈ X ∧ 0 ∈ 0 1 → 0 1 × Y ⁡ 0 = Y
10 7 8 9 sylancl ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → 0 1 × Y ⁡ 0 = Y
11 6 10 eqtrid ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → P ⁡ 0 = Y
12 1 fveq1i ⊢ P ⁡ 1 = 0 1 × Y ⁡ 1
13 1elunit ⊢ 1 ∈ 0 1
14 fvconst2g ⊢ Y ∈ X ∧ 1 ∈ 0 1 → 0 1 × Y ⁡ 1 = Y
15 7 13 14 sylancl ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → 0 1 × Y ⁡ 1 = Y
16 12 15 eqtrid ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → P ⁡ 1 = Y
17 5 11 16 3jca ⊢ J ∈ TopOn ⁡ X ∧ Y ∈ X → P ∈ II Cn J ∧ P ⁡ 0 = Y ∧ P ⁡ 1 = Y