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 |