Definition df-f1o 5361

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 5353	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5351	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5352	. . 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  5604  f1oeq2  5605  f1oeq3  5606  nff1o  5614  f1of1  5615  dff1o2  5621  dff1o5  5625  f1oco  5639  fo00  5654  dff1o6  5951  fcof1o  5964  tposf1o2  6503  cnref1o  9986  1arith  13069  xpsff1o  13579  znf1o  14816  reeff1o  15655  ioocosf1o  15736  mpodvdsmulf1o  15875  gausslemma2dlem1f1o  15950