Theorem brrestrict 34251

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	⊢ 𝐴 ∈ V
brrestrict.2	⊢ 𝐵 ∈ V
brrestrict.3	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
brrestrict	⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵))

Proof of Theorem brrestrict

Dummy variables 𝑎 𝑏 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opex 5379	. . . . 5 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
2		brrestrict.3	. . . . 5 ⊢ 𝐶 ∈ V
3	1, 2	brco 5779	. . . 4 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶))
4	1	brtxp2 34183	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ↔ ∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏))
5		3anrot 1099	. . . . . . . . 9 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ (⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
6		brrestrict.1	. . . . . . . . . . 11 ⊢ 𝐴 ∈ V
7		brrestrict.2	. . . . . . . . . . 11 ⊢ 𝐵 ∈ V
8	6, 7	br1steq 33745	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩1st 𝑎 ↔ 𝑎 = 𝐴)
9		vex 3436	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
10	1, 9	brco 5779	. . . . . . . . . . 11 ⊢ (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏))
11	1	brtxp2 34183	. . . . . . . . . . . . . . 15 ⊢ (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ↔ ∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏))
12		3anrot 1099	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
13	6, 7	br2ndeq 33746	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝐴, 𝐵⟩2nd 𝑎 ↔ 𝑎 = 𝐵)
14	1, 9	brco 5779	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏))
15	6, 7	br1steq 33745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝐴, 𝐵⟩1st 𝑥 ↔ 𝑥 = 𝐴)
16	15	anbi1i 624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ (𝑥 = 𝐴 ∧ 𝑥Range𝑏))
17	16	exbii 1850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏))
18		breq1 5077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝐴 → (𝑥Range𝑏 ↔ 𝐴Range𝑏))
19	6, 18	ceqsexv 3479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
20	17, 19	bitri 274	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
21	6, 9	brrange 34236	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴Range𝑏 ↔ 𝑏 = ran 𝐴)
22	14, 20, 21	3bitri 297	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ 𝑏 = ran 𝐴)
23		biid 260	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝑎, 𝑏⟩)
24	13, 22, 23	3anbi123i 1154	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
25	12, 24	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
26	25	2exbii 1851	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
27	6	rnex 7759	. . . . . . . . . . . . . . . 16 ⊢ ran 𝐴 ∈ V
28		opeq1 4804	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝐵 → ⟨𝑎, 𝑏⟩ = ⟨𝐵, 𝑏⟩)
29	28	eqeq2d 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐵 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, 𝑏⟩))
30		opeq2 4805	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = ran 𝐴 → ⟨𝐵, 𝑏⟩ = ⟨𝐵, ran 𝐴⟩)
31	30	eqeq2d 2749	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = ran 𝐴 → (𝑥 = ⟨𝐵, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩))
32	7, 27, 29, 31	ceqsex2v 3483	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩)
33	11, 26, 32	3bitri 297	. . . . . . . . . . . . . 14 ⊢ (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩)
34	33	anbi1i 624	. . . . . . . . . . . . 13 ⊢ ((⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ (𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
35	34	exbii 1850	. . . . . . . . . . . 12 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
36		opex 5379	. . . . . . . . . . . . 13 ⊢ ⟨𝐵, ran 𝐴⟩ ∈ V
37		breq1 5077	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝐵, ran 𝐴⟩ → (𝑥Cart𝑏 ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏))
38	36, 37	ceqsexv 3479	. . . . . . . . . . . 12 ⊢ (∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
39	35, 38	bitri 274	. . . . . . . . . . 11 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
40	7, 27, 9	brcart 34234	. . . . . . . . . . 11 ⊢ (⟨𝐵, ran 𝐴⟩Cart𝑏 ↔ 𝑏 = (𝐵 × ran 𝐴))
41	10, 39, 40	3bitri 297	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ↔ 𝑏 = (𝐵 × ran 𝐴))
42	8, 41, 23	3anbi123i 1154	. . . . . . . . 9 ⊢ ((⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
43	5, 42	bitri 274	. . . . . . . 8 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ (𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
44	43	2exbii 1851	. . . . . . 7 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
45	7, 27	xpex 7603	. . . . . . . 8 ⊢ (𝐵 × ran 𝐴) ∈ V
46		opeq1 4804	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
47	46	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, 𝑏⟩))
48		opeq2 4805	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 × ran 𝐴) → ⟨𝐴, 𝑏⟩ = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
49	48	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑏 = (𝐵 × ran 𝐴) → (𝑥 = ⟨𝐴, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩))
50	6, 45, 47, 49	ceqsex2v 3483	. . . . . . 7 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
51	4, 44, 50	3bitri 297	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
52	51	anbi1i 624	. . . . 5 ⊢ ((⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶) ↔ (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
53	52	exbii 1850	. . . 4 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶) ↔ ∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
54	3, 53	bitri 274	. . 3 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
55		opex 5379	. . . 4 ⊢ ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∈ V
56		breq1 5077	. . . 4 ⊢ (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ → (𝑥Cap𝐶 ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶))
57	55, 56	ceqsexv 3479	. . 3 ⊢ (∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶) ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶)
58	6, 45, 2	brcap 34242	. . 3 ⊢ (⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
59	54, 57, 58	3bitri 297	. 2 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
60		df-restrict 34173	. . 3 ⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
61	60	breqi 5080	. 2 ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ ⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶)
62		dfres3 5896	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴))
63	62	eqeq2i 2751	. 2 ⊢ (𝐶 = (𝐴 ↾ 𝐵) ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
64	59, 61, 63	3bitr4i 303	1 ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539  ∃wex 1782   ∈ wcel 2106  Vcvv 3432   ∩ cin 3886  ⟨cop 4567   class class class wbr 5074   × cxp 5587  ran crn 5590   ↾ cres 5591   ∘ ccom 5593  1^st c1st 7829  2^nd c2nd 7830   ⊗ ctxp 34132  Cartccart 34143  Rangecrange 34146  Capccap 34149  Restrictcrestrict 34153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-symdif 4176  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-eprel 5495  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fo 6439  df-fv 6441  df-1st 7831  df-2nd 7832  df-txp 34156  df-pprod 34157  df-image 34166  df-cart 34167  df-range 34170  df-cap 34172  df-restrict 34173

This theorem is referenced by:  dfrecs2  34252