Definition df-f1o 5265

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 5257	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5255	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5256	. . 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  5492  f1oeq2  5493  f1oeq3  5494  nff1o  5502  f1of1  5503  dff1o2  5509  dff1o5  5513  f1oco  5527  fo00  5540  dff1o6  5823  fcof1o  5836  tposf1o2  6328  cnref1o  9725  1arith  12536  xpsff1o  12992  znf1o  14207  reeff1o  15009  ioocosf1o  15090  mpodvdsmulf1o  15226  gausslemma2dlem1f1o  15301