This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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