Definition df-f1o 5266

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 5258	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5256	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5257	. . 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  5495  f1oeq2  5496  f1oeq3  5497  nff1o  5505  f1of1  5506  dff1o2  5512  dff1o5  5516  f1oco  5530  fo00  5543  dff1o6  5826  fcof1o  5839  tposf1o2  6337  cnref1o  9742  1arith  12561  xpsff1o  13051  znf1o  14283  reeff1o  15093  ioocosf1o  15174  mpodvdsmulf1o  15310  gausslemma2dlem1f1o  15385