Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fmptcof2 Structured version   Visualization version   GIF version

Theorem fmptcof2 30330
Description: Composition of two functions expressed as ordered-pair class abstractions. (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.) (Revised by Thierry Arnoux, 10-May-2017.)
Hypotheses
Ref Expression
fmptcof2.x 𝑥𝑆
fmptcof2.y 𝑦𝑇
fmptcof2.1 𝑥𝐴
fmptcof2.2 𝑥𝐵
fmptcof2.3 𝑥𝜑
fmptcof2.4 (𝜑 → ∀𝑥𝐴 𝑅𝐵)
fmptcof2.5 (𝜑𝐹 = (𝑥𝐴𝑅))
fmptcof2.6 (𝜑𝐺 = (𝑦𝐵𝑆))
fmptcof2.7 (𝑦 = 𝑅𝑆 = 𝑇)
Assertion
Ref Expression
fmptcof2 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Distinct variable groups:   𝑥,𝑦   𝑦,𝐵   𝑦,𝑅
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥)   𝑅(𝑥)   𝑆(𝑥,𝑦)   𝑇(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem fmptcof2
Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 6090 . 2 Rel (𝐺𝐹)
2 mptrel 5690 . 2 Rel (𝑥𝐴𝑇)
3 fmptcof2.3 . . . . . . . . . . . . 13 𝑥𝜑
4 fmptcof2.1 . . . . . . . . . . . . 13 𝑥𝐴
5 fmptcof2.2 . . . . . . . . . . . . 13 𝑥𝐵
6 fmptcof2.4 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐴 𝑅𝐵)
76r19.21bi 3205 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑅𝐵)
8 eqid 2818 . . . . . . . . . . . . 13 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
93, 4, 5, 7, 8fmptdF 30329 . . . . . . . . . . . 12 (𝜑 → (𝑥𝐴𝑅):𝐴𝐵)
10 fmptcof2.5 . . . . . . . . . . . . 13 (𝜑𝐹 = (𝑥𝐴𝑅))
1110feq1d 6492 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐴𝐵 ↔ (𝑥𝐴𝑅):𝐴𝐵))
129, 11mpbird 258 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
1312ffund 6511 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
14 funbrfv 6709 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
1514imp 407 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
1613, 15sylan 580 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
1716eqcomd 2824 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
1817a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
1918expimpd 454 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
2019pm4.71rd 563 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
2120exbidv 1913 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
22 fvex 6676 . . . . . 6 (𝐹𝑧) ∈ V
23 breq2 5061 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
24 breq1 5060 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
2523, 24anbi12d 630 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
2622, 25ceqsexv 3539 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
27 funfvbrb 6813 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
2813, 27syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
2912fdmd 6516 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
3029eleq2d 2895 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
3128, 30bitr3d 282 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
3210fveq1d 6665 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
33 fmptcof2.6 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
34 eqidd 2819 . . . . . . . 8 (𝜑𝑤 = 𝑤)
3532, 33, 34breq123d 5071 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
3631, 35anbi12d 630 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
374nfcri 2968 . . . . . . . . . 10 𝑥 𝑧𝐴
38 nffvmpt1 6674 . . . . . . . . . . . . 13 𝑥((𝑥𝐴𝑅)‘𝑧)
39 fmptcof2.x . . . . . . . . . . . . . 14 𝑥𝑆
405, 39nfmpt 5154 . . . . . . . . . . . . 13 𝑥(𝑦𝐵𝑆)
41 nfcv 2974 . . . . . . . . . . . . 13 𝑥𝑤
4238, 40, 41nfbr 5104 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
43 nfcsb1v 3904 . . . . . . . . . . . . 13 𝑥𝑧 / 𝑥𝑇
4443nfeq2 2992 . . . . . . . . . . . 12 𝑥 𝑤 = 𝑧 / 𝑥𝑇
4542, 44nfbi 1895 . . . . . . . . . . 11 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
463, 45nfim 1888 . . . . . . . . . 10 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
4737, 46nfim 1888 . . . . . . . . 9 𝑥(𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
48 eleq1w 2892 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
49 fveq2 6663 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
5049breq1d 5067 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
51 csbeq1a 3894 . . . . . . . . . . . . 13 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
5251eqeq2d 2829 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
5350, 52bibi12d 347 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
5453imbi2d 342 . . . . . . . . . 10 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
5548, 54imbi12d 346 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))) ↔ (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))))
56 vex 3495 . . . . . . . . . . . 12 𝑤 ∈ V
57 nfv 1906 . . . . . . . . . . . . . 14 𝑦 𝑅𝐵
58 fmptcof2.y . . . . . . . . . . . . . . 15 𝑦𝑇
5958nfeq2 2992 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑇
6057, 59nfan 1891 . . . . . . . . . . . . 13 𝑦(𝑅𝐵𝑤 = 𝑇)
61 simpl 483 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
6261eleq1d 2894 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
63 simpr 485 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑢 = 𝑤)
64 fmptcof2.7 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑅𝑆 = 𝑇)
6564adantr 481 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑆 = 𝑇)
6663, 65eqeq12d 2834 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
6762, 66anbi12d 630 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
68 df-mpt 5138 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
6960, 67, 68brabgaf 30287 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
707, 56, 69sylancl 586 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
71 simpr 485 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑥𝐴)
724fvmpt2f 6762 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7371, 7, 72syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7473breq1d 5067 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
757biantrurd 533 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
7670, 74, 753bitr4d 312 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
7776expcom 414 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
7847, 55, 77chvarfv 2232 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
7978impcom 408 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
8079pm5.32da 579 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8136, 80bitrd 280 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8226, 81syl5bb 284 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8321, 82bitrd 280 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
84 vex 3495 . . . 4 𝑧 ∈ V
8584, 56opelco 5735 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
86 df-mpt 5138 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
8786eleq2i 2901 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
8843nfeq2 2992 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
8937, 88nfan 1891 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
90 nfv 1906 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
9151eqeq2d 2829 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
9248, 91anbi12d 630 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
93 eqeq1 2822 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
9493anbi2d 628 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
9589, 90, 84, 56, 92, 94opelopabf 5423 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
9687, 95bitri 276 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
9783, 85, 963bitr4g 315 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
981, 2, 97eqrelrdv 5658 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wex 1771  wnf 1775  wcel 2105  wnfc 2958  wral 3135  Vcvv 3492  csb 3880  cop 4563   class class class wbr 5057  {copab 5119  cmpt 5137  dom cdm 5548  ccom 5552  Fun wfun 6342  wf 6344  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356
This theorem is referenced by:  esumf1o  31208
  Copyright terms: Public domain W3C validator