---

Step * 1 of Lemma fset-mapfilter_wf


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))))
BY
{ (RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  X  :  Type
4.  f  :  \{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  X
5.  as  :  T  List
6.  bs  :  T  List
7.  \mforall{}t:T.  ((t  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (t  \mmember{}  bs))
\mvdash{}  \mforall{}t:X
        (\mexists{}y:T.  ((y  \mmember{}  as)  \mwedge{}  ((\muparrow{}(P  y))  c\mwedge{}  (t  =  (f  y))))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}y:T.  ((y  \mmember{}  bs)  \mwedge{}  ((\muparrow{}(P  y))  c\mwedge{}  (t  =  (f  y)))))


By

---

Latex:
(RWO  "-1"  0  THEN  Auto)

---

Home Index