---

Step * of Lemma member-fpf-vals2

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ─→ Type]. ∀[P:A ─→ 𝔹]. ∀[f:x:A fp-> B[x]]. ∀[x:{a:A| ↑(P a)} ]. ∀[v:B[x]].
  {(↑x ∈ dom(f)) ∧ (v = f(x) ∈ B[x])} supposing (<x, v> ∈ fpf-vals(eq;P;f))
BY
{ (Intros
   THEN UseWitness ⌈<Ax, Ax>⌉⋅
   THEN ((InstLemma `member-fpf-vals` [⌈A⌉; ⌈eq⌉; ⌈B⌉; ⌈P⌉; ⌈f⌉; ⌈x⌉; ⌈v⌉])⋅ THENA Auto)
   THEN (D (-1))
   THEN (Thin (-1))
   THEN (D (-1))) }

1
.....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))

2
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))
9. {((↑x ∈ dom(f)) ∧ (↑(P x))) ∧ (v = f(x) ∈ B[x])}
⊢ <Ax, Ax> ∈ {(↑x ∈ dom(f)) ∧ (v = f(x) ∈ B[x])}

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:x:A  fp->  B[x]].  \mforall{}[x:\{a:A|  \muparrow{}(P  a)\}  ].
\mforall{}[v:B[x]].
    \{(\muparrow{}x  \mmember{}  dom(f))  \mwedge{}  (v  =  f(x))\}  supposing  (<x,  v>  \mmember{}  fpf-vals(eq;P;f))


By

(Intros
  THEN  UseWitness  \mkleeneopen{}<Ax,  Ax>\mkleeneclose{}\mcdot{}
  THEN  ((InstLemma  `member-fpf-vals`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}P\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}v\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (D  (-1))
  THEN  (Thin  (-1))
  THEN  (D  (-1)))

---

Home Index