---

Step * 1 of Lemma decidable__exists-single-valued-classrel


1. [Info] : Type
2. [T] : Type
3. X : EClass(T)@i'
4. es : EO+(Info)@i'
5. ∀e:E. ∀v1,v2:T.  (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ T))@i
6. e : E@i
7. 0 < #(X es e)
⊢ ∃v:T. v ↓∈ X es e
BY
{ ((InstHyp [⌈e⌉] (-3)⋅ THENA Auto)
   THEN Unfold `classrel` (-1)
   THEN Try (Fold `single-valued-bag` (-1)⋅)
   THEN (InstConcl [⌈sv-bag-only(X es e)⌉]⋅ THENA Auto)
   THEN BLemma `bag-member-sv-bag-only`
   THEN Auto) }

---

Latex:



1.  [Info]  :  Type
2.  [T]  :  Type
3.  X  :  EClass(T)@i'
4.  es  :  EO+(Info)@i'
5.  \mforall{}e:E.  \mforall{}v1,v2:T.    (v1  \mmember{}  X(e)  {}\mRightarrow{}  v2  \mmember{}  X(e)  {}\mRightarrow{}  (v1  =  v2))@i
6.  e  :  E@i
7.  0  <  \#(X  es  e)
\mvdash{}  \mexists{}v:T.  v  \mdownarrow{}\mmember{}  X  es  e


By

((InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  Unfold  `classrel`  (-1)
  THEN  Try  (Fold  `single-valued-bag`  (-1)\mcdot{})
  THEN  (InstConcl  [\mkleeneopen{}sv-bag-only(X  es  e)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BLemma  `bag-member-sv-bag-only`
  THEN  Auto)

---

Home Index