Definition df-f1o 3197

Description: Define a one-to-one onto function. For equivalent definitions see f1o2 3693, f1o3 3694, f1o4 3696, and f1o5 3697. 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 3181	. 2 wff F:A-1-1-onto->B
5	1, 2, 3	wf1 3179	. . 3 wff F:A-1-1->B
6	1, 2, 3	wfo 3180	. . 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 3684  f1oeq2 3685  f1oeq3 3686  hbf1o 3687  f1of1 3688  f1o2 3693  f1o3 3694  f1o5 3697  f1oco 3707  fo00 3715  f1ofv 3877  f1oweALT 3906  unfilem2 4549  alephiso 4892  icoshftf1oi 6409  reeff1o 7426  efif1o 8738  eff1oi 8746  unopf1ot 9840  ghomf1olem 10396  trnij 10637

Copyright terms: Public domain