Definition df-f1o 5387

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 5379	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5377	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5378	. . 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 used by:  f1oeq1  5630  f1oeq2  5631  f1oeq3  5632  nff1o  5640  f1of1  5641  dff1o2  5647  dff1o5  5651  f1oco  5665  fo00  5680  dff1o6  5985  fcof1o  5998  tposf1o2  6546  cnref1o  10067  1arith  13174  xpsff1o  13728  znf1o  15094  reeff1o  16016  ioocosf1o  16099  mpodvdsmulf1o  16301  gausslemma2dlem1f1o  16401