---

Step * 1 1 1 2 1 1 1 of Lemma sp-lub-is-bottom


1. n : ℕ
2. EquivRel(ℕ ⟶ ℕ ⟶ 𝔹;f,g.fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))
3. B : Base
4. B1 : Base
5. B = B1 ∈ (f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g))
6. B ∈ ℕ ⟶ ℕ ⟶ 𝔹
7. B1 ∈ ℕ ⟶ ℕ ⟶ 𝔹
8. fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);B;B1)
9. B ∈ f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)
10. n1 : ℕ
⊢ B n1 ∈ ℕ ⟶ 𝔹
BY
{ (Thin (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  EquivRel(\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{};f,g.fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g))
3.  B  :  Base
4.  B1  :  Base
5.  B  =  B1
6.  B  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
7.  B1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
8.  fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};B;B1)
9.  B  \mmember{}  f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}//fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g)
10.  n1  :  \mBbbN{}
\mvdash{}  B  n1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}


By

---

Latex:
(Thin  (-2)  THEN  Auto)

---

Home Index