---

Step * 2 of Lemma es-sv-class-implies-single-valued-classrel


1. Info : Type
2. T : Type
3. es : EO+(Info)
4. X : EClass(T)
5. ∀e:E. (#(X es e) ≤ 1)
6. e : E@i
7. v1 : T@i
8. v2 : T@i
9. v1 ∈ X(e)@i
10. v2 ∈ X(e)@i
11. #(X es e) ≤ 1
12. #(X es e) = 1 ∈ ℤ
⊢ v1 = v2 ∈ T
BY
{ ((FLemma `bag-size-one` [-1] THENA Auto)
   THEN All (Unfold `classrel`)
   THEN HypSubst' (-1) (-5)
   THEN HypSubst' (-1) (-4)
   THEN (BagMemberD (-5)⋅ THEN Try ((BLemma `single-valued-bag-if-le1` THEN Auto)))
   THEN BagMemberD (-4)⋅
   THEN Try (BLemma `single-valued-bag-if-le1`)
   THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  es  :  EO+(Info)
4.  X  :  EClass(T)
5.  \mforall{}e:E.  (\#(X  es  e)  \mleq{}  1)
6.  e  :  E@i
7.  v1  :  T@i
8.  v2  :  T@i
9.  v1  \mmember{}  X(e)@i
10.  v2  \mmember{}  X(e)@i
11.  \#(X  es  e)  \mleq{}  1
12.  \#(X  es  e)  =  1
\mvdash{}  v1  =  v2


By

((FLemma  `bag-size-one`  [-1]  THENA  Auto)
  THEN  All  (Unfold  `classrel`)
  THEN  HypSubst'  (-1)  (-5)
  THEN  HypSubst'  (-1)  (-4)
  THEN  (BagMemberD  (-5)\mcdot{}  THEN  Try  ((BLemma  `single-valued-bag-if-le1`  THEN  Auto)))
  THEN  BagMemberD  (-4)\mcdot{}
  THEN  Try  (BLemma  `single-valued-bag-if-le1`)
  THEN  Auto)

---

Home Index