---

Step * of Lemma fset-map_wf

∀[T,X:Type]. ∀[f:T ⟶ X]. ∀[s:fset(T)].  (fset-map(f;s) ∈ fset(X))
BY
{ (Auto
   THEN QuotientElimForEquality (-1)
   THEN EqTypeCD
   THEN Auto
   THEN Unfold `fset-map` 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-map" 0 THENA Auto)) }

1
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)))

---

Latex:

---

Latex:
\mforall{}[T,X:Type].  \mforall{}[f:T  {}\mrightarrow{}  X].  \mforall{}[s:fset(T)].    (fset-map(f;s)  \mmember{}  fset(X))


By

---

Latex:
(Auto
  THEN  QuotientElimForEquality  (-1)
  THEN  EqTypeCD
  THEN  Auto
  THEN  Unfold  `fset-map`  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-map"  0  THENA  Auto))

---

Home Index