---

Step * 1 of Lemma fset-map_wf


1. T : Type
2. X : Type
3. f : T ⟶ X
4. as : T List
5. bs : T List
6. ∀t:T. ((t ∈ as) ⇐⇒ (t ∈ bs))
⊢ ∀t:X. (∃y:T. ((y ∈ as) ∧ (t = (f y) ∈ X)) ⇐⇒ ∃y:T. ((y ∈ bs) ∧ (t = (f y) ∈ X)))
BY
{ (RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

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

---

Home Index