Theorem brrestrict 36419

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 5447	. . . . 5 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
2		brrestrict.3	. . . . 5 ⊢ 𝐶 ∈ V
3	1, 2	brco 5858	. . . 4 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶))
4	1	brtxp2 36349	. . . . . . 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 36241	. . . . . . . . . 10 ⊢ (⟨𝐴, 𝐵⟩1st 𝑎 ↔ 𝑎 = 𝐴)
9		vex 3459	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
10	1, 9	brco 5858	. . . . . . . . . . 11 ⊢ (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏))
11	1	brtxp2 36349	. . . . . . . . . . . . . . 15 ⊢ (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ↔ ∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏))
12		3anrot 1117	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
13	6, 7	br2ndeq 36242	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝐴, 𝐵⟩2nd 𝑎 ↔ 𝑎 = 𝐵)
14	1, 9	brco 5858	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏))
15	6, 7	br1steq 36241	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝐴, 𝐵⟩1st 𝑥 ↔ 𝑥 = 𝐴)
16	15	anbi1i 635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ (𝑥 = 𝐴 ∧ 𝑥Range𝑏))
17	16	exbii 1878	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏))
18		breq1 5113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = 𝐴 → (𝑥Range𝑏 ↔ 𝐴Range𝑏))
19	6, 18	ceqsexv 3503	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
20	17, 19	bitri 278	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏)
21	6, 9	brrange 36402	. . . . . . . . . . . . . . . . . . 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 1879	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
27	6	rnex 7908	. . . . . . . . . . . . . . . 16 ⊢ ran 𝐴 ∈ V
28		opeq1 4839	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝐵 → ⟨𝑎, 𝑏⟩ = ⟨𝐵, 𝑏⟩)
29	28	eqeq2d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝐵 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, 𝑏⟩))
30		opeq2 4840	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = ran 𝐴 → ⟨𝐵, 𝑏⟩ = ⟨𝐵, ran 𝐴⟩)
31	30	eqeq2d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = ran 𝐴 → (𝑥 = ⟨𝐵, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩))
32	7, 27, 29, 31	ceqsex2v 3506	. . . . . . . . . . . . . . 15 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩)
33	11, 26, 32	3bitri 300	. . . . . . . . . . . . . 14 ⊢ (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩)
34	33	anbi1i 635	. . . . . . . . . . . . 13 ⊢ ((⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ (𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
35	34	exbii 1878	. . . . . . . . . . . 12 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
36		opex 5447	. . . . . . . . . . . . 13 ⊢ ⟨𝐵, ran 𝐴⟩ ∈ V
37		breq1 5113	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝐵, ran 𝐴⟩ → (𝑥Cart𝑏 ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏))
38	36, 37	ceqsexv 3503	. . . . . . . . . . . 12 ⊢ (∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
39	35, 38	bitri 278	. . . . . . . . . . 11 ⊢ (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
40	7, 27, 9	brcart 36400	. . . . . . . . . . 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 1879	. . . . . . 7 ⊢ (∃𝑎∃𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
45	7, 27	xpex 7753	. . . . . . . 8 ⊢ (𝐵 × ran 𝐴) ∈ V
46		opeq1 4839	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
47	46	eqeq2d 2774	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, 𝑏⟩))
48		opeq2 4840	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 × ran 𝐴) → ⟨𝐴, 𝑏⟩ = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
49	48	eqeq2d 2774	. . . . . . . 8 ⊢ (𝑏 = (𝐵 × ran 𝐴) → (𝑥 = ⟨𝐴, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩))
50	6, 45, 47, 49	ceqsex2v 3506	. . . . . . 7 ⊢ (∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
51	4, 44, 50	3bitri 300	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
52	51	anbi1i 635	. . . . 5 ⊢ ((⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶) ↔ (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
53	52	exbii 1878	. . . 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 5447	. . . 4 ⊢ ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∈ V
56		breq1 5113	. . . 4 ⊢ (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ → (𝑥Cap𝐶 ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶))
57	55, 56	ceqsexv 3503	. . 3 ⊢ (∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶) ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶)
58	6, 45, 2	brcap 36408	. . 3 ⊢ (⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
59	54, 57, 58	3bitri 300	. 2 ⊢ (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
60		df-restrict 36339	. . 3 ⊢ Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
61	60	breqi 5116	. 2 ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ ⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶)
62		dfres3 5985	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴))
63	62	eqeq2i 2776	. 2 ⊢ (𝐶 = (𝐴 ↾ 𝐵) ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
64	59, 61, 63	3bitr4i 306	1 ⊢ (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455   ∩ cin 3905  ⟨cop 4596   class class class wbr 5110   × cxp 5661  ran crn 5664   ↾ cres 5665   ∘ ccom 5667  1^st c1st 7985  2^nd c2nd 7986   ⊗ ctxp 36298  Cartccart 36309  Rangecrange 36312  Capccap 36315  Restrictcrestrict 36319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-symdif 4207  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-eprel 5563  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fo 6544  df-fv 6546  df-1st 7987  df-2nd 7988  df-txp 36322  df-pprod 36323  df-image 36332  df-cart 36333  df-range 36336  df-cap 36338  df-restrict 36339

This theorem is referenced by:  dfrecs2  36420