---

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


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
6. ↓∃n:ℕ
     ((∀x:T. ((∃i:{(n + 1) + 1...}. (x = (f i) ∈ T)) ⇒ (∃y:T. ((∃i:{n + 1...}. (y = (f i) ∈ T)) ∧ (R x y)))))
     ⇒ (∀x:T. ((∃i:{n + 1...}. (x = (f i) ∈ T)) ⇒ (∃y:T. ((∃i:{(n + 1) + 1...}. (y = (f i) ∈ T)) ∧ (R x y))))))
⊢ ↓∃i,j:ℕ. (i < j ∧ R[f i;f j])
BY
{ (ParallelLast THEN ExRepD THEN D -1) }

1
.....antecedent..... 
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
6. n : ℕ
⊢ ∀x:T. ((∃i:{(n + 1) + 1...}. (x = (f i) ∈ T)) ⇒ (∃y:T. ((∃i:{n + 1...}. (y = (f i) ∈ T)) ∧ (R x y))))

2
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
6. n : ℕ
7. ∀x:T. ((∃i:{n + 1...}. (x = (f i) ∈ T)) ⇒ (∃y:T. ((∃i:{(n + 1) + 1...}. (y = (f i) ∈ T)) ∧ (R x y))))
⊢ ∃i,j:ℕ. (i < j ∧ R[f i;f j])

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  (R  x  x)@i
4.  \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)))))@i'
5.  f  :  \mBbbN{}  {}\mrightarrow{}  T@i
6.  \mdownarrow{}\mexists{}n:\mBbbN{}
          ((\mforall{}x:T
                  ((\mexists{}i:\{(n  +  1)  +  1...\}.  (x  =  (f  i)))  {}\mRightarrow{}  (\mexists{}y:T.  ((\mexists{}i:\{n  +  1...\}.  (y  =  (f  i)))  \mwedge{}  (R  x  y)))))
          {}\mRightarrow{}  (\mforall{}x:T
                      ((\mexists{}i:\{n  +  1...\}.  (x  =  (f  i)))
                      {}\mRightarrow{}  (\mexists{}y:T.  ((\mexists{}i:\{(n  +  1)  +  1...\}.  (y  =  (f  i)))  \mwedge{}  (R  x  y))))))
\mvdash{}  \mdownarrow{}\mexists{}i,j:\mBbbN{}.  (i  <  j  \mwedge{}  R[f  i;f  j])


By

---

Latex:
(ParallelLast  THEN  ExRepD  THEN  D  -1)

---

Home Index