Definition df-f1o 3192

Description: Define a one-to-one onto function. For equivalent definitions see f1o2 3684, f1o3 3685, f1o4 3687, and f1o5 3688. 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 3176	. 2 wff F:A-1-1-onto->B
5	1, 2, 3	wf1 3174	. . 3 wff F:A-1-1->B
6	1, 2, 3	wfo 3175	. . 3 wff F:A-onto->B
7	5, 6	wa 223	. 2 wff (F:A-1-1->B /\ F:A-onto->B)
8	4, 7	wb 146	1 wff (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))

This definition is referenced by:  f1oeq1 3675  f1oeq2 3676  f1oeq3 3677  hbf1o 3678  f1of1 3679  f1o2 3684  f1o3 3685  f1o5 3688  f1oco 3698  fo00 3706  f1ofv 3868  f1oweALT 3897  unfilem2 4531  alephiso 4872  icoshftf1oi 6350  reeff1o 7376  efif1o 8672  eff1oi 8685  unopf1ot 9779  ghomf1olem 10330  trnij 10517

Copyright terms: Public domain