Definition df-f1o 3278

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 3801, dff1o3 3802, dff1o4 3804, and dff1o5 3805. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow).

Assertion

Ref	Expression
df-f1o	|- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))

Detailed syntax breakdown of Definition df-f1o

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf1o 3262	. 2 wff F:A-1-1-onto->B
5	1, 2, 3	wf1 3260	. . 3 wff F:A-1-1->B
6	1, 2, 3	wfo 3261	. . 3 wff F:A-onto->B
7	5, 6	wa 221	. 2 wff (F:A-1-1->B /\ F:A-onto->B)
8	4, 7	wb 144	1 wff (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))

This definition is referenced by:  f1oeq1 3792  f1oeq2 3793  f1oeq3 3794  hbf1o 3795  f1of1 3796  dff1o2 3801  dff1o3 3802  dff1o5 3805  f1oco 3818  fo00 3826  dff1o6 3991  f1oweALT 4020  unfilem2 4695  alephiso 5042  icoshftf1oii 6536  reeff1o 7634  efif1o 9010  eff1oi 9018  unopf1o 10120  ghomf1olem 10681  trnij 11160  hartoglem 11435

Copyright terms: Public domain