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

Definition df-f1o 4164
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 4778, dff1o3 4779, dff1o4 4781, and dff1o5 4782. 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 4148 . 2 wff F:A-1-1-onto->B
51, 2, 3wf1 4146 . . 3 wff F:A-1-1->B
61, 2, 3wfo 4147 . . 3 wff F:A-onto->B
75, 6wa 418 . 2 wff (F:A-1-1->B /\ F:A-onto->B)
84, 7wb 209 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 4767  f1oeq2 4768  f1oeq3 4769  hbf1o 4771  f1of1 4772  dff1o2 4778  dff1o5 4782  f1oco 4796  fo00 4806  dff1o6 5033  f1oweALT 5066  smoiso2 5436  f1finf1o 6006  unfilem2 6032  alephiso 6471  cnref1o 8247  icoshftf1oii 8462  reeff1o 9633  1arith 9958  efif1o 11618  eff1oi 11626  unopf1o 12950  ghomf1olem 13896  dff1o6f 14899  trnij 15540
Copyright terms: Public domain