---

Step * 1 of Lemma property-from-l_member


1. [T] : Type
2. x : T@i
3. [P] : T ⟶ ℙ
4. ∀[d:{i:T| P[i]}  List]. x ∈ {x:T| P[x]}  supposing (x ∈ d)
5. ∀x:T. SqStable(P[x])@i
6. d : {i:T| P[i]}  List@i
7. (x ∈ d)@i
8. x ∈ {x:T| P[x]} 
⊢ P[x]
BY
{ (MemTypeHD (-1)⋅ THEN Auto) }

1
1. [T] : Type
2. x : T@i
3. [P] : T ⟶ ℙ
4. ∀[d:{i:T| P[i]}  List]. x ∈ {x:T| P[x]}  supposing (x ∈ d)
5. ∀x:T. SqStable(P[x])@i
6. d : {i:T| P[i]}  List@i
7. (x ∈ d)@i
8. x = x ∈ T
9. [%11] : P[x]
⊢ P[x]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  T@i
3.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}[d:\{i:T|  P[i]\}    List].  x  \mmember{}  \{x:T|  P[x]\}    supposing  (x  \mmember{}  d)
5.  \mforall{}x:T.  SqStable(P[x])@i
6.  d  :  \{i:T|  P[i]\}    List@i
7.  (x  \mmember{}  d)@i
8.  x  \mmember{}  \{x:T|  P[x]\} 
\mvdash{}  P[x]


By

---

Latex:
(MemTypeHD  (-1)\mcdot{}  THEN  Auto)

---

Home Index