Proof of Nuprl Lemma : increasing

Step * 2 2 of Lemma increasing_split

1. m : ℤ
2. [%1] : 0 < m
3. ∀[P:ℕm - 1 ⟶ ℙ]
     ((∀i:ℕm - 1. Dec(P i))
     ⇒ (∃n,k:ℕ
          ∃f:ℕn ⟶ ℕm - 1
           ∃g:ℕk ⟶ ℕm - 1
            (increasing(f;n)
            ∧ increasing(g;k)
            ∧ (∀i:ℕn. (P (f i)))
            ∧ (∀j:ℕk. (¬(P (g j))))

            ∧ (∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))

4. [P] : ℕm ⟶ ℙ
5. ∀i:ℕm. Dec(P i)
6. ∃n,k:ℕ
    ∃f:ℕn ⟶ ℕm - 1
     ∃g:ℕk ⟶ ℕm - 1
      (increasing(f;n)
      ∧ increasing(g;k)
      ∧ (∀i:ℕn. (P (f i)))
      ∧ (∀j:ℕk. (¬(P (g j))))

      ∧ (∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))

⊢ ∃n,k:ℕ
   ∃f:ℕn ⟶ ℕm
    ∃g:ℕk ⟶ ℕm
     (increasing(f;n)
     ∧ increasing(g;k)
     ∧ (∀i:ℕn. (P (f i)))
     ∧ (∀j:ℕk. (¬(P (g j))))
     ∧ (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))
BY
{ (((InstHyp [m - 1] (-2) THENA Auto') THEN D (-1)) THEN ExRepD) }

1
1. m : ℤ
2. [%1] : 0 < m
3. ∀[P:ℕm - 1 ⟶ ℙ]
     ((∀i:ℕm - 1. Dec(P i))
     ⇒ (∃n,k:ℕ
          ∃f:ℕn ⟶ ℕm - 1
           ∃g:ℕk ⟶ ℕm - 1
            (increasing(f;n)
            ∧ increasing(g;k)
            ∧ (∀i:ℕn. (P (f i)))
            ∧ (∀j:ℕk. (¬(P (g j))))

            ∧ (∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))

4. [P] : ℕm ⟶ ℙ
5. ∀i:ℕm. Dec(P i)
6. n : ℕ
7. k : ℕ
8. f : ℕn ⟶ ℕm - 1
9. g : ℕk ⟶ ℕm - 1
10. increasing(f;n)
11. increasing(g;k)
12. ∀i:ℕn. (P (f i))
13. ∀j:ℕk. (¬(P (g j)))
14. ∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))
15. P (m - 1)
⊢ ∃n,k:ℕ
   ∃f:ℕn ⟶ ℕm
    ∃g:ℕk ⟶ ℕm
     (increasing(f;n)
     ∧ increasing(g;k)
     ∧ (∀i:ℕn. (P (f i)))
     ∧ (∀j:ℕk. (¬(P (g j))))
     ∧ (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))

2
1. m : ℤ
2. [%1] : 0 < m
3. ∀[P:ℕm - 1 ⟶ ℙ]
     ((∀i:ℕm - 1. Dec(P i))
     ⇒ (∃n,k:ℕ
          ∃f:ℕn ⟶ ℕm - 1
           ∃g:ℕk ⟶ ℕm - 1
            (increasing(f;n)
            ∧ increasing(g;k)
            ∧ (∀i:ℕn. (P (f i)))
            ∧ (∀j:ℕk. (¬(P (g j))))

            ∧ (∀i:ℕm - 1. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))

Latex:

Latex:
1. m : \mBbbZ{} 2. [\%1] : 0 < m 3. \mforall{}[P:\mBbbN{}m - 1 {}\mrightarrow{} \mBbbP{}] ((\mforall{}i:\mBbbN{}m - 1. Dec(P i)) {}\mRightarrow{} (\mexists{}n,k:\mBbbN{} \mexists{}f:\mBbbN{}n {}\mrightarrow{} \mBbbN{}m - 1 \mexists{}g:\mBbbN{}k {}\mrightarrow{} \mBbbN{}m - 1 (increasing(f;n) \mwedge{} increasing(g;k) \mwedge{} (\mforall{}i:\mBbbN{}n. (P (f i))) \mwedge{} (\mforall{}j:\mBbbN{}k. (\mneg{}(P (g j)))) \mwedge{} (\mforall{}i:\mBbbN{}m - 1. ((\mexists{}j:\mBbbN{}n. (i = (f j))) \mvee{} (\mexists{}j:\mBbbN{}k. (i = (g j)))))))) 4. [P] : \mBbbN{}m {}\mrightarrow{} \mBbbP{} 5. \mforall{}i:\mBbbN{}m. Dec(P i) 6. \mexists{}n,k:\mBbbN{} \mexists{}f:\mBbbN{}n {}\mrightarrow{} \mBbbN{}m - 1 \mexists{}g:\mBbbN{}k {}\mrightarrow{} \mBbbN{}m - 1 (increasing(f;n) \mwedge{} increasing(g;k) \mwedge{} (\mforall{}i:\mBbbN{}n. (P (f i))) \mwedge{} (\mforall{}j:\mBbbN{}k. (\mneg{}(P (g j)))) \mwedge{} (\mforall{}i:\mBbbN{}m - 1. ((\mexists{}j:\mBbbN{}n. (i = (f j))) \mvee{} (\mexists{}j:\mBbbN{}k. (i = (g j)))))) \mvdash{} \mexists{}n,k:\mBbbN{} \mexists{}f:\mBbbN{}n {}\mrightarrow{} \mBbbN{}m \mexists{}g:\mBbbN{}k {}\mrightarrow{} \mBbbN{}m (increasing(f;n) \mwedge{} increasing(g;k) \mwedge{} (\mforall{}i:\mBbbN{}n. (P (f i))) \mwedge{} (\mforall{}j:\mBbbN{}k. (\mneg{}(P (g j)))) \mwedge{} (\mforall{}i:\mBbbN{}m. ((\mexists{}j:\mBbbN{}n. (i = (f j))) \mvee{} (\mexists{}j:\mBbbN{}k. (i = (g j)))))) By Latex: (((InstHyp [m - 1] (-2) THENA Auto') THEN D (-1)) THEN ExRepD) Home Index