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

Definition df-f1o 4031
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4643, dff1o3 4644, dff1o4 4646, and dff1o5 4647. 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 4015 . 2 wff F:A-1-1-onto->B
51, 2, 3wf1 4013 . . 3 wff F:A-1-1->B
61, 2, 3wfo 4014 . . 3 wff F:A-onto->B
75, 6wa 377 . 2 wff (F:A-1-1->B /\ F:A-onto->B)
84, 7wb 184 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 4632  f1oeq2 4633  f1oeq3 4634  hbf1o 4636  f1of1 4637  dff1o2 4643  dff1o5 4647  f1oco 4661  fo00 4671  dff1o6 4896  f1oweALT 4930  smoiso2 5332  f1finf1o 5925  unfilem2 5950  fofinf1o 5967  alephiso 6362  cnref1o 8151  icoshftf1oii 8367  1arith 9814  reeff1o 12541  recosf1o 12602  efif1olem3 12609  unopf1o 13761  ghomf1olem 14377  dff1o6f 15521  trnij 16134
Copyright terms: Public domain