Definition df-f1o 5325

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 5317	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5315	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5316	. . 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  5560  f1oeq2  5561  f1oeq3  5562  nff1o  5570  f1of1  5571  dff1o2  5577  dff1o5  5581  f1oco  5595  fo00  5609  dff1o6  5900  fcof1o  5913  tposf1o2  6416  cnref1o  9846  1arith  12890  xpsff1o  13382  znf1o  14615  reeff1o  15447  ioocosf1o  15528  mpodvdsmulf1o  15664  gausslemma2dlem1f1o  15739