MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-f1o Structured version   Unicode version

Definition df-f1o 5464
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5682, dff1o3 5683, dff1o4 5685, and dff1o5 5686. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f1o  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )

Detailed syntax breakdown of Definition df-f1o
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3wf1o 5456 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 5454 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 5455 . . 3  wff  F : A -onto-> B
75, 6wa 360 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 178 1  wff  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
Colors of variables: wff set class
This definition is referenced by:  f1oeq1  5668  f1oeq2  5669  f1oeq3  5670  nff1o  5675  f1of1  5676  dff1o2  5682  dff1o5  5686  f1oco  5701  fo00  5714  dff1o6  6016  fcof1o  6029  soisoi  6051  f1oweALT  6077  tposf1o2  6508  smoiso2  6634  f1finf1o  7338  unfilem2  7375  fofinf1o  7390  alephiso  7984  cnref1o  10612  1arith  13300  xpsff1o  13798  isffth2  14118  ffthf1o  14121  orbsta  15095  odf1o1  15211  znf1o  16837  cygznlem3  16855  reeff1o  20368  recosf1o  20442  efif1olem4  20452  dvdsmulf1o  20984  eupatrl  21695  unopf1o  23424  nvof1o  24045  ghomf1olem  25110  frgrancvvdeqlem8  28503
  Copyright terms: Public domain W3C validator