---

Step * of Lemma fset-filter_wf2

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].  ({x ∈ s | P[x]} ∈ fset({x:T| ↑P[x]} ))
BY
{ ((UnivCD ⋅ THENA Auto)
   THEN (D -1 THENA Auto)
   THEN Unfold `fset-filter` 0
   THEN (Assert ∀s:T List. (filter(λx.P[x];s) ∈ {x:T| ↑P[x]}  List) BY
               ((D 0 THENA Auto) THEN Subst' {x:T| ↑P[x]}  ~ {x:T| ↑λx.P[x][x]}  0 THEN Try ((BLemma `filter_type`⋅ THEN\000C Auto)) THEN RepUR ``so_apply`` 0 THEN Auto))
   THEN EqTypeCD⋅
   THEN Auto
   THEN DupHyp (-2)
   THEN RepeatFor 2 (ParallelLast)⋅
   THEN RWO "member-filter" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  \mcdot{}  THENA  Auto)
  THEN  (D  -1  THENA  Auto)
  THEN  Unfold  `fset-filter`  0
  THEN  (Assert  \mforall{}s:T  List.  (filter(\mlambda{}x.P[x];s)  \mmember{}  \{x:T|  \muparrow{}P[x]\}    List)  BY
                          ((D  0  THENA  Auto)
                            THEN  Subst'  \{x:T|  \muparrow{}P[x]\}    \msim{}  \{x:T|  \muparrow{}\mlambda{}x.P[x][x]\}    0
                            THEN  Try  ((BLemma  `filter\_type`\mcdot{}  THEN  Auto))
                            THEN  RepUR  ``so\_apply``  0
                            THEN  Auto))
  THEN  EqTypeCD\mcdot{}
  THEN  Auto
  THEN  DupHyp  (-2)
  THEN  RepeatFor  2  (ParallelLast)\mcdot{}
  THEN  RWO  "member-filter"  0
  THEN  Auto)

---

Home Index