Theorem brrestrict 35931

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 5475	. . . . 5 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
2		brrestrict.3	. . . . 5 ⊢ 𝐶 ∈ V
3	1, 2	brco 5884	. . . 4 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶))
4	1	brtxp2 35863	. . . . . . 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 35752	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩1st 𝑎 ↔ 𝑎 = 𝐴)
9		vex 3482	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
10	1, 9	brco 5884	. . . . . . . . . . 11 ⊢ (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏))
11	1	brtxp2 35863	. . . . . . . . . . . . . . 15 ⊢ (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ↔ ∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏))
12		3anrot 1099	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
13	6, 7	br2ndeq 35753	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝐴, 𝐵⟩2nd 𝑎 ↔ 𝑎 = 𝐵)
14	1, 9	brco 5884	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏))
15	6, 7	br1steq 35752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝐴, 𝐵⟩1st 𝑥 ↔ 𝑥 = 𝐴)
16	15	anbi1i 624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ (𝑥 = 𝐴 ∧ 𝑥Range𝑏))
17	16	exbii 1845	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏))
18		breq1 5151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝐴 → (𝑥Range𝑏 ↔ 𝐴Range𝑏))
19	6, 18	ceqsexv 3530	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
20	17, 19	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
21	6, 9	brrange 35916	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴Range𝑏 ↔ 𝑏 = ran 𝐴)
22	14, 20, 21	3bitri 297	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ 𝑏 = ran 𝐴)
23		biid 261	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝑎, 𝑏⟩)
24	13, 22, 23	3anbi123i 1154	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
25	12, 24	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
26	25	2exbii 1846	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
27	6	rnex 7933	. . . . . . . . . . . . . . . 16 ⊢ ran 𝐴 ∈ V
28		opeq1 4878	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝐵 → ⟨𝑎, 𝑏⟩ = ⟨𝐵, 𝑏⟩)
29	28	eqeq2d 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐵 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, 𝑏⟩))
30		opeq2 4879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = ran 𝐴 → ⟨𝐵, 𝑏⟩ = ⟨𝐵, ran 𝐴⟩)
31	30	eqeq2d 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = ran 𝐴 → (𝑥 = ⟨𝐵, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩))
32	7, 27, 29, 31	ceqsex2v 3536	. . . . . . . . . . . . . . 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 1845	. . . . . . . . . . . 12 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
36		opex 5475	. . . . . . . . . . . . 13 ⊢ ⟨𝐵, ran 𝐴⟩ ∈ V
37		breq1 5151	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝐵, ran 𝐴⟩ → (𝑥Cart𝑏 ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏))
38	36, 37	ceqsexv 3530	. . . . . . . . . . . 12 ⊢ (∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
39	35, 38	bitri 275	. . . . . . . . . . 11 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
40	7, 27, 9	brcart 35914	. . . . . . . . . . 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 275	. . . . . . . 8 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ (𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
44	43	2exbii 1846	. . . . . . 7 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
45	7, 27	xpex 7772	. . . . . . . 8 ⊢ (𝐵 × ran 𝐴) ∈ V
46		opeq1 4878	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
47	46	eqeq2d 2746	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, 𝑏⟩))
48		opeq2 4879	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 × ran 𝐴) → ⟨𝐴, 𝑏⟩ = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
49	48	eqeq2d 2746	. . . . . . . 8 ⊢ (𝑏 = (𝐵 × ran 𝐴) → (𝑥 = ⟨𝐴, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩))
50	6, 45, 47, 49	ceqsex2v 3536	. . . . . . 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 1845	. . . 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 5475	. . . 4 ⊢ ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∈ V
56		breq1 5151	. . . 4 ⊢ (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ → (𝑥Cap𝐶 ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶))
57	55, 56	ceqsexv 3530	. . 3 ⊢ (∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶) ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶)
58	6, 45, 2	brcap 35922	. . 3 ⊢ (⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
59	54, 57, 58	3bitri 297	. 2 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
60		df-restrict 35853	. . 3 ⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
61	60	breqi 5154	. 2 ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ ⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶)
62		dfres3 6005	. . 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 1537  ∃wex 1776   ∈ wcel 2106  Vcvv 3478   ∩ cin 3962  ⟨cop 4637   class class class wbr 5148   × cxp 5687  ran crn 5690   ↾ cres 5691   ∘ ccom 5693  1^st c1st 8011  2^nd c2nd 8012   ⊗ ctxp 35812  Cartccart 35823  Rangecrange 35826  Capccap 35829  Restrictcrestrict 35833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-symdif 4259  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-eprel 5589  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fo 6569  df-fv 6571  df-1st 8013  df-2nd 8014  df-txp 35836  df-pprod 35837  df-image 35846  df-cart 35847  df-range 35850  df-cap 35852  df-restrict 35853

This theorem is referenced by:  dfrecs2  35932