---

Step * 1 of Lemma mu-unique


1. f : ℕ ⟶ 𝔹
2. x : ℕ
3. ↑(f x)
4. ∀y:ℕx. (¬↑(f y))
5. ∀[f:ℕx + 1 ⟶ 𝔹]. ∀[x@0:ℕx + 1].  mu(f) = x@0 ∈ ℤ supposing (↑(f x@0)) ∧ (∀y:ℕx + 1. ((↑(f y)) ⇒ (y = x@0 ∈ ℤ)))
6. ↑(f x)
7. y : ℕx + 1@i
8. ↑(f y)@i
⊢ y = x ∈ ℤ
BY
{ (SupposeNot THEN InstHyp [⌜y⌝] 4⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  x  :  \mBbbN{}
3.  \muparrow{}(f  x)
4.  \mforall{}y:\mBbbN{}x.  (\mneg{}\muparrow{}(f  y))
5.  \mforall{}[f:\mBbbN{}x  +  1  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x@0:\mBbbN{}x  +  1].
          mu(f)  =  x@0  supposing  (\muparrow{}(f  x@0))  \mwedge{}  (\mforall{}y:\mBbbN{}x  +  1.  ((\muparrow{}(f  y))  {}\mRightarrow{}  (y  =  x@0)))
6.  \muparrow{}(f  x)
7.  y  :  \mBbbN{}x  +  1@i
8.  \muparrow{}(f  y)@i
\mvdash{}  y  =  x


By

---

Latex:
(SupposeNot  THEN  InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  4\mcdot{}  THEN  Auto)

---

Home Index