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 29296
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 5592 . 2 Rel (𝐺𝐹)
2 funmpt 5884 . . 3 Fun (𝑥𝐴𝑇)
3 funrel 5864 . . 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 2927 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑅𝐵)
10 eqid 2621 . . . . . . . . . . . . 13 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
115, 6, 7, 9, 10fmptdF 29295 . . . . . . . . . . . 12 (𝜑 → (𝑥𝐴𝑅):𝐴𝐵)
12 fmptcof2.5 . . . . . . . . . . . . 13 (𝜑𝐹 = (𝑥𝐴𝑅))
1312feq1d 5987 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐴𝐵 ↔ (𝑥𝐴𝑅):𝐴𝐵))
1411, 13mpbird 247 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
15 ffun 6005 . . . . . . . . . . 11 (𝐹:𝐴𝐵 → Fun 𝐹)
1614, 15syl 17 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
17 funbrfv 6191 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
1817imp 445 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
1916, 18sylan 488 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
2019eqcomd 2627 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
2120a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
2221expimpd 628 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
2322pm4.71rd 666 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
2423exbidv 1847 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
25 fvex 6158 . . . . . 6 (𝐹𝑧) ∈ V
26 breq2 4617 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
27 breq1 4616 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
2826, 27anbi12d 746 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
2925, 28ceqsexv 3228 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
30 funfvbrb 6286 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
3116, 30syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
32 fdm 6008 . . . . . . . . . 10 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
3314, 32syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
3433eleq2d 2684 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
3531, 34bitr3d 270 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
3612fveq1d 6150 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
37 fmptcof2.6 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
38 eqidd 2622 . . . . . . . 8 (𝜑𝑤 = 𝑤)
3936, 37, 38breq123d 4627 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
4035, 39anbi12d 746 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
416nfcri 2755 . . . . . . . . . 10 𝑥 𝑧𝐴
42 nffvmpt1 6156 . . . . . . . . . . . . 13 𝑥((𝑥𝐴𝑅)‘𝑧)
43 fmptcof2.x . . . . . . . . . . . . . 14 𝑥𝑆
447, 43nfmpt 4706 . . . . . . . . . . . . 13 𝑥(𝑦𝐵𝑆)
45 nfcv 2761 . . . . . . . . . . . . 13 𝑥𝑤
4642, 44, 45nfbr 4659 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
47 nfcsb1v 3530 . . . . . . . . . . . . 13 𝑥𝑧 / 𝑥𝑇
4847nfeq2 2776 . . . . . . . . . . . 12 𝑥 𝑤 = 𝑧 / 𝑥𝑇
4946, 48nfbi 1830 . . . . . . . . . . 11 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
505, 49nfim 1822 . . . . . . . . . 10 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
5141, 50nfim 1822 . . . . . . . . 9 𝑥(𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
52 eleq1 2686 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
53 fveq2 6148 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
5453breq1d 4623 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
55 csbeq1a 3523 . . . . . . . . . . . . 13 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
5655eqeq2d 2631 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
5754, 56bibi12d 335 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
5857imbi2d 330 . . . . . . . . . 10 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
5952, 58imbi12d 334 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))) ↔ (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))))
60 vex 3189 . . . . . . . . . . . 12 𝑤 ∈ V
61 nfv 1840 . . . . . . . . . . . . . 14 𝑦 𝑅𝐵
62 nfcv 2761 . . . . . . . . . . . . . . 15 𝑦𝑤
63 fmptcof2.y . . . . . . . . . . . . . . 15 𝑦𝑇
6462, 63nfeq 2772 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑇
6561, 64nfan 1825 . . . . . . . . . . . . 13 𝑦(𝑅𝐵𝑤 = 𝑇)
66 simpl 473 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
6766eleq1d 2683 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
68 simpr 477 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑢 = 𝑤)
69 fmptcof2.7 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑅𝑆 = 𝑇)
7069adantr 481 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑆 = 𝑇)
7168, 70eqeq12d 2636 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
7267, 71anbi12d 746 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
73 df-mpt 4675 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
7465, 72, 73brabgaf 29260 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
759, 60, 74sylancl 693 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
76 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑥𝐴)
776fvmpt2f 6240 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7876, 9, 77syl2anc 692 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7978breq1d 4623 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
809biantrurd 529 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
8175, 79, 803bitr4d 300 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
8281expcom 451 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
8351, 59, 82chvar 2261 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
8483impcom 446 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
8584pm5.32da 672 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8640, 85bitrd 268 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8729, 86syl5bb 272 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8824, 87bitrd 268 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
89 vex 3189 . . . 4 𝑧 ∈ V
9089, 60opelco 5253 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
91 df-mpt 4675 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
9291eleq2i 2690 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
9347nfeq2 2776 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
9441, 93nfan 1825 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
95 nfv 1840 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
9655eqeq2d 2631 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
9752, 96anbi12d 746 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
98 eqeq1 2625 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
9998anbi2d 739 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
10094, 95, 89, 60, 97, 99opelopabf 4960 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
10192, 100bitri 264 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
10288, 90, 1013bitr4g 303 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
1031, 4, 102eqrelrdv 5177 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wnf 1705  wcel 1987  wnfc 2748  wral 2907  Vcvv 3186  csb 3514  cop 4154   class class class wbr 4613  {copab 4672  cmpt 4673  dom cdm 5074  ccom 5078  Rel wrel 5079  Fun wfun 5841  wf 5843  cfv 5847
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-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-fal 1486  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 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855
This theorem is referenced by:  esumf1o  29890
  Copyright terms: Public domain W3C validator