---

Step * 1 of Lemma rel_plus-uniform-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
7. x1 : T
8. ∀[s:{s:T| R+ x1 s} ]. Q[s]@i
9. s : {s:T| R[x1;s]} 
⊢ 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
7. x1 : T
8. ∀[s:{s:T| R+ x1 s} ]. Q[s]@i
9. s : T
10. R[x1;s]
⊢ 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
7.  x1  :  T
8.  \mforall{}[s:\{s:T|  R\msupplus{}  x1  s\}  ].  Q[s]@i
9.  s  :  \{s:T|  R[x1;s]\} 
\mvdash{}  s  \mmember{}  \{s:T|  R\msupplus{}  x1  s\} 


By

---

Latex:
(D  -1  THEN  MemTypeCD  THEN  Auto)

---

Home Index