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

Definition df-f1o 4022
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4634, dff1o3 4635, dff1o4 4637, and dff1o5 4638. 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 4006 . 2 wff F:A-1-1-onto->B
51, 2, 3wf1 4004 . . 3 wff F:A-1-1->B
61, 2, 3wfo 4005 . . 3 wff F:A-onto->B
75, 6wa 361 . 2 wff (F:A-1-1->B /\ F:A-onto->B)
84, 7wb 174 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 4623  f1oeq2 4624  f1oeq3 4625  hbf1o 4627  f1of1 4628  dff1o2 4634  dff1o5 4638  f1oco 4652  fo00 4662  dff1o6 4887  f1oweALT 4921  smoiso2 5325  f1finf1o 5918  unfilem2 5943  fofinf1o 5960  alephiso 6345  cnref1o 8146  icoshftf1oii 8363  1arith 9866  reeff1o 12642  recosf1o 12703  efif1olem3 12710  unopf1o 13958  ghomf1olem 14574  dff1o6f 15712  trnij 16319
Copyright terms: Public domain