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

Theorem fmptcof2 30420
 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 6064 . 2 Rel (𝐺𝐹)
2 mptrel 5661 . 2 Rel (𝑥𝐴𝑇)
3 fmptcof2.3 . . . . . . . . . . . . 13 𝑥𝜑
4 fmptcof2.1 . . . . . . . . . . . . 13 𝑥𝐴
5 fmptcof2.2 . . . . . . . . . . . . 13 𝑥𝐵
6 fmptcof2.4 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐴 𝑅𝐵)
76r19.21bi 3173 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑅𝐵)
8 eqid 2798 . . . . . . . . . . . . 13 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
93, 4, 5, 7, 8fmptdF 30419 . . . . . . . . . . . 12 (𝜑 → (𝑥𝐴𝑅):𝐴𝐵)
10 fmptcof2.5 . . . . . . . . . . . . 13 (𝜑𝐹 = (𝑥𝐴𝑅))
1110feq1d 6472 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐴𝐵 ↔ (𝑥𝐴𝑅):𝐴𝐵))
129, 11mpbird 260 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
1312ffund 6491 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
14 funbrfv 6691 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
1514imp 410 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
1613, 15sylan 583 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
1716eqcomd 2804 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
1817a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
1918expimpd 457 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
2019pm4.71rd 566 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
2120exbidv 1922 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
22 fvex 6658 . . . . . 6 (𝐹𝑧) ∈ V
23 breq2 5034 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
24 breq1 5033 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
2523, 24anbi12d 633 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
2622, 25ceqsexv 3489 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
27 funfvbrb 6798 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
2813, 27syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
2912fdmd 6497 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
3029eleq2d 2875 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
3128, 30bitr3d 284 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
3210fveq1d 6647 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
33 fmptcof2.6 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
34 eqidd 2799 . . . . . . . 8 (𝜑𝑤 = 𝑤)
3532, 33, 34breq123d 5044 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
3631, 35anbi12d 633 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
374nfcri 2943 . . . . . . . . . 10 𝑥 𝑧𝐴
38 nffvmpt1 6656 . . . . . . . . . . . . 13 𝑥((𝑥𝐴𝑅)‘𝑧)
39 fmptcof2.x . . . . . . . . . . . . . 14 𝑥𝑆
405, 39nfmpt 5127 . . . . . . . . . . . . 13 𝑥(𝑦𝐵𝑆)
41 nfcv 2955 . . . . . . . . . . . . 13 𝑥𝑤
4238, 40, 41nfbr 5077 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
43 nfcsb1v 3852 . . . . . . . . . . . . 13 𝑥𝑧 / 𝑥𝑇
4443nfeq2 2972 . . . . . . . . . . . 12 𝑥 𝑤 = 𝑧 / 𝑥𝑇
4542, 44nfbi 1904 . . . . . . . . . . 11 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
463, 45nfim 1897 . . . . . . . . . 10 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
4737, 46nfim 1897 . . . . . . . . 9 𝑥(𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
48 eleq1w 2872 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
49 fveq2 6645 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
5049breq1d 5040 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
51 csbeq1a 3842 . . . . . . . . . . . . 13 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
5251eqeq2d 2809 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
5350, 52bibi12d 349 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
5453imbi2d 344 . . . . . . . . . 10 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
5548, 54imbi12d 348 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))) ↔ (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))))
56 vex 3444 . . . . . . . . . . . 12 𝑤 ∈ V
57 nfv 1915 . . . . . . . . . . . . . 14 𝑦 𝑅𝐵
58 fmptcof2.y . . . . . . . . . . . . . . 15 𝑦𝑇
5958nfeq2 2972 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑇
6057, 59nfan 1900 . . . . . . . . . . . . 13 𝑦(𝑅𝐵𝑤 = 𝑇)
61 simpl 486 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
6261eleq1d 2874 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
63 simpr 488 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑢 = 𝑤)
64 fmptcof2.7 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑅𝑆 = 𝑇)
6564adantr 484 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑆 = 𝑇)
6663, 65eqeq12d 2814 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
6762, 66anbi12d 633 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
68 df-mpt 5111 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
6960, 67, 68brabgaf 30372 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
707, 56, 69sylancl 589 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
71 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑥𝐴)
724fvmpt2f 6746 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7371, 7, 72syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7473breq1d 5040 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
757biantrurd 536 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
7670, 74, 753bitr4d 314 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
7776expcom 417 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
7847, 55, 77chvarfv 2240 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
7978impcom 411 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
8079pm5.32da 582 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8136, 80bitrd 282 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8226, 81syl5bb 286 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8321, 82bitrd 282 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
84 vex 3444 . . . 4 𝑧 ∈ V
8584, 56opelco 5706 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
86 df-mpt 5111 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
8786eleq2i 2881 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
8843nfeq2 2972 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
8937, 88nfan 1900 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
90 nfv 1915 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
9151eqeq2d 2809 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
9248, 91anbi12d 633 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
93 eqeq1 2802 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
9493anbi2d 631 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
9589, 90, 84, 56, 92, 94opelopabf 5397 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
9687, 95bitri 278 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
9783, 85, 963bitr4g 317 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
981, 2, 97eqrelrdv 5629 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2936  ∀wral 3106  Vcvv 3441  ⦋csb 3828  ⟨cop 4531   class class class wbr 5030  {copab 5092   ↦ cmpt 5110  dom cdm 5519   ∘ ccom 5523  Fun wfun 6318  ⟶wf 6320  ‘cfv 6324 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332 This theorem is referenced by:  esumf1o  31419
 Copyright terms: Public domain W3C validator