Theorem brrestrict 36462

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 5450	. . . . 5 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
2		brrestrict.3	. . . . 5 ⊢ 𝐶 ∈ V
3	1, 2	brco 5861	. . . 4 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶))
4	1	brtxp2 36392	. . . . . . 7 ⊢ (⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ↔ ∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏))
5		3anrot 1117	. . . . . . . . 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 36284	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩1st 𝑎 ↔ 𝑎 = 𝐴)
9		vex 3462	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
10	1, 9	brco 5861	. . . . . . . . . . 11 ⊢ (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏))
11	1	brtxp2 36392	. . . . . . . . . . . . . . 15 ⊢ (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ↔ ∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏))
12		3anrot 1117	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
13	6, 7	br2ndeq 36285	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝐴, 𝐵⟩2nd 𝑎 ↔ 𝑎 = 𝐵)
14	1, 9	brco 5861	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏))
15	6, 7	br1steq 36284	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝐴, 𝐵⟩1st 𝑥 ↔ 𝑥 = 𝐴)
16	15	anbi1i 636	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ (𝑥 = 𝐴 ∧ 𝑥Range𝑏))
17	16	exbii 1881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏))
18		breq1 5117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝐴 → (𝑥Range𝑏 ↔ 𝐴Range𝑏))
19	6, 18	ceqsexv 3506	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
20	17, 19	bitri 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
21	6, 9	brrange 36445	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴Range𝑏 ↔ 𝑏 = ran 𝐴)
22	14, 20, 21	3bitri 300	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ 𝑏 = ran 𝐴)
23		biid 264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝑎, 𝑏⟩)
24	13, 22, 23	3anbi123i 1173	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
25	12, 24	bitri 278	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
26	25	2exbii 1882	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
27	6	rnex 7916	. . . . . . . . . . . . . . . 16 ⊢ ran 𝐴 ∈ V
28		opeq1 4843	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝐵 → ⟨𝑎, 𝑏⟩ = ⟨𝐵, 𝑏⟩)
29	28	eqeq2d 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐵 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, 𝑏⟩))
30		opeq2 4844	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = ran 𝐴 → ⟨𝐵, 𝑏⟩ = ⟨𝐵, ran 𝐴⟩)
31	30	eqeq2d 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = ran 𝐴 → (𝑥 = ⟨𝐵, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩))
32	7, 27, 29, 31	ceqsex2v 3509	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩)
33	11, 26, 32	3bitri 300	. . . . . . . . . . . . . 14 ⊢ (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩)
34	33	anbi1i 636	. . . . . . . . . . . . 13 ⊢ ((⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ (𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
35	34	exbii 1881	. . . . . . . . . . . 12 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
36		opex 5450	. . . . . . . . . . . . 13 ⊢ ⟨𝐵, ran 𝐴⟩ ∈ V
37		breq1 5117	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝐵, ran 𝐴⟩ → (𝑥Cart𝑏 ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏))
38	36, 37	ceqsexv 3506	. . . . . . . . . . . 12 ⊢ (∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
39	35, 38	bitri 278	. . . . . . . . . . 11 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
40	7, 27, 9	brcart 36443	. . . . . . . . . . 11 ⊢ (⟨𝐵, ran 𝐴⟩Cart𝑏 ↔ 𝑏 = (𝐵 × ran 𝐴))
41	10, 39, 40	3bitri 300	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ↔ 𝑏 = (𝐵 × ran 𝐴))
42	8, 41, 23	3anbi123i 1173	. . . . . . . . 9 ⊢ ((⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
43	5, 42	bitri 278	. . . . . . . 8 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ (𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
44	43	2exbii 1882	. . . . . . 7 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
45	7, 27	xpex 7761	. . . . . . . 8 ⊢ (𝐵 × ran 𝐴) ∈ V
46		opeq1 4843	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
47	46	eqeq2d 2777	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, 𝑏⟩))
48		opeq2 4844	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 × ran 𝐴) → ⟨𝐴, 𝑏⟩ = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
49	48	eqeq2d 2777	. . . . . . . 8 ⊢ (𝑏 = (𝐵 × ran 𝐴) → (𝑥 = ⟨𝐴, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩))
50	6, 45, 47, 49	ceqsex2v 3509	. . . . . . 7 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
51	4, 44, 50	3bitri 300	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
52	51	anbi1i 636	. . . . 5 ⊢ ((⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶) ↔ (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
53	52	exbii 1881	. . . 4 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶) ↔ ∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
54	3, 53	bitri 278	. . 3 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
55		opex 5450	. . . 4 ⊢ ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∈ V
56		breq1 5117	. . . 4 ⊢ (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ → (𝑥Cap𝐶 ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶))
57	55, 56	ceqsexv 3506	. . 3 ⊢ (∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶) ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶)
58	6, 45, 2	brcap 36451	. . 3 ⊢ (⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
59	54, 57, 58	3bitri 300	. 2 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
60		df-restrict 36382	. . 3 ⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
61	60	breqi 5120	. 2 ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ ⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶)
62		dfres3 5988	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴))
63	62	eqeq2i 2779	. 2 ⊢ (𝐶 = (𝐴 ↾ 𝐵) ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
64	59, 61, 63	3bitr4i 306	1 ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3458   ∩ cin 3907  ⟨cop 4600   class class class wbr 5114   × cxp 5664  ran crn 5667   ↾ cres 5668   ∘ ccom 5670  1^st c1st 7993  2^nd c2nd 7994   ⊗ ctxp 36341  Cartccart 36352  Rangecrange 36355  Capccap 36358  Restrictcrestrict 36362

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-symdif 4209  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-eprel 5566  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fo 6549  df-fv 6551  df-1st 7995  df-2nd 7996  df-txp 36365  df-pprod 36366  df-image 36375  df-cart 36376  df-range 36379  df-cap 36381  df-restrict 36382

This theorem is used by:  dfrecs2  36463