---

Step * 2 of Lemma injection-is-surjection


1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. ¬(∃i:ℕn. ∀a:ℕn. (¬((f a) = i ∈ ℕn)))
⊢ Surj(ℕn;ℕn;f)
BY
{ (Unfold `surject` 0
   THEN Auto
   THEN SupposeNot
   THEN D 4
   THEN InstConcl [⌜b⌝]⋅
   THEN Auto
   THEN ParallelOp -2
   THEN InstConcl [⌜a⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  Inj(\mBbbN{}n;\mBbbN{}n;f)
4.  \mneg{}(\mexists{}i:\mBbbN{}n.  \mforall{}a:\mBbbN{}n.  (\mneg{}((f  a)  =  i)))
\mvdash{}  Surj(\mBbbN{}n;\mBbbN{}n;f)


By

---

Latex:
(Unfold  `surject`  0
  THEN  Auto
  THEN  SupposeNot
  THEN  D  4
  THEN  InstConcl  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ParallelOp  -2
  THEN  InstConcl  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index