MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnco Structured version   Visualization version   GIF version

Theorem fnco 6210
Description: Composition of two functions. (Contributed by NM, 22-May-2006.)
Assertion
Ref Expression
fnco ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴) → (𝐹𝐺) Fn 𝐵)

Proof of Theorem fnco
StepHypRef Expression
1 fnfun 6199 . . . 4 (𝐹 Fn 𝐴 → Fun 𝐹)
2 fnfun 6199 . . . 4 (𝐺 Fn 𝐵 → Fun 𝐺)
3 funco 6141 . . . 4 ((Fun 𝐹 ∧ Fun 𝐺) → Fun (𝐹𝐺))
41, 2, 3syl2an 585 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → Fun (𝐹𝐺))
543adant3 1155 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴) → Fun (𝐹𝐺))
6 fndm 6201 . . . . . . 7 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
76sseq2d 3830 . . . . . 6 (𝐹 Fn 𝐴 → (ran 𝐺 ⊆ dom 𝐹 ↔ ran 𝐺𝐴))
87biimpar 465 . . . . 5 ((𝐹 Fn 𝐴 ∧ ran 𝐺𝐴) → ran 𝐺 ⊆ dom 𝐹)
9 dmcosseq 5588 . . . . 5 (ran 𝐺 ⊆ dom 𝐹 → dom (𝐹𝐺) = dom 𝐺)
108, 9syl 17 . . . 4 ((𝐹 Fn 𝐴 ∧ ran 𝐺𝐴) → dom (𝐹𝐺) = dom 𝐺)
11103adant2 1154 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴) → dom (𝐹𝐺) = dom 𝐺)
12 fndm 6201 . . . 4 (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
13123ad2ant2 1157 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴) → dom 𝐺 = 𝐵)
1411, 13eqtrd 2840 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴) → dom (𝐹𝐺) = 𝐵)
15 df-fn 6104 . 2 ((𝐹𝐺) Fn 𝐵 ↔ (Fun (𝐹𝐺) ∧ dom (𝐹𝐺) = 𝐵))
165, 14, 15sylanbrc 574 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴) → (𝐹𝐺) Fn 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wss 3769  dom cdm 5311  ran crn 5312  ccom 5315  Fun wfun 6095   Fn wfn 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-opab 4907  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-fun 6103  df-fn 6104
This theorem is referenced by:  fco  6273  fnfco  6284  fipreima  8511  updjudhcoinlf  9041  updjudhcoinrg  9042  cshco  13806  swrdco  13807  isofn  16639  prdsinvlem  17729  prdsmgp  18812  pws1  18818  evlslem1  19723  frlmbas  20309  frlmup3  20349  frlmup4  20350  upxp  21640  uptx  21642  0vfval  27789  xppreima2  29777  psgnfzto1stlem  30175  sseqfv1  30776  sseqfn  30777  sseqfv2  30781  volsupnfl  33767  ftc1anclem5  33801  ftc1anclem8  33804  choicefi  39879  fourierdlem42  40845
  Copyright terms: Public domain W3C validator