---

Step * 1 of Lemma rel_plus-TI

.....wf..... 
1. T : Type@i'
2. R : T ⟶ T ⟶ ℙ@i'
3. ∀Q:T ⟶ ℙ. ((∀x:T. ((∀s:{s:T| R+ x s} . Q[s]) ⇒ Q[x])) ⇒ (∀x:T. (Q x)))@i'
4. Q : T ⟶ ℙ@i'
5. ∀x:T. ((∀s:{s:T| R[x;s]} . Q[s]) ⇒ Q[x])@i
6. x : T@i
7. x1 : T@i
8. ∀s:{s:T| R+ x1 s} . Q[s]@i
9. s : {s:T| R[x1;s]} @i
⊢ s ∈ {s:T| R+ x1 s} 
BY
{ (D -1 THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. T : Type@i'
2. R : T ⟶ T ⟶ ℙ@i'
3. ∀Q:T ⟶ ℙ. ((∀x:T. ((∀s:{s:T| R+ x s} . Q[s]) ⇒ Q[x])) ⇒ (∀x:T. (Q x)))@i'
4. Q : T ⟶ ℙ@i'
5. ∀x:T. ((∀s:{s:T| R[x;s]} . Q[s]) ⇒ Q[x])@i
6. x : T@i
7. x1 : T@i
8. ∀s:{s:T| R+ x1 s} . Q[s]@i
9. s : T@i
10. R[x1;s]@i
⊢ R+ x1 s

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type@i'
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}@i'
3.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}x:T.  ((\mforall{}s:\{s:T|  R\msupplus{}  x  s\}  .  Q[s])  {}\mRightarrow{}  Q[x]))  {}\mRightarrow{}  (\mforall{}x:T.  (Q  x)))@i'
4.  Q  :  T  {}\mrightarrow{}  \mBbbP{}@i'
5.  \mforall{}x:T.  ((\mforall{}s:\{s:T|  R[x;s]\}  .  Q[s])  {}\mRightarrow{}  Q[x])@i
6.  x  :  T@i
7.  x1  :  T@i
8.  \mforall{}s:\{s:T|  R\msupplus{}  x1  s\}  .  Q[s]@i
9.  s  :  \{s:T|  R[x1;s]\}  @i
\mvdash{}  s  \mmember{}  \{s:T|  R\msupplus{}  x1  s\} 


By

---

Latex:
(D  -1  THEN  MemTypeCD  THEN  Auto)

---

Home Index