Metamath Proof Explorer

Theorem brrestrict

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

Ref Expression
Hypotheses brrestrict.1 
|- A e. _V
brrestrict.2 
|- B e. _V
brrestrict.3 
|- C e. _V
Assertion brrestrict 
|- ( <. A , B >. Restrict C <-> C = ( A |` B ) )

Proof

Step Hyp Ref Expression
1 brrestrict.1 
 |-  A e. _V
2 brrestrict.2 
 |-  B e. _V
3 brrestrict.3 
 |-  C e. _V
4 opex 
 |-  <. A , B >. e. _V
5 4 3 brco 
 |-  ( <. 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 /\ x Cap C ) )
6 4 brtxp2 
 |-  ( <. 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 ) )
7 3anrot 
 |-  ( ( 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 >. ) )
8 1 2 br1steq 
 |-  ( <. A , B >. 1st a <-> a = A )
9 vex 
 |-  b e. _V
10 4 9 brco 
 |-  ( <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b <-> E. x ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x /\ x Cart b ) )
11 4 brtxp2 
 |-  ( <. 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 
 |-  ( ( 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 1 2 br2ndeq 
 |-  ( <. A , B >. 2nd a <-> a = B )
14 4 9 brco 
 |-  ( <. A , B >. ( Range o. 1st ) b <-> E. x ( <. A , B >. 1st x /\ x Range b ) )
15 1 2 br1steq 
 |-  ( <. A , B >. 1st x <-> x = A )
16 15 anbi1i 
 |-  ( ( <. A , B >. 1st x /\ x Range b ) <-> ( x = A /\ x Range b ) )
17 16 exbii 
 |-  ( E. x ( <. A , B >. 1st x /\ x Range b ) <-> E. x ( x = A /\ x Range b ) )
18 breq1 
 |-  ( x = A -> ( x Range b <-> A Range b ) )
19 1 18 ceqsexv 
 |-  ( E. x ( x = A /\ x Range b ) <-> A Range b )
20 17 19 bitri 
 |-  ( E. x ( <. A , B >. 1st x /\ x Range b ) <-> A Range b )
21 1 9 brrange 
 |-  ( A Range b <-> b = ran A )
22 14 20 21 3bitri 
 |-  ( <. A , B >. ( Range o. 1st ) b <-> b = ran A )
23 biid 
 |-  ( x = <. a , b >. <-> x = <. a , b >. )
24 13 22 23 3anbi123i 
 |-  ( ( <. 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 
 |-  ( ( x = <. a , b >. /\ <. A , B >. 2nd a /\ <. A , B >. ( Range o. 1st ) b ) <-> ( a = B /\ b = ran A /\ x = <. a , b >. ) )
26 25 2exbii 
 |-  ( 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 1 rnex 
 |-  ran A e. _V
28 opeq1 
 |-  ( a = B -> <. a , b >. = <. B , b >. )
29 28 eqeq2d 
 |-  ( a = B -> ( x = <. a , b >. <-> x = <. B , b >. ) )
30 opeq2 
 |-  ( b = ran A -> <. B , b >. = <. B , ran A >. )
31 30 eqeq2d 
 |-  ( b = ran A -> ( x = <. B , b >. <-> x = <. B , ran A >. ) )
32 2 27 29 31 ceqsex2v 
 |-  ( E. a E. b ( a = B /\ b = ran A /\ x = <. a , b >. ) <-> x = <. B , ran A >. )
33 11 26 32 3bitri 
 |-  ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x <-> x = <. B , ran A >. )
34 33 anbi1i 
 |-  ( ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x /\ x Cart b ) <-> ( x = <. B , ran A >. /\ x Cart b ) )
35 34 exbii 
 |-  ( E. x ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x /\ x Cart b ) <-> E. x ( x = <. B , ran A >. /\ x Cart b ) )
36 opex 
 |-  <. B , ran A >. e. _V
37 breq1 
 |-  ( x = <. B , ran A >. -> ( x Cart b <-> <. B , ran A >. Cart b ) )
38 36 37 ceqsexv 
 |-  ( E. x ( x = <. B , ran A >. /\ x Cart b ) <-> <. B , ran A >. Cart b )
39 35 38 bitri 
 |-  ( E. x ( <. A , B >. ( 2nd (x) ( Range o. 1st ) ) x /\ x Cart b ) <-> <. B , ran A >. Cart b )
40 2 27 9 brcart 
 |-  ( <. B , ran A >. Cart b <-> b = ( B X. ran A ) )
41 10 39 40 3bitri 
 |-  ( <. A , B >. ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) b <-> b = ( B X. ran A ) )
42 8 41 23 3anbi123i 
 |-  ( ( <. 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 7 42 bitri 
 |-  ( ( 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 
 |-  ( 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 2 27 xpex 
 |-  ( B X. ran A ) e. _V
46 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
47 46 eqeq2d 
 |-  ( a = A -> ( x = <. a , b >. <-> x = <. A , b >. ) )
48 opeq2 
 |-  ( b = ( B X. ran A ) -> <. A , b >. = <. A , ( B X. ran A ) >. )
49 48 eqeq2d 
 |-  ( b = ( B X. ran A ) -> ( x = <. A , b >. <-> x = <. A , ( B X. ran A ) >. ) )
50 1 45 47 49 ceqsex2v 
 |-  ( E. a E. b ( a = A /\ b = ( B X. ran A ) /\ x = <. a , b >. ) <-> x = <. A , ( B X. ran A ) >. )
51 6 44 50 3bitri 
 |-  ( <. A , B >. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) x <-> x = <. A , ( B X. ran A ) >. )
52 51 anbi1i 
 |-  ( ( <. A , B >. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) x /\ x Cap C ) <-> ( x = <. A , ( B X. ran A ) >. /\ x Cap C ) )
53 52 exbii 
 |-  ( E. x ( <. A , B >. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) x /\ x Cap C ) <-> E. x ( x = <. A , ( B X. ran A ) >. /\ x Cap C ) )
54 5 53 bitri 
 |-  ( <. A , B >. ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) ) C <-> E. x ( x = <. A , ( B X. ran A ) >. /\ x Cap C ) )
55 opex 
 |-  <. A , ( B X. ran A ) >. e. _V
56 breq1 
 |-  ( x = <. A , ( B X. ran A ) >. -> ( x Cap C <-> <. A , ( B X. ran A ) >. Cap C ) )
57 55 56 ceqsexv 
 |-  ( E. x ( x = <. A , ( B X. ran A ) >. /\ x Cap C ) <-> <. A , ( B X. ran A ) >. Cap C )
58 1 45 3 brcap 
 |-  ( <. A , ( B X. ran A ) >. Cap C <-> C = ( A i^i ( B X. ran A ) ) )
59 54 57 58 3bitri 
 |-  ( <. 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 
 |-  Restrict = ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) )
61 60 breqi 
 |-  ( <. A , B >. Restrict C <-> <. A , B >. ( Cap o. ( 1st (x) ( Cart o. ( 2nd (x) ( Range o. 1st ) ) ) ) ) C )
62 dfres3 
 |-  ( A |` B ) = ( A i^i ( B X. ran A ) )
63 62 eqeq2i 
 |-  ( C = ( A |` B ) <-> C = ( A i^i ( B X. ran A ) ) )
64 59 61 63 3bitr4i 
 |-  ( <. A , B >. Restrict C <-> C = ( A |` B ) )