Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brrestrict Structured version   Visualization version   GIF version

Theorem brrestrict 31733
 Description: The binary relationship 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.
StepHypRef Expression
1 opex 4898 . . . . 5 𝐴, 𝐵⟩ ∈ V
2 brrestrict.3 . . . . 5 𝐶 ∈ V
31, 2brco 5257 . . . 4 (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥𝑥Cap𝐶))
41brtxp2 31665 . . . . . . 7 (⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ↔ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏))
5 3anrot 1041 . . . . . . . . 9 ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ (⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏𝑥 = ⟨𝑎, 𝑏⟩))
6 brrestrict.1 . . . . . . . . . . 11 𝐴 ∈ V
7 brrestrict.2 . . . . . . . . . . 11 𝐵 ∈ V
8 vex 3192 . . . . . . . . . . 11 𝑎 ∈ V
96, 7, 8br1steq 31409 . . . . . . . . . 10 (⟨𝐴, 𝐵⟩1st 𝑎𝑎 = 𝐴)
10 vex 3192 . . . . . . . . . . . 12 𝑏 ∈ V
111, 10brco 5257 . . . . . . . . . . 11 (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥𝑥Cart𝑏))
121brtxp2 31665 . . . . . . . . . . . . . . 15 (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥 ↔ ∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏))
13 3anrot 1041 . . . . . . . . . . . . . . . . 17 ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏𝑥 = ⟨𝑎, 𝑏⟩))
146, 7, 8br2ndeq 31410 . . . . . . . . . . . . . . . . . 18 (⟨𝐴, 𝐵⟩2nd 𝑎𝑎 = 𝐵)
151, 10brco 5257 . . . . . . . . . . . . . . . . . . 19 (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏 ↔ ∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥𝑥Range𝑏))
16 vex 3192 . . . . . . . . . . . . . . . . . . . . . . 23 𝑥 ∈ V
176, 7, 16br1steq 31409 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝐴, 𝐵⟩1st 𝑥𝑥 = 𝐴)
1817anbi1i 730 . . . . . . . . . . . . . . . . . . . . 21 ((⟨𝐴, 𝐵⟩1st 𝑥𝑥Range𝑏) ↔ (𝑥 = 𝐴𝑥Range𝑏))
1918exbii 1771 . . . . . . . . . . . . . . . . . . . 20 (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥𝑥Range𝑏) ↔ ∃𝑥(𝑥 = 𝐴𝑥Range𝑏))
20 breq1 4621 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝐴 → (𝑥Range𝑏𝐴Range𝑏))
216, 20ceqsexv 3231 . . . . . . . . . . . . . . . . . . . 20 (∃𝑥(𝑥 = 𝐴𝑥Range𝑏) ↔ 𝐴Range𝑏)
2219, 21bitri 264 . . . . . . . . . . . . . . . . . . 19 (∃𝑥(⟨𝐴, 𝐵⟩1st 𝑥𝑥Range𝑏) ↔ 𝐴Range𝑏)
236, 10brrange 31718 . . . . . . . . . . . . . . . . . . 19 (𝐴Range𝑏𝑏 = ran 𝐴)
2415, 22, 233bitri 286 . . . . . . . . . . . . . . . . . 18 (⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏𝑏 = ran 𝐴)
25 biid 251 . . . . . . . . . . . . . . . . . 18 (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝑎, 𝑏⟩)
2614, 24, 253anbi123i 1249 . . . . . . . . . . . . . . . . 17 ((⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏𝑥 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐵𝑏 = ran 𝐴𝑥 = ⟨𝑎, 𝑏⟩))
2713, 26bitri 264 . . . . . . . . . . . . . . . 16 ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ (𝑎 = 𝐵𝑏 = ran 𝐴𝑥 = ⟨𝑎, 𝑏⟩))
28272exbii 1772 . . . . . . . . . . . . . . 15 (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩2nd 𝑎 ∧ ⟨𝐴, 𝐵⟩(Range ∘ 1st )𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝐵𝑏 = ran 𝐴𝑥 = ⟨𝑎, 𝑏⟩))
296rnex 7054 . . . . . . . . . . . . . . . 16 ran 𝐴 ∈ V
30 opeq1 4375 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝐵 → ⟨𝑎, 𝑏⟩ = ⟨𝐵, 𝑏⟩)
3130eqeq2d 2631 . . . . . . . . . . . . . . . 16 (𝑎 = 𝐵 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, 𝑏⟩))
32 opeq2 4376 . . . . . . . . . . . . . . . . 17 (𝑏 = ran 𝐴 → ⟨𝐵, 𝑏⟩ = ⟨𝐵, ran 𝐴⟩)
3332eqeq2d 2631 . . . . . . . . . . . . . . . 16 (𝑏 = ran 𝐴 → (𝑥 = ⟨𝐵, 𝑏⟩ ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩))
347, 29, 31, 33ceqsex2v 3234 . . . . . . . . . . . . . . 15 (∃𝑎𝑏(𝑎 = 𝐵𝑏 = ran 𝐴𝑥 = ⟨𝑎, 𝑏⟩) ↔ 𝑥 = ⟨𝐵, ran 𝐴⟩)
3512, 28, 343bitri 286 . . . . . . . . . . . . . 14 (⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥𝑥 = ⟨𝐵, ran 𝐴⟩)
3635anbi1i 730 . . . . . . . . . . . . 13 ((⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥𝑥Cart𝑏) ↔ (𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
3736exbii 1771 . . . . . . . . . . . 12 (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥𝑥Cart𝑏) ↔ ∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏))
38 opex 4898 . . . . . . . . . . . . 13 𝐵, ran 𝐴⟩ ∈ V
39 breq1 4621 . . . . . . . . . . . . 13 (𝑥 = ⟨𝐵, ran 𝐴⟩ → (𝑥Cart𝑏 ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏))
4038, 39ceqsexv 3231 . . . . . . . . . . . 12 (∃𝑥(𝑥 = ⟨𝐵, ran 𝐴⟩ ∧ 𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
4137, 40bitri 264 . . . . . . . . . . 11 (∃𝑥(⟨𝐴, 𝐵⟩(2nd ⊗ (Range ∘ 1st ))𝑥𝑥Cart𝑏) ↔ ⟨𝐵, ran 𝐴⟩Cart𝑏)
427, 29, 10brcart 31716 . . . . . . . . . . 11 (⟨𝐵, ran 𝐴⟩Cart𝑏𝑏 = (𝐵 × ran 𝐴))
4311, 41, 423bitri 286 . . . . . . . . . 10 (⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏𝑏 = (𝐵 × ran 𝐴))
449, 43, 253anbi123i 1249 . . . . . . . . 9 ((⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏𝑥 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝐴𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
455, 44bitri 264 . . . . . . . 8 ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ (𝑎 = 𝐴𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
46452exbii 1772 . . . . . . 7 (∃𝑎𝑏(𝑥 = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐴, 𝐵⟩1st 𝑎 ∧ ⟨𝐴, 𝐵⟩(Cart ∘ (2nd ⊗ (Range ∘ 1st )))𝑏) ↔ ∃𝑎𝑏(𝑎 = 𝐴𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩))
477, 29xpex 6922 . . . . . . . 8 (𝐵 × ran 𝐴) ∈ V
48 opeq1 4375 . . . . . . . . 9 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
4948eqeq2d 2631 . . . . . . . 8 (𝑎 = 𝐴 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, 𝑏⟩))
50 opeq2 4376 . . . . . . . . 9 (𝑏 = (𝐵 × ran 𝐴) → ⟨𝐴, 𝑏⟩ = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
5150eqeq2d 2631 . . . . . . . 8 (𝑏 = (𝐵 × ran 𝐴) → (𝑥 = ⟨𝐴, 𝑏⟩ ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩))
526, 47, 49, 51ceqsex2v 3234 . . . . . . 7 (∃𝑎𝑏(𝑎 = 𝐴𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = ⟨𝑎, 𝑏⟩) ↔ 𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
534, 46, 523bitri 286 . . . . . 6 (⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩)
5453anbi1i 730 . . . . 5 ((⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥𝑥Cap𝐶) ↔ (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
5554exbii 1771 . . . 4 (∃𝑥(⟨𝐴, 𝐵⟩(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥𝑥Cap𝐶) ↔ ∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
563, 55bitri 264 . . 3 (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶 ↔ ∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶))
57 opex 4898 . . . 4 𝐴, (𝐵 × ran 𝐴)⟩ ∈ V
58 breq1 4621 . . . 4 (𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ → (𝑥Cap𝐶 ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶))
5957, 58ceqsexv 3231 . . 3 (∃𝑥(𝑥 = ⟨𝐴, (𝐵 × ran 𝐴)⟩ ∧ 𝑥Cap𝐶) ↔ ⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶)
606, 47, 2brcap 31724 . . 3 (⟨𝐴, (𝐵 × ran 𝐴)⟩Cap𝐶𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
6156, 59, 603bitri 286 . 2 (⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
62 df-restrict 31654 . . 3 Restrict = (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))
6362breqi 4624 . 2 (⟨𝐴, 𝐵⟩Restrict𝐶 ↔ ⟨𝐴, 𝐵⟩(Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶)
64 dfres3 31392 . . 3 (𝐴𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴))
6564eqeq2i 2633 . 2 (𝐶 = (𝐴𝐵) ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴)))
6661, 63, 653bitr4i 292 1 (⟨𝐴, 𝐵⟩Restrict𝐶𝐶 = (𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987  Vcvv 3189   ∩ cin 3558  ⟨cop 4159   class class class wbr 4618   × cxp 5077  ran crn 5080   ↾ cres 5081   ∘ ccom 5083  1st c1st 7118  2nd c2nd 7119   ⊗ ctxp 31613  Cartccart 31624  Rangecrange 31627  Capccap 31630  Restrictcrestrict 31634 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-symdif 3827  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-eprel 4990  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-fo 5858  df-fv 5860  df-1st 7120  df-2nd 7121  df-txp 31637  df-pprod 31638  df-image 31647  df-cart 31648  df-range 31651  df-cap 31653  df-restrict 31654 This theorem is referenced by:  dfrecs2  31734
 Copyright terms: Public domain W3C validator