Definition df-f1o 5297

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 5289	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5287	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5288	. . 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  5532  f1oeq2  5533  f1oeq3  5534  nff1o  5542  f1of1  5543  dff1o2  5549  dff1o5  5553  f1oco  5567  fo00  5581  dff1o6  5868  fcof1o  5881  tposf1o2  6379  cnref1o  9807  1arith  12805  xpsff1o  13296  znf1o  14528  reeff1o  15360  ioocosf1o  15441  mpodvdsmulf1o  15577  gausslemma2dlem1f1o  15652