Definition df-f1o 5287

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	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

Detailed syntax breakdown of Definition df-f1o

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf1o 5279	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5277	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5278	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 104	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 105	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  5522  f1oeq2  5523  f1oeq3  5524  nff1o  5532  f1of1  5533  dff1o2  5539  dff1o5  5543  f1oco  5557  fo00  5571  dff1o6  5858  fcof1o  5871  tposf1o2  6369  cnref1o  9792  1arith  12765  xpsff1o  13256  znf1o  14488  reeff1o  15320  ioocosf1o  15401  mpodvdsmulf1o  15537  gausslemma2dlem1f1o  15612