Theorem brrestrict 35967

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 5439	. . . . 5 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
2		brrestrict.3	. . . . 5 ⊢ 𝐶 ∈ V
3	1, 2	brco 5850	. . . 4 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶))
4	1	brtxp2 35899	. . . . . . 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 35788	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩1st 𝑎 ↔ 𝑎 = 𝐴)
9		vex 3463	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
10	1, 9	brco 5850	. . . . . . . . . . 11 ⊢ (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏))
11	1	brtxp2 35899	. . . . . . . . . . . . . . 15 ⊢ (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ↔ ∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏))
12		3anrot 1099	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
13	6, 7	br2ndeq 35789	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝐴, 𝐵⟩2nd 𝑎 ↔ 𝑎 = 𝐵)
14	1, 9	brco 5850	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏))
15	6, 7	br1steq 35788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝐴, 𝐵⟩1st 𝑥 ↔ 𝑥 = 𝐴)
16	15	anbi1i 624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ (𝑥 = 𝐴 ∧ 𝑥Range𝑏))
17	16	exbii 1848	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏))
18		breq1 5122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝐴 → (𝑥Range𝑏 ↔ 𝐴Range𝑏))
19	6, 18	ceqsexv 3511	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
20	17, 19	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
21	6, 9	brrange 35952	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴Range𝑏 ↔ 𝑏 = ran 𝐴)
22	14, 20, 21	3bitri 297	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ 𝑏 = ran 𝐴)
23		biid 261	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝑎, 𝑏⟩)
24	13, 22, 23	3anbi123i 1155	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
25	12, 24	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
26	25	2exbii 1849	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
27	6	rnex 7906	. . . . . . . . . . . . . . . 16 ⊢ ran 𝐴 ∈ V
28		opeq1 4849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝐵 → ⟨𝑎, 𝑏⟩ = ⟨𝐵, 𝑏⟩)
29	28	eqeq2d 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐵 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, 𝑏⟩))
30		opeq2 4850	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = ran 𝐴 → ⟨𝐵, 𝑏⟩ = ⟨𝐵, ran 𝐴⟩)
31	30	eqeq2d 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = ran 𝐴 → (𝑥 = ⟨𝐵, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩))
32	7, 27, 29, 31	ceqsex2v 3515	. . . . . . . . . . . . . . 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 1848	. . . . . . . . . . . 12 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
36		opex 5439	. . . . . . . . . . . . 13 ⊢ ⟨𝐵, ran 𝐴⟩ ∈ V
37		breq1 5122	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝐵, ran 𝐴⟩ → (𝑥Cart𝑏 ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏))
38	36, 37	ceqsexv 3511	. . . . . . . . . . . 12 ⊢ (∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
39	35, 38	bitri 275	. . . . . . . . . . 11 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
40	7, 27, 9	brcart 35950	. . . . . . . . . . 11 ⊢ (⟨𝐵, ran 𝐴⟩Cart𝑏 ↔ 𝑏 = (𝐵 × ran 𝐴))
41	10, 39, 40	3bitri 297	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ↔ 𝑏 = (𝐵 × ran 𝐴))
42	8, 41, 23	3anbi123i 1155	. . . . . . . . 9 ⊢ ((⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
43	5, 42	bitri 275	. . . . . . . 8 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ (𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
44	43	2exbii 1849	. . . . . . 7 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
45	7, 27	xpex 7747	. . . . . . . 8 ⊢ (𝐵 × ran 𝐴) ∈ V
46		opeq1 4849	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
47	46	eqeq2d 2746	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, 𝑏⟩))
48		opeq2 4850	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 × ran 𝐴) → ⟨𝐴, 𝑏⟩ = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
49	48	eqeq2d 2746	. . . . . . . 8 ⊢ (𝑏 = (𝐵 × ran 𝐴) → (𝑥 = ⟨𝐴, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩))
50	6, 45, 47, 49	ceqsex2v 3515	. . . . . . 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 1848	. . . 4 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶) ↔ ∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
54	3, 53	bitri 275	. . 3 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
55		opex 5439	. . . 4 ⊢ ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∈ V
56		breq1 5122	. . . 4 ⊢ (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ → (𝑥Cap𝐶 ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶))
57	55, 56	ceqsexv 3511	. . 3 ⊢ (∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶) ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶)
58	6, 45, 2	brcap 35958	. . 3 ⊢ (⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
59	54, 57, 58	3bitri 297	. 2 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
60		df-restrict 35889	. . 3 ⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
61	60	breqi 5125	. 2 ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ ⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶)
62		dfres3 5971	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴))
63	62	eqeq2i 2748	. 2 ⊢ (𝐶 = (𝐴 ↾ 𝐵) ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
64	59, 61, 63	3bitr4i 303	1 ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459   ∩ cin 3925  ⟨cop 4607   class class class wbr 5119   × cxp 5652  ran crn 5655   ↾ cres 5656   ∘ ccom 5658  1^st c1st 7986  2^nd c2nd 7987   ⊗ ctxp 35848  Cartccart 35859  Rangecrange 35862  Capccap 35865  Restrictcrestrict 35869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-symdif 4228  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-eprel 5553  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fo 6537  df-fv 6539  df-1st 7988  df-2nd 7989  df-txp 35872  df-pprod 35873  df-image 35882  df-cart 35883  df-range 35886  df-cap 35888  df-restrict 35889

This theorem is referenced by:  dfrecs2  35968