ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-f1o GIF version

Definition df-f1o 5190
Description: Define a one-to-one onto function. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f1o (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))

Detailed syntax breakdown of Definition df-f1o
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wf1o 5182 . 2 wff 𝐹:𝐴1-1-onto𝐵
51, 2, 3wf1 5180 . . 3 wff 𝐹:𝐴1-1𝐵
61, 2, 3wfo 5181 . . 3 wff 𝐹:𝐴onto𝐵
75, 6wa 103 . 2 wff (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵)
84, 7wb 104 1 wff (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
Colors of variables: wff set class
This definition is referenced by:  f1oeq1  5416  f1oeq2  5417  f1oeq3  5418  nff1o  5425  f1of1  5426  dff1o2  5432  dff1o5  5436  f1oco  5450  fo00  5463  dff1o6  5739  fcof1o  5752  tposf1o2  6230  cnref1o  9580  1arith  12286  reeff1o  13261  ioocosf1o  13342
  Copyright terms: Public domain W3C validator