---

Step * 2 of Lemma l_all-mapfilter


1. [T] : Type
2. [A] : Type
3. as : T List
4. p : {a:T| (a ∈ as)}  ⟶ 𝔹
5. f : {a:T| (a ∈ as) ∧ (↑(p a))}  ⟶ A
6. P : A ⟶ ℙ
7. (∀x∈mapfilter(f;p;as).P[x]) ∈ ℙ
8. ∀x:T. ((x ∈ as) ⇒ (↑(p x)) ⇒ P[f x])
⊢ (∀x∈mapfilter(f;p;as).P[x])
BY
{ (Try ((Using [`T',⌜A⌝] (BLemma `l_all_iff`)⋅ THEN Auto))
   THEN TACTIC:(RW ListC (-1) THENA Auto)
   THEN ExRepD
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  Type
3.  as  :  T  List
4.  p  :  \{a:T|  (a  \mmember{}  as)\}    {}\mrightarrow{}  \mBbbB{}
5.  f  :  \{a:T|  (a  \mmember{}  as)  \mwedge{}  (\muparrow{}(p  a))\}    {}\mrightarrow{}  A
6.  P  :  A  {}\mrightarrow{}  \mBbbP{}
7.  (\mforall{}x\mmember{}mapfilter(f;p;as).P[x])  \mmember{}  \mBbbP{}
8.  \mforall{}x:T.  ((x  \mmember{}  as)  {}\mRightarrow{}  (\muparrow{}(p  x))  {}\mRightarrow{}  P[f  x])
\mvdash{}  (\mforall{}x\mmember{}mapfilter(f;p;as).P[x])


By

---

Latex:
(Try  ((Using  [`T',\mkleeneopen{}A\mkleeneclose{}]  (BLemma  `l\_all\_iff`)\mcdot{}  THEN  Auto))
  THEN  TACTIC:(RW  ListC  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  Auto)

---

Home Index