---

Step * 1 1 of Lemma weak-continuity-rel-fun


1. P : (ℕ ⟶ ℕ) ⟶ ℙ
2. ∀f:ℕ ⟶ ℕ. ⇃(P f)
3. f : ℕ ⟶ ℕ
4. f1 : ℕ ⟶ ℕ
⊢ ⇃(∃n:ℕ. (P f1))
BY
{ ((InstHyp [⌜f1⌝] (-3)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN BLemma `implies-quotient-true`
   THEN Auto
   THEN InstConcl [⌜0⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  P  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(P  f)
3.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
4.  f1  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  \00D9(\mexists{}n:\mBbbN{}.  (P  f1))


By

---

Latex:
((InstHyp  [\mkleeneopen{}f1\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  BLemma  `implies-quotient-true`
  THEN  Auto
  THEN  InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index