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

Definition df-f1o 4990
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 4982 . 2 wff 𝐹:𝐴1-1-onto𝐵
51, 2, 3wf1 4980 . . 3 wff 𝐹:𝐴1-1𝐵
61, 2, 3wfo 4981 . . 3 wff 𝐹:𝐴onto𝐵
75, 6wa 102 . 2 wff (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵)
84, 7wb 103 1 wff (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
Colors of variables: wff set class
This definition is referenced by:  f1oeq1  5209  f1oeq2  5210  f1oeq3  5211  nff1o  5216  f1of1  5217  dff1o2  5223  dff1o5  5227  f1oco  5241  fo00  5254  dff1o6  5518  fcof1o  5531  tposf1o2  5991  cnref1o  9068
  Copyright terms: Public domain W3C validator