HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-f1o 4027
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4637, dff1o3 4638, dff1o4 4640, and dff1o5 4641. 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
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class F
41, 2, 3wf1o 4011 . 2 wff F:A-1-1-onto->B
51, 2, 3wf1 4009 . . 3 wff F:A-1-1->B
61, 2, 3wfo 4010 . . 3 wff F:A-onto->B
75, 6wa 382 . 2 wff (F:A-1-1->B /\ F:A-onto->B)
84, 7wb 189 1 wff (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
Colors of variables: wff set class
This definition is referenced by:  f1oeq1 4626  f1oeq2 4627  f1oeq3 4628  hbf1o 4630  f1of1 4631  dff1o2 4637  dff1o5 4641  f1oco 4655  fo00 4665  dff1o6 4889  f1oweALT 4923  smoiso2 5296  f1finf1o 5889  unfilem2 5914  alephiso 6324  cnref1o 8103  icoshftf1oii 8316  reeff1o 9360  1arith 9751  recosf1o 11881  efif1olem3 11887  unopf1o 12953  ghomf1olem 13777  dff1o6f 14924  trnij 15540
Copyright terms: Public domain