---

Step * of Lemma not_base_enumerable3

(f:  Base. Surj(;Base;f))
BY
{ ((D (0) THEN Auto)
   THEN InstLemma `surject_implies_decidble_eq2` [Base]
   THEN Auto
   THEN InstLemma `not_base_decidble_eq_diag2` []
   THEN Auto) }


\mneg{}(\mexists{}f:\mBbbN{}  {}\mrightarrow{}  Base.  Surj(\mBbbN{};Base;f))


By

((D  (0)  THEN  Auto)
  THEN  InstLemma  `surject\_implies\_decidble\_eq2`  [\mkleeneopen{}Base\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstLemma  `not\_base\_decidble\_eq\_diag2`  []\mcdot{}
  THEN  Auto)



Home Index