Definition df-f1o 5382

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 5374	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5372	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5373	. . 3 wff F : A -onto-> B
7	5, 6	wa 104	. 2 wff ( F : A -1-1-> B /\ F : A -onto-> B )
8	4, 7	wb 105	1 wff ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

This definition is referenced by:  f1oeq1  5625  f1oeq2  5626  f1oeq3  5627  nff1o  5635  f1of1  5636  dff1o2  5642  dff1o5  5646  f1oco  5660  fo00  5675  dff1o6  5975  fcof1o  5988  tposf1o2  6534  cnref1o  10033  1arith  13127  xpsff1o  13650  znf1o  14961  reeff1o  15800  ioocosf1o  15881  mpodvdsmulf1o  16021  gausslemma2dlem1f1o  16096