---

Step * 2 1 2 of Lemma sp-meet_wf


1. f : Base
2. f1 : Base
3. f = f1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
4. f ∈ ℕ ⟶ 𝔹
5. f1 ∈ ℕ ⟶ 𝔹
6. g : Base
7. g1 : Base
8. g = g1 ∈ (f,g:ℕ ⟶ 𝔹//(f = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ g = ⊥ ∈ (ℕ ⟶ 𝔹)))
9. g ∈ ℕ ⟶ 𝔹
10. g1 ∈ ℕ ⟶ 𝔹
11. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇒ (g1 = ⊥ ∈ (ℕ ⟶ 𝔹))
12. (g = ⊥ ∈ (ℕ ⟶ 𝔹)) ⇐ g1 = ⊥ ∈ (ℕ ⟶ 𝔹)
13. ∀n:ℕ. (¬↑let x,y = coded-pair(n) in (f1 x) ∧b (g1 y))
14. i : ℕ
15. j : ℕ
16. ↑((f i) ∧b (g j))
17. f1 = ⊥ ∈ (ℕ ⟶ 𝔹)
18. f = ⊥ ∈ (ℕ ⟶ 𝔹)
19. f1 = ⊥ ∈ (ℕ ⟶ 𝔹)
⊢ False
BY
{ ((RWO "equal-Sierpinski-bottom" (-2) THENA Auto) THEN InstHyp [⌜i⌝] (-2)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Base
2.  f1  :  Base
3.  f  =  f1
4.  f  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
5.  f1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
6.  g  :  Base
7.  g1  :  Base
8.  g  =  g1
9.  g  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
10.  g1  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
11.  (g  =  \mbot{})  {}\mRightarrow{}  (g1  =  \mbot{})
12.  (g  =  \mbot{})  \mLeftarrow{}{}  g1  =  \mbot{}
13.  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}let  x,y  =  coded-pair(n)  in  (f1  x)  \mwedge{}\msubb{}  (g1  y))
14.  i  :  \mBbbN{}
15.  j  :  \mBbbN{}
16.  \muparrow{}((f  i)  \mwedge{}\msubb{}  (g  j))
17.  f1  =  \mbot{}
18.  f  =  \mbot{}
19.  f1  =  \mbot{}
\mvdash{}  False


By

---

Latex:
((RWO  "equal-Sierpinski-bottom"  (-2)  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)

---

Home Index