---

Step * of Lemma power-set-lift-well-founded-implies

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀x:T. (R x x))
  ⇒ (∀f:ℕ ⟶ P(T). (↓∃n:ℕ. ((power-set-lift(T;R) (f (n + 1)) (f n)) ⇒ (power-set-lift(T;R) (f n) (f (n + 1))))))
  ⇒ AFx,y:T.R[x;y])
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x:T. (R x x)@i
4. ∀f:ℕ ⟶ P(T). (↓∃n:ℕ. ((power-set-lift(T;R) (f (n + 1)) (f n)) ⇒ (power-set-lift(T;R) (f n) (f (n + 1)))))@i'
5. f : ℕ ⟶ T@i
⊢ ↓∃i,j:ℕ. (i < j ∧ R[f i;f j])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:T.  (R  x  x))
    {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  P(T)
                (\mdownarrow{}\mexists{}n:\mBbbN{}
                      ((power-set-lift(T;R)  (f  (n  +  1))  (f  n))  {}\mRightarrow{}  (power-set-lift(T;R)  (f  n)  (f  (n  +  1))))))
    {}\mRightarrow{}  AFx,y:T.R[x;y])


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index