---

Step * 1 of Lemma list-prod-set-type


1. A : Type
2. T : Type
3. L : (A × T) List
4. P : T ⟶ ℙ
5. (∀p∈L.P[snd(p)])
6. L = L ∈ ({p:A × T| P[snd(p)]}  List)
⊢ {p:A × T| P[snd(p)]}  ⊆r (A × {x:T| P[x]} )
BY
{ (D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  T  :  Type
3.  L  :  (A  \mtimes{}  T)  List
4.  P  :  T  {}\mrightarrow{}  \mBbbP{}
5.  (\mforall{}p\mmember{}L.P[snd(p)])
6.  L  =  L
\mvdash{}  \{p:A  \mtimes{}  T|  P[snd(p)]\}    \msubseteq{}r  (A  \mtimes{}  \{x:T|  P[x]\}  )


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index