Theorem brrestrict 32056

Description: Binary relation form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

Hypotheses

Ref	Expression
brrestrict.1	|- A e. _V
brrestrict.2	|- B e. _V
brrestrict.3	|- C e. _V

Assertion

Ref	Expression
brrestrict	|- ( <. A , B >.Restrict C <-> C = ( A |` B ) )

Proof of Theorem brrestrict

Dummy variables a b x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opex 4932	. . . . 5 |- <. A , B >. e. _V
2		brrestrict.3	. . . . 5 |- C e. _V
3	1, 2	brco 5292	. . . 4 |- ( <. A , B >. (Cap o. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) ) C <-> E. x ( <. A , B >. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) x /\ xCap C ) )
4	1	brtxp2 31988	. . . . . . 7 |- ( <. A , B >. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) x <-> E. a E. b ( x = <. a , b >. /\ <. A , B >. 1st a /\ <. A , B >. (Cart o. ( 2nd (x) (Range o. 1st ) ) ) b ) )
5		3anrot 1043	. . . . . . . . 9 |- ( ( x = <. a , b >. /\ <. A , B >. 1st a /\ <. A , B >. (Cart o. ( 2nd (x) (Range o. 1st ) ) ) b ) <-> ( <. A , B >. 1st a /\ <. A , B >. (Cart o. ( 2nd (x) (Range o. 1st ) ) ) b /\ x = <. a , b >. ) )
6		brrestrict.1	. . . . . . . . . . 11 |- A e. _V
7		brrestrict.2	. . . . . . . . . . 11 |- B e. _V
8	6, 7	br1steq 31670	. . . . . . . . . 10 |- ( <. A , B >. 1st a <-> a = A )
9		vex 3203	. . . . . . . . . . . 12 |- b e. _V
10	1, 9	brco 5292	. . . . . . . . . . 11 |- ( <. A , B >. (Cart o. ( 2nd (x) (Range o. 1st ) ) ) b <-> E. x ( <. A , B >. ( 2nd (x) (Range o. 1st ) ) x /\ xCart b ) )
11	1	brtxp2 31988	. . . . . . . . . . . . . . 15 |- ( <. A , B >. ( 2nd (x) (Range o. 1st ) ) x <-> E. a E. b ( x = <. a , b >. /\ <. A , B >. 2nd a /\ <. A , B >. (Range o. 1st ) b ) )
12		3anrot 1043	. . . . . . . . . . . . . . . . 17 |- ( ( x = <. a , b >. /\ <. A , B >. 2nd a /\ <. A , B >. (Range o. 1st ) b ) <-> ( <. A , B >. 2nd a /\ <. A , B >. (Range o. 1st ) b /\ x = <. a , b >. ) )
13	6, 7	br2ndeq 31671	. . . . . . . . . . . . . . . . . 18 |- ( <. A , B >. 2nd a <-> a = B )
14	1, 9	brco 5292	. . . . . . . . . . . . . . . . . . 19 |- ( <. A , B >. (Range o. 1st ) b <-> E. x ( <. A , B >. 1st x /\ xRange b ) )
15	6, 7	br1steq 31670	. . . . . . . . . . . . . . . . . . . . . 22 |- ( <. A , B >. 1st x <-> x = A )
16	15	anbi1i 731	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( <. A , B >. 1st x /\ xRange b ) <-> ( x = A /\ xRange b ) )
17	16	exbii 1774	. . . . . . . . . . . . . . . . . . . 20 |- ( E. x ( <. A , B >. 1st x /\ xRange b ) <-> E. x ( x = A /\ xRange b ) )
18		breq1 4656	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = A -> ( xRange b <-> ARange b ) )
19	6, 18	ceqsexv 3242	. . . . . . . . . . . . . . . . . . . 20 |- ( E. x ( x = A /\ xRange b ) <-> ARange b )
20	17, 19	bitri 264	. . . . . . . . . . . . . . . . . . 19 |- ( E. x ( <. A , B >. 1st x /\ xRange b ) <-> ARange b )
21	6, 9	brrange 32041	. . . . . . . . . . . . . . . . . . 19 |- ( ARange b <-> b = ran A )
22	14, 20, 21	3bitri 286	. . . . . . . . . . . . . . . . . 18 |- ( <. A , B >. (Range o. 1st ) b <-> b = ran A )
23		biid 251	. . . . . . . . . . . . . . . . . 18 |- ( x = <. a , b >. <-> x = <. a , b >. )
24	13, 22, 23	3anbi123i 1251	. . . . . . . . . . . . . . . . 17 |- ( ( <. A , B >. 2nd a /\ <. A , B >. (Range o. 1st ) b /\ x = <. a , b >. ) <-> ( a = B /\ b = ran A /\ x = <. a , b >. ) )
25	12, 24	bitri 264	. . . . . . . . . . . . . . . 16 |- ( ( x = <. a , b >. /\ <. A , B >. 2nd a /\ <. A , B >. (Range o. 1st ) b ) <-> ( a = B /\ b = ran A /\ x = <. a , b >. ) )
26	25	2exbii 1775	. . . . . . . . . . . . . . 15 |- ( E. a E. b ( x = <. a , b >. /\ <. A , B >. 2nd a /\ <. A , B >. (Range o. 1st ) b ) <-> E. a E. b ( a = B /\ b = ran A /\ x = <. a , b >. ) )
27	6	rnex 7100	. . . . . . . . . . . . . . . 16 |- ran A e. _V
28		opeq1 4402	. . . . . . . . . . . . . . . . 17 |- ( a = B -> <. a , b >. = <. B , b >. )
29	28	eqeq2d 2632	. . . . . . . . . . . . . . . 16 |- ( a = B -> ( x = <. a , b >. <-> x = <. B , b >. ) )
30		opeq2 4403	. . . . . . . . . . . . . . . . 17 |- ( b = ran A -> <. B , b >. = <. B , ran A >. )
31	30	eqeq2d 2632	. . . . . . . . . . . . . . . 16 |- ( b = ran A -> ( x = <. B , b >. <-> x = <. B , ran A >. ) )
32	7, 27, 29, 31	ceqsex2v 3245	. . . . . . . . . . . . . . 15 |- ( E. a E. b ( a = B /\ b = ran A /\ x = <. a , b >. ) <-> x = <. B , ran A >. )
33	11, 26, 32	3bitri 286	. . . . . . . . . . . . . 14 |- ( <. A , B >. ( 2nd (x) (Range o. 1st ) ) x <-> x = <. B , ran A >. )
34	33	anbi1i 731	. . . . . . . . . . . . 13 |- ( ( <. A , B >. ( 2nd (x) (Range o. 1st ) ) x /\ xCart b ) <-> ( x = <. B , ran A >. /\ xCart b ) )
35	34	exbii 1774	. . . . . . . . . . . 12 |- ( E. x ( <. A , B >. ( 2nd (x) (Range o. 1st ) ) x /\ xCart b ) <-> E. x ( x = <. B , ran A >. /\ xCart b ) )
36		opex 4932	. . . . . . . . . . . . 13 |- <. B , ran A >. e. _V
37		breq1 4656	. . . . . . . . . . . . 13 |- ( x = <. B , ran A >. -> ( xCart b <-> <. B , ran A >.Cart b ) )
38	36, 37	ceqsexv 3242	. . . . . . . . . . . 12 |- ( E. x ( x = <. B , ran A >. /\ xCart b ) <-> <. B , ran A >.Cart b )
39	35, 38	bitri 264	. . . . . . . . . . 11 |- ( E. x ( <. A , B >. ( 2nd (x) (Range o. 1st ) ) x /\ xCart b ) <-> <. B , ran A >.Cart b )
40	7, 27, 9	brcart 32039	. . . . . . . . . . 11 |- ( <. B , ran A >.Cart b <-> b = ( B X. ran A ) )
41	10, 39, 40	3bitri 286	. . . . . . . . . 10 |- ( <. A , B >. (Cart o. ( 2nd (x) (Range o. 1st ) ) ) b <-> b = ( B X. ran A ) )
42	8, 41, 23	3anbi123i 1251	. . . . . . . . 9 |- ( ( <. A , B >. 1st a /\ <. A , B >. (Cart o. ( 2nd (x) (Range o. 1st ) ) ) b /\ x = <. a , b >. ) <-> ( a = A /\ b = ( B X. ran A ) /\ x = <. a , b >. ) )
43	5, 42	bitri 264	. . . . . . . 8 |- ( ( x = <. a , b >. /\ <. A , B >. 1st a /\ <. A , B >. (Cart o. ( 2nd (x) (Range o. 1st ) ) ) b ) <-> ( a = A /\ b = ( B X. ran A ) /\ x = <. a , b >. ) )
44	43	2exbii 1775	. . . . . . 7 |- ( E. a E. b ( x = <. a , b >. /\ <. A , B >. 1st a /\ <. A , B >. (Cart o. ( 2nd (x) (Range o. 1st ) ) ) b ) <-> E. a E. b ( a = A /\ b = ( B X. ran A ) /\ x = <. a , b >. ) )
45	7, 27	xpex 6962	. . . . . . . 8 |- ( B X. ran A ) e. _V
46		opeq1 4402	. . . . . . . . 9 |- ( a = A -> <. a , b >. = <. A , b >. )
47	46	eqeq2d 2632	. . . . . . . 8 |- ( a = A -> ( x = <. a , b >. <-> x = <. A , b >. ) )
48		opeq2 4403	. . . . . . . . 9 |- ( b = ( B X. ran A ) -> <. A , b >. = <. A , ( B X. ran A ) >. )
49	48	eqeq2d 2632	. . . . . . . 8 |- ( b = ( B X. ran A ) -> ( x = <. A , b >. <-> x = <. A , ( B X. ran A ) >. ) )
50	6, 45, 47, 49	ceqsex2v 3245	. . . . . . 7 |- ( E. a E. b ( a = A /\ b = ( B X. ran A ) /\ x = <. a , b >. ) <-> x = <. A , ( B X. ran A ) >. )
51	4, 44, 50	3bitri 286	. . . . . 6 |- ( <. A , B >. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) x <-> x = <. A , ( B X. ran A ) >. )
52	51	anbi1i 731	. . . . 5 |- ( ( <. A , B >. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) x /\ xCap C ) <-> ( x = <. A , ( B X. ran A ) >. /\ xCap C ) )
53	52	exbii 1774	. . . 4 |- ( E. x ( <. A , B >. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) x /\ xCap C ) <-> E. x ( x = <. A , ( B X. ran A ) >. /\ xCap C ) )
54	3, 53	bitri 264	. . 3 |- ( <. A , B >. (Cap o. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) ) C <-> E. x ( x = <. A , ( B X. ran A ) >. /\ xCap C ) )
55		opex 4932	. . . 4 |- <. A , ( B X. ran A ) >. e. _V
56		breq1 4656	. . . 4 |- ( x = <. A , ( B X. ran A ) >. -> ( xCap C <-> <. A , ( B X. ran A ) >.Cap C ) )
57	55, 56	ceqsexv 3242	. . 3 |- ( E. x ( x = <. A , ( B X. ran A ) >. /\ xCap C ) <-> <. A , ( B X. ran A ) >.Cap C )
58	6, 45, 2	brcap 32047	. . 3 |- ( <. A , ( B X. ran A ) >.Cap C <-> C = ( A i^i ( B X. ran A ) ) )
59	54, 57, 58	3bitri 286	. 2 |- ( <. A , B >. (Cap o. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) ) C <-> C = ( A i^i ( B X. ran A ) ) )
60		df-restrict 31978	. . 3 |- Restrict = (Cap o. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) )
61	60	breqi 4659	. 2 |- ( <. A , B >.Restrict C <-> <. A , B >. (Cap o. ( 1st (x) (Cart o. ( 2nd (x) (Range o. 1st ) ) ) ) ) C )
62		dfres3 5403	. . 3 |- ( A |` B ) = ( A i^i ( B X. ran A ) )
63	62	eqeq2i 2634	. 2 |- ( C = ( A |` B ) <-> C = ( A i^i ( B X. ran A ) ) )
64	59, 61, 63	3bitr4i 292	1 |- ( <. A , B >.Restrict C <-> C = ( A |` B ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200   i^i cin 3573   <.cop 4183   class class class wbr 4653   X. cxp 5112   ran crn 5115   |` cres 5116   o. ccom 5118   1stc1st 7166   2ndc2nd 7167   (x) ctxp 31937  Cartccart 31948  Rangecrange 31951  Capccap 31954  Restrictcrestrict 31958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-symdif 3844  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-eprel 5029  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fo 5894  df-fv 5896  df-1st 7168  df-2nd 7169  df-txp 31961  df-pprod 31962  df-image 31971  df-cart 31972  df-range 31975  df-cap 31977  df-restrict 31978

This theorem is referenced by:  dfrecs2  32057