---

Step * 1 of Lemma member-fpf-vals2

.....antecedent..... 
1. A : Type
2. eq : EqDecider(A)
3. B : A ─→ Type
4. P : A ─→ 𝔹
5. f : x:A fp-> B[x]
6. x : {a:A| ↑(P a)} 
7. v : B[x]
8. (<x, v> ∈ fpf-vals(eq;P;f))
⊢ (<x, v> ∈ fpf-vals(eq;P;f))
BY
{ ((Using [`A',⌈x:{a:A| ↑(P a)}  × B[x]⌉] (BLemma `l_member_subtype`))⋅ THEN Auto THEN D 0 THEN Auto) }

---

Latex:


.....antecedent..... 
1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  B  :  A  {}\mrightarrow{}  Type
4.  P  :  A  {}\mrightarrow{}  \mBbbB{}
5.  f  :  x:A  fp->  B[x]
6.  x  :  \{a:A|  \muparrow{}(P  a)\} 
7.  v  :  B[x]
8.  (<x,  v>  \mmember{}  fpf-vals(eq;P;f))
\mvdash{}  (<x,  v>  \mmember{}  fpf-vals(eq;P;f))


By

((Using  [`A',\mkleeneopen{}x:\{a:A|  \muparrow{}(P  a)\}    \mtimes{}  B[x]\mkleeneclose{}]  (BLemma  `l\_member\_subtype`))\mcdot{}  THEN  Auto  THEN  D  0  THEN  Auto)

---

Home Index