Definition df-f1o 3204

Description: Define a one-to-one onto function. For equivalent definitions see f1o2 3700, f1o3 3701, f1o4 3703, and f1o5 3704. 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 3188	. 2 wff F:A-1-1-onto->B
5	1, 2, 3	wf1 3186	. . 3 wff F:A-1-1->B
6	1, 2, 3	wfo 3187	. . 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 3691  f1oeq2 3692  f1oeq3 3693  hbf1o 3694  f1of1 3695  f1o2 3700  f1o3 3701  f1o5 3704  f1oco 3714  fo00 3722  f1ofv 3884  f1oweALT 3913  unfilem2 4563  alephiso 4910  icoshftf1oi 6417  reeff1o 7433  efif1o 8740  eff1oi 8748  unopf1ot 9842  ghomf1olem 10399  trnij 10616

Copyright terms: Public domain