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] \times \{Y\}$
	Assertion	pcoptcl	$⊢ (J \in TopOn (X) \land Y \in X) \to (P \in (II Cn J) \land P (0) = Y \land P (1) = Y)$

Proof

Step	Hyp	Ref	Expression
1		pcopt.1	$⊢ P = [0, 1] \times \{Y\}$
2		iitopon	$⊢ II \in TopOn ([0, 1])$
3		cnconst2	$⊢ (II \in TopOn ([0, 1]) \land J \in TopOn (X) \land Y \in X) \to [0, 1] \times \{Y\} \in (II Cn J)$
4	2 3	mp3an1	$⊢ (J \in TopOn (X) \land Y \in X) \to [0, 1] \times \{Y\} \in (II Cn J)$
5	1 4	eqeltrid	$⊢ (J \in TopOn (X) \land Y \in X) \to P \in (II Cn J)$
6	1	fveq1i	$⊢ P (0) = ([0, 1] \times \{Y\}) (0)$
7		simpr	$⊢ (J \in TopOn (X) \land Y \in X) \to Y \in X$
8		0elunit	$⊢ 0 \in [0, 1]$
9		fvconst2g	$⊢ (Y \in X \land 0 \in [0, 1]) \to ([0, 1] \times \{Y\}) (0) = Y$
10	7 8 9	sylancl	$⊢ (J \in TopOn (X) \land Y \in X) \to ([0, 1] \times \{Y\}) (0) = Y$
11	6 10	eqtrid	$⊢ (J \in TopOn (X) \land Y \in X) \to P (0) = Y$
12	1	fveq1i	$⊢ P (1) = ([0, 1] \times \{Y\}) (1)$
13		1elunit	$⊢ 1 \in [0, 1]$
14		fvconst2g	$⊢ (Y \in X \land 1 \in [0, 1]) \to ([0, 1] \times \{Y\}) (1) = Y$
15	7 13 14	sylancl	$⊢ (J \in TopOn (X) \land Y \in X) \to ([0, 1] \times \{Y\}) (1) = Y$
16	12 15	eqtrid	$⊢ (J \in TopOn (X) \land Y \in X) \to P (1) = Y$
17	5 11 16	3jca	$⊢ (J \in TopOn (X) \land Y \in X) \to (P \in (II Cn J) \land P (0) = Y \land P (1) = Y)$