Theorem fourierdlem17

Description: The defined L is actually a function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem17.a	|- ( ph -> A e. RR )
	fourierdlem17.b	|- ( ph -> B e. RR )
	fourierdlem17.altb	|- ( ph -> A < B )
	fourierdlem17.l	|- L = ( x e. ( A (,] B ) |-> if ( x = B , A , x ) )
Assertion	fourierdlem17	|- ( ph -> L : ( A (,] B ) --> ( A [,] B ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem17.a	|- ( ph -> A e. RR )
2		fourierdlem17.b	|- ( ph -> B e. RR )
3		fourierdlem17.altb	|- ( ph -> A < B )
4		fourierdlem17.l	|- L = ( x e. ( A (,] B ) |-> if ( x = B , A , x ) )
5	1	leidd	|- ( ph -> A <_ A )
6	1 2 3	ltled	|- ( ph -> A <_ B )
7	1 2 1 5 6	eliccd	|- ( ph -> A e. ( A [,] B ) )
8	7	ad2antrr	|- ( ( ( ph /\ x e. ( A (,] B ) ) /\ x = B ) -> A e. ( A [,] B ) )
9		iocssicc	|- ( A (,] B ) C_ ( A [,] B )
10	9	sseli	|- ( x e. ( A (,] B ) -> x e. ( A [,] B ) )
11	10	ad2antlr	|- ( ( ( ph /\ x e. ( A (,] B ) ) /\ -. x = B ) -> x e. ( A [,] B ) )
12	8 11	ifclda	|- ( ( ph /\ x e. ( A (,] B ) ) -> if ( x = B , A , x ) e. ( A [,] B ) )
13	12 4	fmptd	|- ( ph -> L : ( A (,] B ) --> ( A [,] B ) )