Definition df-f1o 5278

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 5270	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5268	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5269	. . 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  5510  f1oeq2  5511  f1oeq3  5512  nff1o  5520  f1of1  5521  dff1o2  5527  dff1o5  5531  f1oco  5545  fo00  5558  dff1o6  5845  fcof1o  5858  tposf1o2  6356  cnref1o  9772  1arith  12690  xpsff1o  13181  znf1o  14413  reeff1o  15245  ioocosf1o  15326  mpodvdsmulf1o  15462  gausslemma2dlem1f1o  15537