Definition df-f1o 5420

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5638, dff1o3 5639, dff1o4 5641, and dff1o5 5642. 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf1o 5412	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5410	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5411	. . 3 wff F : A -onto-> B
7	5, 6	wa 359	. 2 wff ( F : A -1-1-> B /\ F : A -onto-> B )
8	4, 7	wb 177	1 wff ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

This definition is referenced by:  f1oeq1  5624  f1oeq2  5625  f1oeq3  5626  nff1o  5631  f1of1  5632  dff1o2  5638  dff1o5  5642  f1oco  5657  fo00  5670  dff1o6  5972  fcof1o  5985  soisoi  6007  f1oweALT  6033  tposf1o2  6464  smoiso2  6590  f1finf1o  7294  unfilem2  7331  fofinf1o  7346  alephiso  7935  cnref1o  10563  1arith  13250  xpsff1o  13748  isffth2  14068  ffthf1o  14071  orbsta  15045  odf1o1  15161  znf1o  16787  cygznlem3  16805  reeff1o  20316  recosf1o  20390  efif1olem4  20400  dvdsmulf1o  20932  eupatrl  21643  unopf1o  23372  nvof1o  23993  ghomf1olem  25058  frgrancvvdeqlem8  28143