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 29585
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 5671 . 2 Rel (𝐺𝐹)
2 funmpt 5964 . . 3 Fun (𝑥𝐴𝑇)
3 funrel 5943 . . 3 (Fun (𝑥𝐴𝑇) → Rel (𝑥𝐴𝑇))
42, 3ax-mp 5 . 2 Rel (𝑥𝐴𝑇)
5 fmptcof2.3 . . . . . . . . . . . . 13 𝑥𝜑
6 fmptcof2.1 . . . . . . . . . . . . 13 𝑥𝐴
7 fmptcof2.2 . . . . . . . . . . . . 13 𝑥𝐵
8 fmptcof2.4 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐴 𝑅𝐵)
98r19.21bi 2961 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑅𝐵)
10 eqid 2651 . . . . . . . . . . . . 13 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
115, 6, 7, 9, 10fmptdF 29584 . . . . . . . . . . . 12 (𝜑 → (𝑥𝐴𝑅):𝐴𝐵)
12 fmptcof2.5 . . . . . . . . . . . . 13 (𝜑𝐹 = (𝑥𝐴𝑅))
1312feq1d 6068 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐴𝐵 ↔ (𝑥𝐴𝑅):𝐴𝐵))
1411, 13mpbird 247 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
15 ffun 6086 . . . . . . . . . . 11 (𝐹:𝐴𝐵 → Fun 𝐹)
1614, 15syl 17 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
17 funbrfv 6272 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
1817imp 444 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
1916, 18sylan 487 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
2019eqcomd 2657 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
2120a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
2221expimpd 628 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
2322pm4.71rd 668 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
2423exbidv 1890 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
25 fvex 6239 . . . . . 6 (𝐹𝑧) ∈ V
26 breq2 4689 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
27 breq1 4688 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
2826, 27anbi12d 747 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
2925, 28ceqsexv 3273 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
30 funfvbrb 6370 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
3116, 30syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
32 fdm 6089 . . . . . . . . . 10 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
3314, 32syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
3433eleq2d 2716 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
3531, 34bitr3d 270 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
3612fveq1d 6231 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
37 fmptcof2.6 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
38 eqidd 2652 . . . . . . . 8 (𝜑𝑤 = 𝑤)
3936, 37, 38breq123d 4699 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
4035, 39anbi12d 747 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
416nfcri 2787 . . . . . . . . . 10 𝑥 𝑧𝐴
42 nffvmpt1 6237 . . . . . . . . . . . . 13 𝑥((𝑥𝐴𝑅)‘𝑧)
43 fmptcof2.x . . . . . . . . . . . . . 14 𝑥𝑆
447, 43nfmpt 4779 . . . . . . . . . . . . 13 𝑥(𝑦𝐵𝑆)
45 nfcv 2793 . . . . . . . . . . . . 13 𝑥𝑤
4642, 44, 45nfbr 4732 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
47 nfcsb1v 3582 . . . . . . . . . . . . 13 𝑥𝑧 / 𝑥𝑇
4847nfeq2 2809 . . . . . . . . . . . 12 𝑥 𝑤 = 𝑧 / 𝑥𝑇
4946, 48nfbi 1873 . . . . . . . . . . 11 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
505, 49nfim 1865 . . . . . . . . . 10 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
5141, 50nfim 1865 . . . . . . . . 9 𝑥(𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
52 eleq1 2718 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
53 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
5453breq1d 4695 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
55 csbeq1a 3575 . . . . . . . . . . . . 13 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
5655eqeq2d 2661 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
5754, 56bibi12d 334 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
5857imbi2d 329 . . . . . . . . . 10 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
5952, 58imbi12d 333 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))) ↔ (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))))
60 vex 3234 . . . . . . . . . . . 12 𝑤 ∈ V
61 nfv 1883 . . . . . . . . . . . . . 14 𝑦 𝑅𝐵
62 nfcv 2793 . . . . . . . . . . . . . . 15 𝑦𝑤
63 fmptcof2.y . . . . . . . . . . . . . . 15 𝑦𝑇
6462, 63nfeq 2805 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑇
6561, 64nfan 1868 . . . . . . . . . . . . 13 𝑦(𝑅𝐵𝑤 = 𝑇)
66 simpl 472 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
6766eleq1d 2715 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
68 simpr 476 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑢 = 𝑤)
69 fmptcof2.7 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑅𝑆 = 𝑇)
7069adantr 480 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑆 = 𝑇)
7168, 70eqeq12d 2666 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
7267, 71anbi12d 747 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
73 df-mpt 4763 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
7465, 72, 73brabgaf 29546 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
759, 60, 74sylancl 695 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
76 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑥𝐴)
776fvmpt2f 6322 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7876, 9, 77syl2anc 694 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7978breq1d 4695 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
809biantrurd 528 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
8175, 79, 803bitr4d 300 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
8281expcom 450 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
8351, 59, 82chvar 2298 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
8483impcom 445 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
8584pm5.32da 674 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8640, 85bitrd 268 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8729, 86syl5bb 272 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8824, 87bitrd 268 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
89 vex 3234 . . . 4 𝑧 ∈ V
9089, 60opelco 5326 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
91 df-mpt 4763 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
9291eleq2i 2722 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
9347nfeq2 2809 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
9441, 93nfan 1868 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
95 nfv 1883 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
9655eqeq2d 2661 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
9752, 96anbi12d 747 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
98 eqeq1 2655 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
9998anbi2d 740 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
10094, 95, 89, 60, 97, 99opelopabf 5029 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
10192, 100bitri 264 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
10288, 90, 1013bitr4g 303 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
1031, 4, 102eqrelrdv 5250 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wex 1744  wnf 1748  wcel 2030  wnfc 2780  wral 2941  Vcvv 3231  csb 3566  cop 4216   class class class wbr 4685  {copab 4745  cmpt 4762  dom cdm 5143  ccom 5147  Rel wrel 5148  Fun wfun 5920  wf 5922  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934
This theorem is referenced by:  esumf1o  30240
  Copyright terms: Public domain W3C validator