Definition df-f1o 4146

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4727, dff1o3 4728, dff1o4 4730, and dff1o5 4731. 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 4130	. 2 wff F:A-1-1-onto->B
5	1, 2, 3	wf1 4128	. . 3 wff F:A-1-1->B
6	1, 2, 3	wfo 4129	. . 3 wff F:A-onto->B
7	5, 6	wa 337	. 2 wff (F:A-1-1->B /\ F:A-onto->B)
8	4, 7	wb 219	1 wff (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))

This definition is referenced by:  f1oeq1 4718  f1oeq2 4719  f1oeq3 4720  hbf1o 4721  f1of1 4722  dff1o2 4727  dff1o5 4731  f1oco 4744  fo00 4755  dff1o6 4948  f1oweALT 4980  smoiso2 5280  unfilem2 5861  alephiso 6221  icoshftf1oii 7924  reeff1o 9089  1arith 9426  efif1o 10963  eff1oi 10971  unopf1o 12309  ghomf1olem 14374  dff1o6f 15128  trnij 15807  hartoglem 16207

Copyright terms: Public domain