---

Step * of Lemma fset-mapfilter_wf

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[X:Type]. ∀[f:{x:T| ↑(P x)}  ⟶ X]. ∀[s:fset(T)].  (fset-mapfilter(f;P;s) ∈ fset(X))
BY
{ (Auto
   THEN QuotientElimForEquality (-1)
   THEN EqTypeCD
   THEN Auto
   THEN Unfold `fset-mapfilter` 0
   THEN Auto
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜s = as ∈ (T List)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜s1 = bs ∈ (T List)⌝⋅ THENA Auto)
   THEN All  Thin
   THEN Auto
   THEN ParallelLast
   THEN (RWO  "member-mapfilter" 0 THENA Auto)) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. X : Type
4. f : {x:T| ↑(P x)}  ⟶ X
5. as : T List
6. bs : T List
7. ∀t:T. ((t ∈ as) ⇐⇒ (t ∈ bs))
⊢ ∀t:X. (∃y:T. ((y ∈ as) ∧ ((↑(P y)) c∧ (t = (f y) ∈ X))) ⇐⇒ ∃y:T. ((y ∈ bs) ∧ ((↑(P y)) c∧ (t = (f y) ∈ X))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[X:Type].  \mforall{}[f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  X].  \mforall{}[s:fset(T)].
    (fset-mapfilter(f;P;s)  \mmember{}  fset(X))


By

---

Latex:
(Auto
  THEN  QuotientElimForEquality  (-1)
  THEN  EqTypeCD
  THEN  Auto
  THEN  Unfold  `fset-mapfilter`  0
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}s  =  as\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}s1  =  bs\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All    Thin
  THEN  Auto
  THEN  ParallelLast
  THEN  (RWO    "member-mapfilter"  0  THENA  Auto))

---

Home Index