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 V
brrestrict.2 B V
brrestrict.3 C V
Assertion brrestrict A B 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 C C = A B

Proof

Step Hyp Ref Expression
1 brrestrict.1 A V
2 brrestrict.2 B V
3 brrestrict.3 C V
4 opex A B V
5 4 3 brco A B 𝖢𝖺𝗉 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st C x A B 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x x 𝖢𝖺𝗉 C
6 4 brtxp2 A B 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x a b x = a b A B 1 st a A B 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st b
7 3anrot x = a b A B 1 st a A B 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st b A B 1 st a A B 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st b x = a b
8 1 2 br1steq A B 1 st a a = A
9 vex b V
10 4 9 brco A B 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st b x A B 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x x 𝖢𝖺𝗋𝗍 b
11 4 brtxp2 A B 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x a b x = a b A B 2 nd a A B 𝖱𝖺𝗇𝗀𝖾 1 st b
12 3anrot x = a b A B 2 nd a A B 𝖱𝖺𝗇𝗀𝖾 1 st b A B 2 nd a A B 𝖱𝖺𝗇𝗀𝖾 1 st b x = a b
13 1 2 br2ndeq A B 2 nd a a = B
14 4 9 brco A B 𝖱𝖺𝗇𝗀𝖾 1 st b x A B 1 st x x 𝖱𝖺𝗇𝗀𝖾 b
15 1 2 br1steq A B 1 st x x = A
16 15 anbi1i A B 1 st x x 𝖱𝖺𝗇𝗀𝖾 b x = A x 𝖱𝖺𝗇𝗀𝖾 b
17 16 exbii x A B 1 st x x 𝖱𝖺𝗇𝗀𝖾 b x x = A x 𝖱𝖺𝗇𝗀𝖾 b
18 breq1 x = A x 𝖱𝖺𝗇𝗀𝖾 b A 𝖱𝖺𝗇𝗀𝖾 b
19 1 18 ceqsexv x x = A x 𝖱𝖺𝗇𝗀𝖾 b A 𝖱𝖺𝗇𝗀𝖾 b
20 17 19 bitri x A B 1 st x x 𝖱𝖺𝗇𝗀𝖾 b A 𝖱𝖺𝗇𝗀𝖾 b
21 1 9 brrange A 𝖱𝖺𝗇𝗀𝖾 b b = ran A
22 14 20 21 3bitri A B 𝖱𝖺𝗇𝗀𝖾 1 st b b = ran A
23 biid x = a b x = a b
24 13 22 23 3anbi123i A B 2 nd a A B 𝖱𝖺𝗇𝗀𝖾 1 st b x = a b a = B b = ran A x = a b
25 12 24 bitri x = a b A B 2 nd a A B 𝖱𝖺𝗇𝗀𝖾 1 st b a = B b = ran A x = a b
26 25 2exbii a b x = a b A B 2 nd a A B 𝖱𝖺𝗇𝗀𝖾 1 st b a b a = B b = ran A x = a b
27 1 rnex ran A 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 a b a = B b = ran A x = a b x = B ran A
33 11 26 32 3bitri A B 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x x = B ran A
34 33 anbi1i A B 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x x 𝖢𝖺𝗋𝗍 b x = B ran A x 𝖢𝖺𝗋𝗍 b
35 34 exbii x A B 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x x 𝖢𝖺𝗋𝗍 b x x = B ran A x 𝖢𝖺𝗋𝗍 b
36 opex B ran A V
37 breq1 x = B ran A x 𝖢𝖺𝗋𝗍 b B ran A 𝖢𝖺𝗋𝗍 b
38 36 37 ceqsexv x x = B ran A x 𝖢𝖺𝗋𝗍 b B ran A 𝖢𝖺𝗋𝗍 b
39 35 38 bitri x A B 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x x 𝖢𝖺𝗋𝗍 b B ran A 𝖢𝖺𝗋𝗍 b
40 2 27 9 brcart B ran A 𝖢𝖺𝗋𝗍 b b = B × ran A
41 10 39 40 3bitri A B 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st b b = B × ran A
42 8 41 23 3anbi123i A B 1 st a A B 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st b x = a b a = A b = B × ran A x = a b
43 7 42 bitri x = a b A B 1 st a A B 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st b a = A b = B × ran A x = a b
44 43 2exbii a b x = a b A B 1 st a A B 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st b a b a = A b = B × ran A x = a b
45 2 27 xpex B × ran A V
46 opeq1 a = A a b = A b
47 46 eqeq2d a = A x = a b x = A b
48 opeq2 b = B × ran A A b = A B × ran A
49 48 eqeq2d b = B × ran A x = A b x = A B × ran A
50 1 45 47 49 ceqsex2v a b a = A b = B × ran A x = a b x = A B × ran A
51 6 44 50 3bitri A B 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x x = A B × ran A
52 51 anbi1i A B 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x x 𝖢𝖺𝗉 C x = A B × ran A x 𝖢𝖺𝗉 C
53 52 exbii x A B 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st x x 𝖢𝖺𝗉 C x x = A B × ran A x 𝖢𝖺𝗉 C
54 5 53 bitri A B 𝖢𝖺𝗉 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st C x x = A B × ran A x 𝖢𝖺𝗉 C
55 opex A B × ran A V
56 breq1 x = A B × ran A x 𝖢𝖺𝗉 C A B × ran A 𝖢𝖺𝗉 C
57 55 56 ceqsexv x x = A B × ran A x 𝖢𝖺𝗉 C A B × ran A 𝖢𝖺𝗉 C
58 1 45 3 brcap A B × ran A 𝖢𝖺𝗉 C C = A B × ran A
59 54 57 58 3bitri A B 𝖢𝖺𝗉 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st C C = A B × ran A
60 df-restrict 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 = 𝖢𝖺𝗉 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st
61 60 breqi A B 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 C A B 𝖢𝖺𝗉 1 st 𝖢𝖺𝗋𝗍 2 nd 𝖱𝖺𝗇𝗀𝖾 1 st C
62 dfres3 A B = A B × ran A
63 62 eqeq2i C = A B C = A B × ran A
64 59 61 63 3bitr4i A B 𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍 C C = A B