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\in \mathrm{V}$$
	brrestrict.2	$$⊢B\in \mathrm{V}$$
	brrestrict.3	$$⊢C\in \mathrm{V}$$
Assertion	brrestrict	$$⊢⟨A,B⟩\mathrm{𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍}C\leftrightarrow C={A\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		brrestrict.1	$$⊢A\in \mathrm{V}$$
2		brrestrict.2	$$⊢B\in \mathrm{V}$$
3		brrestrict.3	$$⊢C\in \mathrm{V}$$
4		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
5	4 3	brco	$$⊢⟨A,B⟩\left(\mathrm{𝖢𝖺𝗉}\circ \left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)\right)C\leftrightarrow \exists x\left(⟨A,B⟩\left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)x\wedge x\mathrm{𝖢𝖺𝗉}C\right)$$
6	4	brtxp2	$$⊢⟨A,B⟩\left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)x\leftrightarrow \exists a\exists b\left(x=⟨a,b⟩\wedge ⟨A,B⟩1^{st}a\wedge ⟨A,B⟩\left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)b\right)$$
7		3anrot	$$⊢\left(x=⟨a,b⟩\wedge ⟨A,B⟩1^{st}a\wedge ⟨A,B⟩\left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)b\right)\leftrightarrow \left(⟨A,B⟩1^{st}a\wedge ⟨A,B⟩\left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)b\wedge x=⟨a,b⟩\right)$$
8	1 2	br1steq	$$⊢⟨A,B⟩1^{st}a\leftrightarrow a=A$$
9		vex	$$⊢b\in \mathrm{V}$$
10	4 9	brco	$$⊢⟨A,B⟩\left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)b\leftrightarrow \exists x\left(⟨A,B⟩\left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)x\wedge x\mathrm{𝖢𝖺𝗋𝗍}b\right)$$
11	4	brtxp2	$$⊢⟨A,B⟩\left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)x\leftrightarrow \exists a\exists b\left(x=⟨a,b⟩\wedge ⟨A,B⟩2^{nd}a\wedge ⟨A,B⟩\left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)b\right)$$
12		3anrot	$$⊢\left(x=⟨a,b⟩\wedge ⟨A,B⟩2^{nd}a\wedge ⟨A,B⟩\left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)b\right)\leftrightarrow \left(⟨A,B⟩2^{nd}a\wedge ⟨A,B⟩\left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)b\wedge x=⟨a,b⟩\right)$$
13	1 2	br2ndeq	$$⊢⟨A,B⟩2^{nd}a\leftrightarrow a=B$$
14	4 9	brco	$$⊢⟨A,B⟩\left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)b\leftrightarrow \exists x\left(⟨A,B⟩1^{st}x\wedge x\mathrm{𝖱𝖺𝗇𝗀𝖾}b\right)$$
15	1 2	br1steq	$$⊢⟨A,B⟩1^{st}x\leftrightarrow x=A$$
16	15	anbi1i	$$⊢\left(⟨A,B⟩1^{st}x\wedge x\mathrm{𝖱𝖺𝗇𝗀𝖾}b\right)\leftrightarrow \left(x=A\wedge x\mathrm{𝖱𝖺𝗇𝗀𝖾}b\right)$$
17	16	exbii	$$⊢\exists x\left(⟨A,B⟩1^{st}x\wedge x\mathrm{𝖱𝖺𝗇𝗀𝖾}b\right)\leftrightarrow \exists x\left(x=A\wedge x\mathrm{𝖱𝖺𝗇𝗀𝖾}b\right)$$
18		breq1	$$⊢x=A\to \left(x\mathrm{𝖱𝖺𝗇𝗀𝖾}b\leftrightarrow A\mathrm{𝖱𝖺𝗇𝗀𝖾}b\right)$$
19	1 18	ceqsexv	$$⊢\exists x\left(x=A\wedge x\mathrm{𝖱𝖺𝗇𝗀𝖾}b\right)\leftrightarrow A\mathrm{𝖱𝖺𝗇𝗀𝖾}b$$
20	17 19	bitri	$$⊢\exists x\left(⟨A,B⟩1^{st}x\wedge x\mathrm{𝖱𝖺𝗇𝗀𝖾}b\right)\leftrightarrow A\mathrm{𝖱𝖺𝗇𝗀𝖾}b$$
21	1 9	brrange	$$⊢A\mathrm{𝖱𝖺𝗇𝗀𝖾}b\leftrightarrow b=\mathrm{ran}A$$
22	14 20 21	3bitri	$$⊢⟨A,B⟩\left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)b\leftrightarrow b=\mathrm{ran}A$$
23		biid	$$⊢x=⟨a,b⟩\leftrightarrow x=⟨a,b⟩$$
24	13 22 23	3anbi123i	$$⊢\left(⟨A,B⟩2^{nd}a\wedge ⟨A,B⟩\left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)b\wedge x=⟨a,b⟩\right)\leftrightarrow \left(a=B\wedge b=\mathrm{ran}A\wedge x=⟨a,b⟩\right)$$
25	12 24	bitri	$$⊢\left(x=⟨a,b⟩\wedge ⟨A,B⟩2^{nd}a\wedge ⟨A,B⟩\left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)b\right)\leftrightarrow \left(a=B\wedge b=\mathrm{ran}A\wedge x=⟨a,b⟩\right)$$
26	25	2exbii	$$⊢\exists a\exists b\left(x=⟨a,b⟩\wedge ⟨A,B⟩2^{nd}a\wedge ⟨A,B⟩\left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)b\right)\leftrightarrow \exists a\exists b\left(a=B\wedge b=\mathrm{ran}A\wedge x=⟨a,b⟩\right)$$
27	1	rnex	$$⊢\mathrm{ran}A\in \mathrm{V}$$
28		opeq1	$$⊢a=B\to ⟨a,b⟩=⟨B,b⟩$$
29	28	eqeq2d	$$⊢a=B\to \left(x=⟨a,b⟩\leftrightarrow x=⟨B,b⟩\right)$$
30		opeq2	$$⊢b=\mathrm{ran}A\to ⟨B,b⟩=⟨B,\mathrm{ran}A⟩$$
31	30	eqeq2d	$$⊢b=\mathrm{ran}A\to \left(x=⟨B,b⟩\leftrightarrow x=⟨B,\mathrm{ran}A⟩\right)$$
32	2 27 29 31	ceqsex2v	$$⊢\exists a\exists b\left(a=B\wedge b=\mathrm{ran}A\wedge x=⟨a,b⟩\right)\leftrightarrow x=⟨B,\mathrm{ran}A⟩$$
33	11 26 32	3bitri	$$⊢⟨A,B⟩\left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)x\leftrightarrow x=⟨B,\mathrm{ran}A⟩$$
34	33	anbi1i	$$⊢\left(⟨A,B⟩\left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)x\wedge x\mathrm{𝖢𝖺𝗋𝗍}b\right)\leftrightarrow \left(x=⟨B,\mathrm{ran}A⟩\wedge x\mathrm{𝖢𝖺𝗋𝗍}b\right)$$
35	34	exbii	$$⊢\exists x\left(⟨A,B⟩\left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)x\wedge x\mathrm{𝖢𝖺𝗋𝗍}b\right)\leftrightarrow \exists x\left(x=⟨B,\mathrm{ran}A⟩\wedge x\mathrm{𝖢𝖺𝗋𝗍}b\right)$$
36		opex	$$⊢⟨B,\mathrm{ran}A⟩\in \mathrm{V}$$
37		breq1	$$⊢x=⟨B,\mathrm{ran}A⟩\to \left(x\mathrm{𝖢𝖺𝗋𝗍}b\leftrightarrow ⟨B,\mathrm{ran}A⟩\mathrm{𝖢𝖺𝗋𝗍}b\right)$$
38	36 37	ceqsexv	$$⊢\exists x\left(x=⟨B,\mathrm{ran}A⟩\wedge x\mathrm{𝖢𝖺𝗋𝗍}b\right)\leftrightarrow ⟨B,\mathrm{ran}A⟩\mathrm{𝖢𝖺𝗋𝗍}b$$
39	35 38	bitri	$$⊢\exists x\left(⟨A,B⟩\left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)x\wedge x\mathrm{𝖢𝖺𝗋𝗍}b\right)\leftrightarrow ⟨B,\mathrm{ran}A⟩\mathrm{𝖢𝖺𝗋𝗍}b$$
40	2 27 9	brcart	$$⊢⟨B,\mathrm{ran}A⟩\mathrm{𝖢𝖺𝗋𝗍}b\leftrightarrow b=B\times \mathrm{ran}A$$
41	10 39 40	3bitri	$$⊢⟨A,B⟩\left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)b\leftrightarrow b=B\times \mathrm{ran}A$$
42	8 41 23	3anbi123i	$$⊢\left(⟨A,B⟩1^{st}a\wedge ⟨A,B⟩\left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)b\wedge x=⟨a,b⟩\right)\leftrightarrow \left(a=A\wedge b=B\times \mathrm{ran}A\wedge x=⟨a,b⟩\right)$$
43	7 42	bitri	$$⊢\left(x=⟨a,b⟩\wedge ⟨A,B⟩1^{st}a\wedge ⟨A,B⟩\left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)b\right)\leftrightarrow \left(a=A\wedge b=B\times \mathrm{ran}A\wedge x=⟨a,b⟩\right)$$
44	43	2exbii	$$⊢\exists a\exists b\left(x=⟨a,b⟩\wedge ⟨A,B⟩1^{st}a\wedge ⟨A,B⟩\left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)b\right)\leftrightarrow \exists a\exists b\left(a=A\wedge b=B\times \mathrm{ran}A\wedge x=⟨a,b⟩\right)$$
45	2 27	xpex	$$⊢B\times \mathrm{ran}A\in \mathrm{V}$$
46		opeq1	$$⊢a=A\to ⟨a,b⟩=⟨A,b⟩$$
47	46	eqeq2d	$$⊢a=A\to \left(x=⟨a,b⟩\leftrightarrow x=⟨A,b⟩\right)$$
48		opeq2	$$⊢b=B\times \mathrm{ran}A\to ⟨A,b⟩=⟨A,B\times \mathrm{ran}A⟩$$
49	48	eqeq2d	$$⊢b=B\times \mathrm{ran}A\to \left(x=⟨A,b⟩\leftrightarrow x=⟨A,B\times \mathrm{ran}A⟩\right)$$
50	1 45 47 49	ceqsex2v	$$⊢\exists a\exists b\left(a=A\wedge b=B\times \mathrm{ran}A\wedge x=⟨a,b⟩\right)\leftrightarrow x=⟨A,B\times \mathrm{ran}A⟩$$
51	6 44 50	3bitri	$$⊢⟨A,B⟩\left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)x\leftrightarrow x=⟨A,B\times \mathrm{ran}A⟩$$
52	51	anbi1i	$$⊢\left(⟨A,B⟩\left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)x\wedge x\mathrm{𝖢𝖺𝗉}C\right)\leftrightarrow \left(x=⟨A,B\times \mathrm{ran}A⟩\wedge x\mathrm{𝖢𝖺𝗉}C\right)$$
53	52	exbii	$$⊢\exists x\left(⟨A,B⟩\left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)x\wedge x\mathrm{𝖢𝖺𝗉}C\right)\leftrightarrow \exists x\left(x=⟨A,B\times \mathrm{ran}A⟩\wedge x\mathrm{𝖢𝖺𝗉}C\right)$$
54	5 53	bitri	$$⊢⟨A,B⟩\left(\mathrm{𝖢𝖺𝗉}\circ \left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)\right)C\leftrightarrow \exists x\left(x=⟨A,B\times \mathrm{ran}A⟩\wedge x\mathrm{𝖢𝖺𝗉}C\right)$$
55		opex	$$⊢⟨A,B\times \mathrm{ran}A⟩\in \mathrm{V}$$
56		breq1	$$⊢x=⟨A,B\times \mathrm{ran}A⟩\to \left(x\mathrm{𝖢𝖺𝗉}C\leftrightarrow ⟨A,B\times \mathrm{ran}A⟩\mathrm{𝖢𝖺𝗉}C\right)$$
57	55 56	ceqsexv	$$⊢\exists x\left(x=⟨A,B\times \mathrm{ran}A⟩\wedge x\mathrm{𝖢𝖺𝗉}C\right)\leftrightarrow ⟨A,B\times \mathrm{ran}A⟩\mathrm{𝖢𝖺𝗉}C$$
58	1 45 3	brcap	$$⊢⟨A,B\times \mathrm{ran}A⟩\mathrm{𝖢𝖺𝗉}C\leftrightarrow C=A\cap \left(B\times \mathrm{ran}A\right)$$
59	54 57 58	3bitri	$$⊢⟨A,B⟩\left(\mathrm{𝖢𝖺𝗉}\circ \left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)\right)C\leftrightarrow C=A\cap \left(B\times \mathrm{ran}A\right)$$
60		df-restrict	$$⊢\mathrm{𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍}=\mathrm{𝖢𝖺𝗉}\circ \left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)$$
61	60	breqi	$$⊢⟨A,B⟩\mathrm{𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍}C\leftrightarrow ⟨A,B⟩\left(\mathrm{𝖢𝖺𝗉}\circ \left(1^{st}\otimes \left(\mathrm{𝖢𝖺𝗋𝗍}\circ \left(2^{nd}\otimes \left(\mathrm{𝖱𝖺𝗇𝗀𝖾}\circ 1^{st}\right)\right)\right)\right)\right)C$$
62		dfres3	$$⊢{A\upharpoonright }_B=A\cap \left(B\times \mathrm{ran}A\right)$$
63	62	eqeq2i	$$⊢C={A\upharpoonright }_B\leftrightarrow C=A\cap \left(B\times \mathrm{ran}A\right)$$
64	59 61 63	3bitr4i	$$⊢⟨A,B⟩\mathrm{𝖱𝖾𝗌𝗍𝗋𝗂𝖼𝗍}C\leftrightarrow C={A\upharpoonright }_B$$