HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-f1o 4283
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5002, dff1o3 5003, dff1o4 5005, and dff1o5 5006. 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 4267 . 2  wff  F : A
-1-1-onto-> B
51, 2, 3wf1 4265 . . 3  wff  F : A -1-1-> B
61, 2, 3wfo 4266 . . 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  4991  f1oeq2  4992  f1oeq3  4993  hbf1o  4995  f1of1  4996  dff1o2  5002  dff1o5  5006  f1oco  5020  fo00  5033  dff1o6  5302  fcof1o  5316  soisoi  5329  f1oweALT  5353  tposf1o2  5743  smoiso2  5841  f1finf1o  6569  unfilem2  6605  fofinf1o  6620  alephiso  7207  cnref1o  9718  1arith  12079  xpsff1o  12554  orbsta  13476  odf1o1  13592  znf1o  15212  cygznlem3  15229  reeff1o  18411  recosf1o  18481  efif1olem4  18490  dvdsmulf1o  18988  unopf1o  21029  ghomf1olem  21877  dff1o6f  22907  trnij  23438
Copyright terms: Public domain