---

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

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)].  single-valued-classrel(es;X;T) supposing es-sv-class(es;X)
BY
{ (RepUR ``es-sv-class single-valued-classrel`` 0
   THEN (UnivCD THENA Auto)
   THEN (InstHyp [⌈e⌉] (-6)⋅ THENA Auto)
   THEN (Assert ⌈(#(X es e) = 0 ∈ ℤ) ∨ (#(X es e) = 1 ∈ ℤ)⌉⋅ THENA Auto')
   THEN D (-1)) }

1
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) = 0 ∈ ℤ
⊢ v1 = v2 ∈ T

2
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

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T)].
    single-valued-classrel(es;X;T)  supposing  es-sv-class(es;X)


By

(RepUR  ``es-sv-class  single-valued-classrel``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(\#(X  es  e)  =  0)  \mvee{}  (\#(X  es  e)  =  1)\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  D  (-1))

---

Home Index