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

Definition df-f1o 4035
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4647, dff1o3 4648, dff1o4 4650, and dff1o5 4651. 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 4019 . 2 wff F:A-1-1-onto->B
51, 2, 3wf1 4017 . . 3 wff F:A-1-1->B
61, 2, 3wfo 4018 . . 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 4636  f1oeq2 4637  f1oeq3 4638  hbf1o 4640  f1of1 4641  dff1o2 4647  dff1o5 4651  f1oco 4665  fo00 4675  dff1o6 4900  f1oweALT 4934  smoiso2 5335  f1finf1o 5928  unfilem2 5953  alephiso 6363  cnref1o 8151  icoshftf1oii 8365  1arith 9792  reeff1o 12378  recosf1o 12439  efif1olem3 12446  unopf1o 13564  ghomf1olem 14180  dff1o6f 15324  trnij 15937
Copyright terms: Public domain