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

Theorem fmptcof2 28839
 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 5550 . 2 Rel (𝐺𝐹)
2 funmpt 5840 . . 3 Fun (𝑥𝐴𝑇)
3 funrel 5821 . . 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 2916 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑅𝐵)
10 eqid 2610 . . . . . . . . . . . . 13 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
115, 6, 7, 9, 10fmptdF 28836 . . . . . . . . . . . 12 (𝜑 → (𝑥𝐴𝑅):𝐴𝐵)
12 fmptcof2.5 . . . . . . . . . . . . 13 (𝜑𝐹 = (𝑥𝐴𝑅))
1312feq1d 5943 . . . . . . . . . . . 12 (𝜑 → (𝐹:𝐴𝐵 ↔ (𝑥𝐴𝑅):𝐴𝐵))
1411, 13mpbird 246 . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
15 ffun 5961 . . . . . . . . . . 11 (𝐹:𝐴𝐵 → Fun 𝐹)
1614, 15syl 17 . . . . . . . . . 10 (𝜑 → Fun 𝐹)
17 funbrfv 6144 . . . . . . . . . . 11 (Fun 𝐹 → (𝑧𝐹𝑢 → (𝐹𝑧) = 𝑢))
1817imp 444 . . . . . . . . . 10 ((Fun 𝐹𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
1916, 18sylan 487 . . . . . . . . 9 ((𝜑𝑧𝐹𝑢) → (𝐹𝑧) = 𝑢)
2019eqcomd 2616 . . . . . . . 8 ((𝜑𝑧𝐹𝑢) → 𝑢 = (𝐹𝑧))
2120a1d 25 . . . . . . 7 ((𝜑𝑧𝐹𝑢) → (𝑢𝐺𝑤𝑢 = (𝐹𝑧)))
2221expimpd 627 . . . . . 6 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) → 𝑢 = (𝐹𝑧)))
2322pm4.71rd 665 . . . . 5 (𝜑 → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
2423exbidv 1837 . . . 4 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ ∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤))))
25 fvex 6113 . . . . . 6 (𝐹𝑧) ∈ V
26 breq2 4587 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑧𝐹𝑢𝑧𝐹(𝐹𝑧)))
27 breq1 4586 . . . . . . 7 (𝑢 = (𝐹𝑧) → (𝑢𝐺𝑤 ↔ (𝐹𝑧)𝐺𝑤))
2826, 27anbi12d 743 . . . . . 6 (𝑢 = (𝐹𝑧) → ((𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤)))
2925, 28ceqsexv 3215 . . . . 5 (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤))
30 funfvbrb 6238 . . . . . . . . 9 (Fun 𝐹 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
3116, 30syl 17 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐹(𝐹𝑧)))
32 fdm 5964 . . . . . . . . . 10 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
3314, 32syl 17 . . . . . . . . 9 (𝜑 → dom 𝐹 = 𝐴)
3433eleq2d 2673 . . . . . . . 8 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
3531, 34bitr3d 269 . . . . . . 7 (𝜑 → (𝑧𝐹(𝐹𝑧) ↔ 𝑧𝐴))
3612fveq1d 6105 . . . . . . . 8 (𝜑 → (𝐹𝑧) = ((𝑥𝐴𝑅)‘𝑧))
37 fmptcof2.6 . . . . . . . 8 (𝜑𝐺 = (𝑦𝐵𝑆))
38 eqidd 2611 . . . . . . . 8 (𝜑𝑤 = 𝑤)
3936, 37, 38breq123d 4597 . . . . . . 7 (𝜑 → ((𝐹𝑧)𝐺𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
4035, 39anbi12d 743 . . . . . 6 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤)))
416nfcri 2745 . . . . . . . . . 10 𝑥 𝑧𝐴
42 nffvmpt1 6111 . . . . . . . . . . . . 13 𝑥((𝑥𝐴𝑅)‘𝑧)
43 fmptcof2.x . . . . . . . . . . . . . 14 𝑥𝑆
447, 43nfmpt 4674 . . . . . . . . . . . . 13 𝑥(𝑦𝐵𝑆)
45 nfcv 2751 . . . . . . . . . . . . 13 𝑥𝑤
4642, 44, 45nfbr 4629 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤
47 nfcsb1v 3515 . . . . . . . . . . . . 13 𝑥𝑧 / 𝑥𝑇
4847nfeq2 2766 . . . . . . . . . . . 12 𝑥 𝑤 = 𝑧 / 𝑥𝑇
4946, 48nfbi 1821 . . . . . . . . . . 11 𝑥(((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)
505, 49nfim 1813 . . . . . . . . . 10 𝑥(𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
5141, 50nfim 1813 . . . . . . . . 9 𝑥(𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
52 eleq1 2676 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
53 fveq2 6103 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → ((𝑥𝐴𝑅)‘𝑥) = ((𝑥𝐴𝑅)‘𝑧))
5453breq1d 4593 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤 ↔ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤))
55 csbeq1a 3508 . . . . . . . . . . . . 13 (𝑥 = 𝑧𝑇 = 𝑧 / 𝑥𝑇)
5655eqeq2d 2620 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑤 = 𝑇𝑤 = 𝑧 / 𝑥𝑇))
5754, 56bibi12d 334 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇) ↔ (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
5857imbi2d 329 . . . . . . . . . 10 (𝑥 = 𝑧 → ((𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)) ↔ (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))))
5952, 58imbi12d 333 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))) ↔ (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))))
60 vex 3176 . . . . . . . . . . . 12 𝑤 ∈ V
61 nfv 1830 . . . . . . . . . . . . . 14 𝑦 𝑅𝐵
62 nfcv 2751 . . . . . . . . . . . . . . 15 𝑦𝑤
63 fmptcof2.y . . . . . . . . . . . . . . 15 𝑦𝑇
6462, 63nfeq 2762 . . . . . . . . . . . . . 14 𝑦 𝑤 = 𝑇
6561, 64nfan 1816 . . . . . . . . . . . . 13 𝑦(𝑅𝐵𝑤 = 𝑇)
66 simpl 472 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑦 = 𝑅)
6766eleq1d 2672 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑦𝐵𝑅𝐵))
68 simpr 476 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑢 = 𝑤)
69 fmptcof2.7 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑅𝑆 = 𝑇)
7069adantr 480 . . . . . . . . . . . . . . 15 ((𝑦 = 𝑅𝑢 = 𝑤) → 𝑆 = 𝑇)
7168, 70eqeq12d 2625 . . . . . . . . . . . . . 14 ((𝑦 = 𝑅𝑢 = 𝑤) → (𝑢 = 𝑆𝑤 = 𝑇))
7267, 71anbi12d 743 . . . . . . . . . . . . 13 ((𝑦 = 𝑅𝑢 = 𝑤) → ((𝑦𝐵𝑢 = 𝑆) ↔ (𝑅𝐵𝑤 = 𝑇)))
73 df-mpt 4645 . . . . . . . . . . . . 13 (𝑦𝐵𝑆) = {⟨𝑦, 𝑢⟩ ∣ (𝑦𝐵𝑢 = 𝑆)}
7465, 72, 73brabgaf 28800 . . . . . . . . . . . 12 ((𝑅𝐵𝑤 ∈ V) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
759, 60, 74sylancl 693 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑅(𝑦𝐵𝑆)𝑤 ↔ (𝑅𝐵𝑤 = 𝑇)))
76 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → 𝑥𝐴)
776fvmpt2f 6192 . . . . . . . . . . . . 13 ((𝑥𝐴𝑅𝐵) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7876, 9, 77syl2anc 691 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ((𝑥𝐴𝑅)‘𝑥) = 𝑅)
7978breq1d 4593 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑅(𝑦𝐵𝑆)𝑤))
809biantrurd 528 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (𝑤 = 𝑇 ↔ (𝑅𝐵𝑤 = 𝑇)))
8175, 79, 803bitr4d 299 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇))
8281expcom 450 . . . . . . . . 9 (𝑥𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑥)(𝑦𝐵𝑆)𝑤𝑤 = 𝑇)))
8351, 59, 82chvar 2250 . . . . . . . 8 (𝑧𝐴 → (𝜑 → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇)))
8483impcom 445 . . . . . . 7 ((𝜑𝑧𝐴) → (((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤𝑤 = 𝑧 / 𝑥𝑇))
8584pm5.32da 671 . . . . . 6 (𝜑 → ((𝑧𝐴 ∧ ((𝑥𝐴𝑅)‘𝑧)(𝑦𝐵𝑆)𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8640, 85bitrd 267 . . . . 5 (𝜑 → ((𝑧𝐹(𝐹𝑧) ∧ (𝐹𝑧)𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8729, 86syl5bb 271 . . . 4 (𝜑 → (∃𝑢(𝑢 = (𝐹𝑧) ∧ (𝑧𝐹𝑢𝑢𝐺𝑤)) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
8824, 87bitrd 267 . . 3 (𝜑 → (∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
89 vex 3176 . . . 4 𝑧 ∈ V
9089, 60opelco 5215 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ∃𝑢(𝑧𝐹𝑢𝑢𝐺𝑤))
91 df-mpt 4645 . . . . 5 (𝑥𝐴𝑇) = {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)}
9291eleq2i 2680 . . . 4 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ ⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)})
9347nfeq2 2766 . . . . . 6 𝑥 𝑣 = 𝑧 / 𝑥𝑇
9441, 93nfan 1816 . . . . 5 𝑥(𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)
95 nfv 1830 . . . . 5 𝑣(𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)
9655eqeq2d 2620 . . . . . 6 (𝑥 = 𝑧 → (𝑣 = 𝑇𝑣 = 𝑧 / 𝑥𝑇))
9752, 96anbi12d 743 . . . . 5 (𝑥 = 𝑧 → ((𝑥𝐴𝑣 = 𝑇) ↔ (𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇)))
98 eqeq1 2614 . . . . . 6 (𝑣 = 𝑤 → (𝑣 = 𝑧 / 𝑥𝑇𝑤 = 𝑧 / 𝑥𝑇))
9998anbi2d 736 . . . . 5 (𝑣 = 𝑤 → ((𝑧𝐴𝑣 = 𝑧 / 𝑥𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇)))
10094, 95, 89, 60, 97, 99opelopabf 4925 . . . 4 (⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑣⟩ ∣ (𝑥𝐴𝑣 = 𝑇)} ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
10192, 100bitri 263 . . 3 (⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇) ↔ (𝑧𝐴𝑤 = 𝑧 / 𝑥𝑇))
10288, 90, 1013bitr4g 302 . 2 (𝜑 → (⟨𝑧, 𝑤⟩ ∈ (𝐺𝐹) ↔ ⟨𝑧, 𝑤⟩ ∈ (𝑥𝐴𝑇)))
1031, 4, 102eqrelrdv 5139 1 (𝜑 → (𝐺𝐹) = (𝑥𝐴𝑇))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738  ∀wral 2896  Vcvv 3173  ⦋csb 3499  ⟨cop 4131   class class class wbr 4583  {copab 4642   ↦ cmpt 4643  dom cdm 5038   ∘ ccom 5042  Rel wrel 5043  Fun wfun 5798  ⟶wf 5800  ‘cfv 5804 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812 This theorem is referenced by:  esumf1o  29439
 Copyright terms: Public domain W3C validator