Definition df-f1o 5364

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 5356	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5354	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5355	. . 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  5607  f1oeq2  5608  f1oeq3  5609  nff1o  5617  f1of1  5618  dff1o2  5624  dff1o5  5628  f1oco  5642  fo00  5657  dff1o6  5955  fcof1o  5968  tposf1o2  6514  cnref1o  10001  1arith  13090  xpsff1o  13613  znf1o  14925  reeff1o  15764  ioocosf1o  15845  mpodvdsmulf1o  15984  gausslemma2dlem1f1o  16059