Definition df-f1o 5066

Description: Define a one-to-one onto function. 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 5058	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5056	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5057	. . 3 wff F : A -onto-> B
7	5, 6	wa 103	. 2 wff ( F : A -1-1-> B /\ F : A -onto-> B )
8	4, 7	wb 104	1 wff ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

This definition is referenced by:  f1oeq1  5292  f1oeq2  5293  f1oeq3  5294  nff1o  5299  f1of1  5300  dff1o2  5306  dff1o5  5310  f1oco  5324  fo00  5337  dff1o6  5609  fcof1o  5622  tposf1o2  6097  cnref1o  9290