Metamath Proof Explorer


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 ) )