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 ) X. { Y } )
Assertion	pcoptcl	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( P e. ( II Cn J ) /\ ( P ` 0 ) = Y /\ ( P ` 1 ) = Y ) )

Proof

Step	Hyp	Ref	Expression
1		pcopt.1	|- P = ( ( 0 [,] 1 ) X. { Y } )
2		iitopon	|- II e. ( TopOn ` ( 0 [,] 1 ) )
3		cnconst2	|- ( ( II e. ( TopOn ` ( 0 [,] 1 ) ) /\ J e. ( TopOn ` X ) /\ Y e. X ) -> ( ( 0 [,] 1 ) X. { Y } ) e. ( II Cn J ) )
4	2 3	mp3an1	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( ( 0 [,] 1 ) X. { Y } ) e. ( II Cn J ) )
5	1 4	eqeltrid	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> P e. ( II Cn J ) )
6	1	fveq1i	|- ( P ` 0 ) = ( ( ( 0 [,] 1 ) X. { Y } ) ` 0 )
7		simpr	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> Y e. X )
8		0elunit	|- 0 e. ( 0 [,] 1 )
9		fvconst2g	|- ( ( Y e. X /\ 0 e. ( 0 [,] 1 ) ) -> ( ( ( 0 [,] 1 ) X. { Y } ) ` 0 ) = Y )
10	7 8 9	sylancl	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( ( ( 0 [,] 1 ) X. { Y } ) ` 0 ) = Y )
11	6 10	syl5eq	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( P ` 0 ) = Y )
12	1	fveq1i	|- ( P ` 1 ) = ( ( ( 0 [,] 1 ) X. { Y } ) ` 1 )
13		1elunit	|- 1 e. ( 0 [,] 1 )
14		fvconst2g	|- ( ( Y e. X /\ 1 e. ( 0 [,] 1 ) ) -> ( ( ( 0 [,] 1 ) X. { Y } ) ` 1 ) = Y )
15	7 13 14	sylancl	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( ( ( 0 [,] 1 ) X. { Y } ) ` 1 ) = Y )
16	12 15	syl5eq	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( P ` 1 ) = Y )
17	5 11 16	3jca	|- ( ( J e. ( TopOn ` X ) /\ Y e. X ) -> ( P e. ( II Cn J ) /\ ( P ` 0 ) = Y /\ ( P ` 1 ) = Y ) )