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

Definition df-f1o 5130
 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 5122 . 2 wff 𝐹:𝐴1-1-onto𝐵
51, 2, 3wf1 5120 . . 3 wff 𝐹:𝐴1-1𝐵
61, 2, 3wfo 5121 . . 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  5356  f1oeq2  5357  f1oeq3  5358  nff1o  5365  f1of1  5366  dff1o2  5372  dff1o5  5376  f1oco  5390  fo00  5403  dff1o6  5677  fcof1o  5690  tposf1o2  6167  cnref1o  9452  reeff1o  12877  ioocosf1o  12957
 Copyright terms: Public domain W3C validator