Theorem oprpiece1res2 21180

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

Hypotheses

Ref	Expression
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.9	|- ( x = K -> R = P )
oprpiece1.10	|- ( x = K -> S = Q )
oprpiece1.11	|- ( y e. C -> P = Q )
oprpiece1.12	|- G = ( x e. ( K [,] B ) , y e. C |-> S )

Assertion

Ref	Expression
oprpiece1res2	|- ( F |` ( ( K [,] B ) X. C ) ) = G

Distinct variable groups:   x, A, y   x, B, y   x, C, y   x, K, y   x, P   x, Q

Allowed substitution hints:   P( y)   Q( y)   R( x, y)   S( x, y)   F( x, y)   G( x, y)

Proof of Theorem oprpiece1res2

Step	Hyp	Ref	Expression
1		oprpiece1.6	. . . 4 |- K e. ( A [,] B )
2		oprpiece1.1	. . . . . 6 |- A e. RR
3	2	rexri 9635	. . . . 5 |- A e. RR*
4		oprpiece1.2	. . . . . 6 |- B e. RR
5	4	rexri 9635	. . . . 5 |- B e. RR*
6		oprpiece1.3	. . . . 5 |- A <_ B
7		ubicc2 11626	. . . . 5 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
8	3, 5, 6, 7	mp3an 1319	. . . 4 |- B e. ( A [,] B )
9		iccss2 11584	. . . 4 |- ( ( K e. ( A [,] B ) /\ B e. ( A [,] B ) ) -> ( K [,] B ) C_ ( A [,] B ) )
10	1, 8, 9	mp2an 672	. . 3 |- ( K [,] B ) C_ ( A [,] B )
11		ssid 3516	. . 3 |- C C_ C
12		resmpt2 6375	. . 3 |- ( ( ( 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 ) ) )
13	10, 11, 12	mp2an 672	. 2 |- ( ( 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 ) )
14		oprpiece1.7	. . 3 |- F = ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) )
15	14	reseq1i 5260	. 2 |- ( F |` ( ( K [,] B ) X. C ) ) = ( ( x e. ( A [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) |` ( ( K [,] B ) X. C ) )
16		oprpiece1.12	. . 3 |- G = ( x e. ( K [,] B ) , y e. C |-> S )
17		eqeq1 2464	. . . . 5 |- ( R = if ( x <_ K , R , S ) -> ( R = S <-> if ( x <_ K , R , S ) = S ) )
18		eqeq1 2464	. . . . 5 |- ( S = if ( x <_ K , R , S ) -> ( S = S <-> if ( x <_ K , R , S ) = S ) )
19		oprpiece1.11	. . . . . . 7 |- ( y e. C -> P = Q )
20	19	ad2antlr 726	. . . . . 6 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> P = Q )
21		simpr 461	. . . . . . . 8 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> x <_ K )
22	2, 4	elicc2i 11579	. . . . . . . . . . . . 13 |- ( K e. ( A [,] B ) <-> ( K e. RR /\ A <_ K /\ K <_ B ) )
23	22	simp1bi 1006	. . . . . . . . . . . 12 |- ( K e. ( A [,] B ) -> K e. RR )
24	1, 23	ax-mp 5	. . . . . . . . . . 11 |- K e. RR
25	24, 4	elicc2i 11579	. . . . . . . . . 10 |- ( x e. ( K [,] B ) <-> ( x e. RR /\ K <_ x /\ x <_ B ) )
26	25	simp2bi 1007	. . . . . . . . 9 |- ( x e. ( K [,] B ) -> K <_ x )
27	26	ad2antrr 725	. . . . . . . 8 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> K <_ x )
28	25	simp1bi 1006	. . . . . . . . . 10 |- ( x e. ( K [,] B ) -> x e. RR )
29	28	ad2antrr 725	. . . . . . . . 9 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> x e. RR )
30		letri3 9659	. . . . . . . . 9 |- ( ( x e. RR /\ K e. RR ) -> ( x = K <-> ( x <_ K /\ K <_ x ) ) )
31	29, 24, 30	sylancl 662	. . . . . . . 8 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> ( x = K <-> ( x <_ K /\ K <_ x ) ) )
32	21, 27, 31	mpbir2and 915	. . . . . . 7 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> x = K )
33		oprpiece1.9	. . . . . . 7 |- ( x = K -> R = P )
34	32, 33	syl 16	. . . . . 6 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> R = P )
35		oprpiece1.10	. . . . . . 7 |- ( x = K -> S = Q )
36	32, 35	syl 16	. . . . . 6 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> S = Q )
37	20, 34, 36	3eqtr4d 2511	. . . . 5 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ x <_ K ) -> R = S )
38		eqidd 2461	. . . . 5 |- ( ( ( x e. ( K [,] B ) /\ y e. C ) /\ -. x <_ K ) -> S = S )
39	17, 18, 37, 38	ifbothda 3967	. . . 4 |- ( ( x e. ( K [,] B ) /\ y e. C ) -> if ( x <_ K , R , S ) = S )
40	39	mpt2eq3ia 6337	. . 3 |- ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) ) = ( x e. ( K [,] B ) , y e. C |-> S )
41	16, 40	eqtr4i 2492	. 2 |- G = ( x e. ( K [,] B ) , y e. C |-> if ( x <_ K , R , S ) )
42	13, 15, 41	3eqtr4i 2499	1 |- ( F |` ( ( K [,] B ) X. C ) ) = G

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1374   e. wcel 1762   _Vcvv 3106   C_ wss 3469   ifcif 3932   class class class wbr 4440   X. cxp 4990   |` cres 4994  (class class class)co 6275   |-> cmpt2 6277   RRcr 9480   RR*cxr 9616   <_ cle 9618   [,]cicc 11521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-cnex 9537  ax-resscn 9538  ax-pre-lttri 9555  ax-pre-lttrn 9556

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-po 4793  df-so 4794  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6774  df-2nd 6775  df-er 7301  df-en 7507  df-dom 7508  df-sdom 7509  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-icc 11525

This theorem is referenced by: (None)