brrestrict

Description: Binary relation form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brrestrict.1	⊢ 𝐴 ∈ V
	brrestrict.2	⊢ 𝐵 ∈ V
	brrestrict.3	⊢ 𝐶 ∈ V
Assertion	brrestrict	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Restrict 𝐶 ↔ 𝐶 = ( 𝐴 ↾ 𝐵 ) )

Proof

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

Metamath Proof Explorer

Theorem brrestrict

Proof