Metamath Proof Explorer


Theorem 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 ∘ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) ) 𝐶 ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) 𝑥𝑥 Cap 𝐶 ) )
6 4 brtxp2 ( ⟨ 𝐴 , 𝐵 ⟩ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) 𝑥 ↔ ∃ 𝑎𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) 𝑏 ) )
7 3anrot ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) 𝑏 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) 𝑏𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) )
8 1 2 br1steq ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑎𝑎 = 𝐴 )
9 vex 𝑏 ∈ V
10 4 9 brco ( ⟨ 𝐴 , 𝐵 ⟩ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) 𝑏 ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ ( 2nd ⊗ ( Range ∘ 1st ) ) 𝑥𝑥 Cart 𝑏 ) )
11 4 brtxp2 ( ⟨ 𝐴 , 𝐵 ⟩ ( 2nd ⊗ ( Range ∘ 1st ) ) 𝑥 ↔ ∃ 𝑎𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ 2nd 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Range ∘ 1st ) 𝑏 ) )
12 3anrot ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ 2nd 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Range ∘ 1st ) 𝑏 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ 2nd 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Range ∘ 1st ) 𝑏𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) )
13 1 2 br2ndeq ( ⟨ 𝐴 , 𝐵 ⟩ 2nd 𝑎𝑎 = 𝐵 )
14 4 9 brco ( ⟨ 𝐴 , 𝐵 ⟩ ( Range ∘ 1st ) 𝑏 ↔ ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑥𝑥 Range 𝑏 ) )
15 1 2 br1steq ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑥𝑥 = 𝐴 )
16 15 anbi1i ( ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑥𝑥 Range 𝑏 ) ↔ ( 𝑥 = 𝐴𝑥 Range 𝑏 ) )
17 16 exbii ( ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑥𝑥 Range 𝑏 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴𝑥 Range 𝑏 ) )
18 breq1 ( 𝑥 = 𝐴 → ( 𝑥 Range 𝑏𝐴 Range 𝑏 ) )
19 1 18 ceqsexv ( ∃ 𝑥 ( 𝑥 = 𝐴𝑥 Range 𝑏 ) ↔ 𝐴 Range 𝑏 )
20 17 19 bitri ( ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑥𝑥 Range 𝑏 ) ↔ 𝐴 Range 𝑏 )
21 1 9 brrange ( 𝐴 Range 𝑏𝑏 = ran 𝐴 )
22 14 20 21 3bitri ( ⟨ 𝐴 , 𝐵 ⟩ ( Range ∘ 1st ) 𝑏𝑏 = ran 𝐴 )
23 biid ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ )
24 13 22 23 3anbi123i ( ( ⟨ 𝐴 , 𝐵 ⟩ 2nd 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Range ∘ 1st ) 𝑏𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( 𝑎 = 𝐵𝑏 = ran 𝐴𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) )
25 12 24 bitri ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ 2nd 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Range ∘ 1st ) 𝑏 ) ↔ ( 𝑎 = 𝐵𝑏 = ran 𝐴𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) )
26 25 2exbii ( ∃ 𝑎𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ 2nd 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Range ∘ 1st ) 𝑏 ) ↔ ∃ 𝑎𝑏 ( 𝑎 = 𝐵𝑏 = 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 ( ⟨ 𝐴 , 𝐵 ⟩ ( 2nd ⊗ ( Range ∘ 1st ) ) 𝑥𝑥 = ⟨ 𝐵 , ran 𝐴 ⟩ )
34 33 anbi1i ( ( ⟨ 𝐴 , 𝐵 ⟩ ( 2nd ⊗ ( Range ∘ 1st ) ) 𝑥𝑥 Cart 𝑏 ) ↔ ( 𝑥 = ⟨ 𝐵 , ran 𝐴 ⟩ ∧ 𝑥 Cart 𝑏 ) )
35 34 exbii ( ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ ( 2nd ⊗ ( Range ∘ 1st ) ) 𝑥𝑥 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 ( ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ ( 2nd ⊗ ( Range ∘ 1st ) ) 𝑥𝑥 Cart 𝑏 ) ↔ ⟨ 𝐵 , ran 𝐴 ⟩ Cart 𝑏 )
40 2 27 9 brcart ( ⟨ 𝐵 , ran 𝐴 ⟩ Cart 𝑏𝑏 = ( 𝐵 × ran 𝐴 ) )
41 10 39 40 3bitri ( ⟨ 𝐴 , 𝐵 ⟩ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) 𝑏𝑏 = ( 𝐵 × ran 𝐴 ) )
42 8 41 23 3anbi123i ( ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) 𝑏𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( 𝑎 = 𝐴𝑏 = ( 𝐵 × ran 𝐴 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) )
43 7 42 bitri ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) 𝑏 ) ↔ ( 𝑎 = 𝐴𝑏 = ( 𝐵 × ran 𝐴 ) ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) )
44 43 2exbii ( ∃ 𝑎𝑏 ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑎 ∧ ⟨ 𝐴 , 𝐵 ⟩ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) 𝑏 ) ↔ ∃ 𝑎𝑏 ( 𝑎 = 𝐴𝑏 = ( 𝐵 × 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 ( ⟨ 𝐴 , 𝐵 ⟩ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) 𝑥𝑥 = ⟨ 𝐴 , ( 𝐵 × ran 𝐴 ) ⟩ )
52 51 anbi1i ( ( ⟨ 𝐴 , 𝐵 ⟩ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) 𝑥𝑥 Cap 𝐶 ) ↔ ( 𝑥 = ⟨ 𝐴 , ( 𝐵 × ran 𝐴 ) ⟩ ∧ 𝑥 Cap 𝐶 ) )
53 52 exbii ( ∃ 𝑥 ( ⟨ 𝐴 , 𝐵 ⟩ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) 𝑥𝑥 Cap 𝐶 ) ↔ ∃ 𝑥 ( 𝑥 = ⟨ 𝐴 , ( 𝐵 × ran 𝐴 ) ⟩ ∧ 𝑥 Cap 𝐶 ) )
54 5 53 bitri ( ⟨ 𝐴 , 𝐵 ⟩ ( Cap ∘ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) ) 𝐶 ↔ ∃ 𝑥 ( 𝑥 = ⟨ 𝐴 , ( 𝐵 × 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 ∘ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) ) 𝐶𝐶 = ( 𝐴 ∩ ( 𝐵 × ran 𝐴 ) ) )
60 df-restrict Restrict = ( Cap ∘ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) )
61 60 breqi ( ⟨ 𝐴 , 𝐵 ⟩ Restrict 𝐶 ↔ ⟨ 𝐴 , 𝐵 ⟩ ( Cap ∘ ( 1st ⊗ ( Cart ∘ ( 2nd ⊗ ( Range ∘ 1st ) ) ) ) ) 𝐶 )
62 dfres3 ( 𝐴𝐵 ) = ( 𝐴 ∩ ( 𝐵 × ran 𝐴 ) )
63 62 eqeq2i ( 𝐶 = ( 𝐴𝐵 ) ↔ 𝐶 = ( 𝐴 ∩ ( 𝐵 × ran 𝐴 ) ) )
64 59 61 63 3bitr4i ( ⟨ 𝐴 , 𝐵 ⟩ Restrict 𝐶𝐶 = ( 𝐴𝐵 ) )