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

Definition df-f1o 4293
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5012, dff1o3 5013, dff1o4 5015, and dff1o5 5016. 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 4277 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4275 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4276 . . 3  wff  F : A -onto-> B
75, 6wa 356 . 2  wff  ( F : A -1-1-> B  /\  F : A -onto-> B )
84, 7wb 174 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  5001  f1oeq2  5002  f1oeq3  5003  hbf1o  5005  f1of1  5006  dff1o2  5012  dff1o5  5016  f1oco  5030  fo00  5043  dff1o6  5312  fcof1o  5326  soisoi  5339  f1oweALT  5363  tposf1o2  5753  smoiso2  5851  f1finf1o  6579  unfilem2  6615  fofinf1o  6630  alephiso  7217  cnref1o  9737  1arith  12099  xpsff1o  12575  orbsta  13497  odf1o1  13613  znf1o  15233  cygznlem3  15250  reeff1o  18432  recosf1o  18502  efif1olem4  18511  dvdsmulf1o  19009  unopf1o  21052  ghomf1olem  21898  dff1o6f  22929  trnij  23460
  Copyright terms: Public domain W3C validator