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.9 |
|- ( x = K -> R = P ) |
9 |
|
oprpiece1.10 |
|- ( x = K -> S = Q ) |
10 |
|
oprpiece1.11 |
|- ( y e. C -> P = Q ) |
11 |
|
oprpiece1.12 |
|- G = ( x e. ( K [,] B ) , y e. C |-> S ) |
12 |
1
|
rexri |
|- A e. RR* |
13 |
2
|
rexri |
|- B e. RR* |
14 |
|
ubicc2 |
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) ) |
15 |
12 13 3 14
|
mp3an |
|- B e. ( A [,] B ) |
16 |
|
iccss2 |
|- ( ( K e. ( A [,] B ) /\ B e. ( A [,] B ) ) -> ( K [,] B ) C_ ( A [,] B ) ) |
17 |
6 15 16
|
mp2an |
|- ( K [,] B ) C_ ( A [,] B ) |
18 |
|
ssid |
|- C C_ C |
19 |
|
resmpo |
|- ( ( ( K [,] B ) C_ ( A [,] B ) /\ C C_ C ) -> ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( K [,] B ) X. C ) ) = ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) ) |
20 |
17 18 19
|
mp2an |
|- ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( K [,] B ) X. C ) ) = ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |
21 |
7
|
reseq1i |
|- ( F |` ( ( K [,] B ) X. C ) ) = ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( K [,] B ) X. C ) ) |
22 |
10
|
ad2antlr |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> P = Q ) |
23 |
|
simpr |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> x <_ K ) |
24 |
1 2
|
elicc2i |
|- ( K e. ( A [,] B ) <-> ( K e. RR /\ A <_ K /\ K <_ B ) ) |
25 |
24
|
simp1bi |
|- ( K e. ( A [,] B ) -> K e. RR ) |
26 |
6 25
|
ax-mp |
|- K e. RR |
27 |
26 2
|
elicc2i |
|- ( x e. ( K [,] B ) <-> ( x e. RR /\ K <_ x /\ x <_ B ) ) |
28 |
27
|
simp2bi |
|- ( x e. ( K [,] B ) -> K <_ x ) |
29 |
28
|
ad2antrr |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> K <_ x ) |
30 |
27
|
simp1bi |
|- ( x e. ( K [,] B ) -> x e. RR ) |
31 |
30
|
ad2antrr |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> x e. RR ) |
32 |
|
letri3 |
|- ( ( x e. RR /\ K e. RR ) -> ( x = K <-> ( x <_ K /\ K <_ x ) ) ) |
33 |
31 26 32
|
sylancl |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> ( x = K <-> ( x <_ K /\ K <_ x ) ) ) |
34 |
23 29 33
|
mpbir2and |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> x = K ) |
35 |
34 8
|
syl |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> R = P ) |
36 |
34 9
|
syl |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> S = Q ) |
37 |
22 35 36
|
3eqtr4d |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> R = S ) |
38 |
|
eqidd |
|- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ -. x <_ K ) -> S = S ) |
39 |
37 38
|
ifeqda |
|- ( ( x e. ( K [,] B ) /\ y e. C ) -> if ( x <_ K , R , S ) = S ) |
40 |
39
|
mpoeq3ia |
|- ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) = ( x e. ( K [,] B ) , y e. C |-> S ) |
41 |
11 40
|
eqtr4i |
|- G = ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |
42 |
20 21 41
|
3eqtr4i |
|- ( F |` ( ( K [,] B ) X. C ) ) = G |