---

Step * 1 1 2 1 of Lemma notAC20


1. T : Type@i'
2. ⇃(T)@i
3. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T ⟶ ℙ
     ((∀n:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃m:T. (P n m))) ⇒ ⇃(∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n (f n))))@i'
4. P : ((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ@i'
5. ∀t:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(P t)@i
6. ⇃(∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n))
⊢ ⇃(∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (P t))
BY
{ ((Assert ⌜(∃f:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ T. ∀n:(ℕ ⟶ ℕ) ⟶ ℕ. (P n)) ⇒ (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (P t))⌝⋅
   THENM (RenameVar `f' (-1) THEN RenameVar `M' (-2) THEN UseWitness ⌜f M⌝⋅ THEN (newQuotientElim1 (-2)⋅ THEN Auto))
   )
   THEN (D 0 THENA Auto)
   THEN ExRepD
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  \00D9(T)@i
3.  \mforall{}P:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}m:T.  (P  n  m)))
          {}\mRightarrow{}  \00D9(\mexists{}f:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T.  \mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (P  n  (f  n))))@i'
4.  P  :  ((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}@i'
5.  \mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \00D9(P  t)@i
6.  \00D9(\mexists{}f:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T.  \mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (P  n))
\mvdash{}  \00D9(\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (P  t))


By

---

Latex:
((Assert  \mkleeneopen{}(\mexists{}f:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  T.  \mforall{}n:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (P  n))  {}\mRightarrow{}  (\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (P  t))\mkleeneclose{}\mcdot{}
  THENM  (RenameVar  `f'  (-1)
                THEN  RenameVar  `M'  (-2)
                THEN  UseWitness  \mkleeneopen{}f  M\mkleeneclose{}\mcdot{}
                THEN  (newQuotientElim1  (-2)\mcdot{}  THEN  Auto))
  )
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD
  THEN  Auto)

---

Home Index