---

Step * 3 of Lemma descending-chain-barred-implies-wellfounded


1. T : Type
2. < : T ⟶ T ⟶ ℙ
3. B : T ⟶ T ⟶ ℙ
4. ∀x,y,z:T.  ((x < y) ⇒ (y < z) ⇒ (x < z))
5. ∀x,y:T.  Dec(x B y)
6. ∀x,y:T.  ((x B y) ⇒ (¬(x < y)))
7. ∀f:ℕ ⟶ T. (↓∃j:ℕ. ∃i:ℕj. ((f j) B (f i)))
8. P : T ⟶ ℙ
9. ∀j:T. ((∀k:T. ((k < j) ⇒ P[k])) ⇒ P[j])
10. alpha : ℕ ⟶ T
⊢ ↓∃m:ℕ. ∃j:ℕm. ∃i:ℕj. ((alpha j) B (alpha i))
BY
{ ((With ⌜alpha⌝ (D 7)⋅ THENA Auto) THEN ExRepD) }

1
1. T : Type
2. < : T ⟶ T ⟶ ℙ
3. B : T ⟶ T ⟶ ℙ
4. ∀x,y,z:T.  ((x < y) ⇒ (y < z) ⇒ (x < z))
5. ∀x,y:T.  Dec(x B y)
6. ∀x,y:T.  ((x B y) ⇒ (¬(x < y)))
7. P : T ⟶ ℙ
8. ∀j:T. ((∀k:T. ((k < j) ⇒ P[k])) ⇒ P[j])
9. alpha : ℕ ⟶ T
10. ↓∃j:ℕ. ∃i:ℕj. ((alpha j) B (alpha i))
⊢ ↓∃m:ℕ. ∃j:ℕm. ∃i:ℕj. ((alpha j) B (alpha i))

---

Latex:

---

Latex:

1.  T  :  Type
2.  <  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  B  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x,y,z:T.    ((x  <  y)  {}\mRightarrow{}  (y  <  z)  {}\mRightarrow{}  (x  <  z))
5.  \mforall{}x,y:T.    Dec(x  B  y)
6.  \mforall{}x,y:T.    ((x  B  y)  {}\mRightarrow{}  (\mneg{}(x  <  y)))
7.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}j:\mBbbN{}.  \mexists{}i:\mBbbN{}j.  ((f  j)  B  (f  i)))
8.  P  :  T  {}\mrightarrow{}  \mBbbP{}
9.  \mforall{}j:T.  ((\mforall{}k:T.  ((k  <  j)  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j])
10.  alpha  :  \mBbbN{}  {}\mrightarrow{}  T
\mvdash{}  \mdownarrow{}\mexists{}m:\mBbbN{}.  \mexists{}j:\mBbbN{}m.  \mexists{}i:\mBbbN{}j.  ((alpha  j)  B  (alpha  i))


By

---

Latex:
((With  \mkleeneopen{}alpha\mkleeneclose{}  (D  7)\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index