---

Step * of Lemma bag-member-classfun

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)].  ∀[e:E]. X(e) ↓∈ X es e supposing X is functional
BY
{ (Auto
   THEN DupHyp 5
   THEN D -1
   THEN RepeatFor 2 ((With ⌈e⌉ (D (-2))⋅ THENA Auto))
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (RepUR ``class-ap classfun classrel`` 0 THEN (GenConcl ⌈(X es e) = b ∈ bag(T)⌉⋅ THENA Auto))
   THEN Fold `single-valued-bag` 0
   THEN All Thin) }

1
1. T : Type
2. b : bag(T)@i
⊢ single-valued-bag(b;T) ⇒ (1 ≤ #(b)) ⇒ sv-bag-only(b) ↓∈ b

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T)].    \mforall{}[e:E].  X(e)  \mdownarrow{}\mmember{}  X  es  e  supposing  X  is  functional


By

(Auto
  THEN  DupHyp  5
  THEN  D  -1
  THEN  RepeatFor  2  ((With  \mkleeneopen{}e\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto))
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (RepUR  ``class-ap  classfun  classrel``  0  THEN  (GenConcl  \mkleeneopen{}(X  es  e)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  Fold  `single-valued-bag`  0
  THEN  All  Thin)

---

Home Index