MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1oco Unicode version

Theorem f1oco 5639
Description: Composition of one-to-one onto functions. (Contributed by NM, 19-Mar-1998.)
Assertion
Ref Expression
f1oco  |-  ( ( F : B -1-1-onto-> C  /\  G : A -1-1-onto-> B )  ->  ( F  o.  G ) : A -1-1-onto-> C )

Proof of Theorem f1oco
StepHypRef Expression
1 df-f1o 5402 . . 3  |-  ( F : B -1-1-onto-> C  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) )
2 df-f1o 5402 . . 3  |-  ( G : A -1-1-onto-> B  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) )
3 f1co 5589 . . . . 5  |-  ( ( F : B -1-1-> C  /\  G : A -1-1-> B
)  ->  ( F  o.  G ) : A -1-1-> C )
4 foco 5604 . . . . 5  |-  ( ( F : B -onto-> C  /\  G : A -onto-> B
)  ->  ( F  o.  G ) : A -onto-> C )
53, 4anim12i 550 . . . 4  |-  ( ( ( F : B -1-1-> C  /\  G : A -1-1-> B )  /\  ( F : B -onto-> C  /\  G : A -onto-> B ) )  ->  ( ( F  o.  G ) : A -1-1-> C  /\  ( F  o.  G ) : A -onto-> C ) )
65an4s 800 . . 3  |-  ( ( ( F : B -1-1-> C  /\  F : B -onto-> C )  /\  ( G : A -1-1-> B  /\  G : A -onto-> B ) )  ->  ( ( F  o.  G ) : A -1-1-> C  /\  ( F  o.  G ) : A -onto-> C ) )
71, 2, 6syl2anb 466 . 2  |-  ( ( F : B -1-1-onto-> C  /\  G : A -1-1-onto-> B )  ->  (
( F  o.  G
) : A -1-1-> C  /\  ( F  o.  G
) : A -onto-> C
) )
8 df-f1o 5402 . 2  |-  ( ( F  o.  G ) : A -1-1-onto-> C  <->  ( ( F  o.  G ) : A -1-1-> C  /\  ( F  o.  G ) : A -onto-> C ) )
97, 8sylibr 204 1  |-  ( ( F : B -1-1-onto-> C  /\  G : A -1-1-onto-> B )  ->  ( F  o.  G ) : A -1-1-onto-> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    o. ccom 4823   -1-1->wf1 5392   -onto->wfo 5393   -1-1-onto->wf1o 5394
This theorem is referenced by:  fveqf1o  5969  isotr  5996  ener  7091  omf1o  7148  oef1o  7589  cnfcom3  7595  infxpenc  7833  ackbij2lem2  8054  canthp1lem2  8462  pwfseqlem5  8472  hashfacen  11631  summolem3  12436  fsumf1o  12445  ackbijnn  12535  eulerthlem2  13099  symgcl  15029  gsumval3eu  15441  gsumval3  15442  resinf1o  20306  counop  23273  derangenlem  24637  subfacp1lem5  24650  prodmolem3  25039  fprodf1o  25052  rngoisoco  26290  enfixsn  26927  pmtrfconj  27077  lautco  30212
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pr 4345
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-br 4155  df-opab 4209  df-id 4440  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402
  Copyright terms: Public domain W3C validator