Metamath Proof Explorer

Theorem oprpiece1res1

Description: Restriction to the first part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010) (Proof shortened by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses oprpiece1.1 
|- A e. RR
oprpiece1.2 
|- B e. RR
oprpiece1.3 
|- A <_ B
oprpiece1.4 
|- R e. _V
oprpiece1.5 
|- S e. _V
oprpiece1.6 
|- K e. ( A [,] B )
oprpiece1.7 
|- F = ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) )
oprpiece1.8 
|- G = ( x e. ( A [,] K ) , y e. C |-> R )
Assertion oprpiece1res1 
|- ( F |` ( ( A [,] K ) X. C ) ) = G

Proof

Step Hyp Ref Expression
1 oprpiece1.1 
 |-  A e. RR
2 oprpiece1.2 
 |-  B e. RR
3 oprpiece1.3 
 |-  A <_ B
4 oprpiece1.4 
 |-  R e. _V
5 oprpiece1.5 
 |-  S e. _V
6 oprpiece1.6 
 |-  K e. ( A [,] B )
7 oprpiece1.7 
 |-  F = ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) )
8 oprpiece1.8 
 |-  G = ( x e. ( A [,] K ) , y e. C |-> R )
9 1 rexri 
 |-  A e. RR*
10 2 rexri 
 |-  B e. RR*
11 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
12 9 10 3 11 mp3an 
 |-  A e. ( A [,] B )
13 iccss2 
 |-  ( ( A e. ( A [,] B ) /\ K e. ( A [,] B ) ) -> ( A [,] K ) C_ ( A [,] B ) )
14 12 6 13 mp2an 
 |-  ( A [,] K ) C_ ( A [,] B )
15 ssid 
 |-  C C_ C
16 resmpo 
 |-  ( ( ( A [,] K ) C_ ( A [,] B ) /\ C C_ C ) -> ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( A [,] K ) X. C ) ) = ( x e. ( A [,] K ) , y e. C |-> if ( x <_ K , R , S ) ) )
17 14 15 16 mp2an 
 |-  ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( A [,] K ) X. C ) ) = ( x e. ( A [,] K ) , y e. C |-> if ( x <_ K , R , S ) )
18 7 reseq1i 
 |-  ( F |` ( ( A [,] K ) X. C ) ) = ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( A [,] K ) X. C ) )
19 eliccxr 
 |-  ( K e. ( A [,] B ) -> K e. RR* )
20 6 19 ax-mp 
 |-  K e. RR*
21 iccleub 
 |-  ( ( A e. RR* /\ K e. RR* /\ x e. ( A [,] K ) ) -> x <_ K )
22 9 20 21 mp3an12 
 |-  ( x e. ( A [,] K ) -> x <_ K )
23 22 iftrued 
 |-  ( x e. ( A [,] K ) -> if ( x <_ K , R , S ) = R )
24 23 adantr 
 |-  ( ( x e. ( A [,] K ) /\ y e. C ) -> if ( x <_ K , R , S ) = R )
25 24 mpoeq3ia 
 |-  ( x e. ( A [,] K ) , y e. C |-> if ( x <_ K , R , S ) ) = ( x e. ( A [,] K ) , y e. C |-> R )
26 8 25 eqtr4i 
 |-  G = ( x e. ( A [,] K ) , y e. C |-> if ( x <_ K , R , S ) )
27 17 18 26 3eqtr4i 
 |-  ( F |` ( ( A [,] K ) X. C ) ) = G