Definition df-f1o 5333

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 5325	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5323	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5324	. . 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  5571  f1oeq2  5572  f1oeq3  5573  nff1o  5581  f1of1  5582  dff1o2  5588  dff1o5  5592  f1oco  5606  fo00  5621  dff1o6  5916  fcof1o  5929  tposf1o2  6435  cnref1o  9884  1arith  12939  xpsff1o  13431  znf1o  14664  reeff1o  15496  ioocosf1o  15577  mpodvdsmulf1o  15713  gausslemma2dlem1f1o  15788