---

Step * 1 of Lemma classrel-classfun-res-alt1


1. Info : Type
2. T : Type
3. es : EO+(Info)
4. X : EClass(T)
5. e : E
6. v : T
7. single-valued-classrel(es;X;T)
⊢ uiff(v ∈ X(e);if e ∈b X then v = X@e ∈ T else False fi )
BY
{ RepeatFor 2 ((D 0 THEN Try (Complete (Auto)))) }

1
1. Info : Type
2. T : Type
3. es : EO+(Info)
4. X : EClass(T)
5. e : E
6. v : T
7. single-valued-classrel(es;X;T)
8. v ∈ X(e)
⊢ if e ∈b X then v = X@e ∈ T else False fi 

2
.....wf..... 
1. Info : Type
2. T : Type
3. es : EO+(Info)
4. X : EClass(T)
5. e : E
6. v : T
7. single-valued-classrel(es;X;T)
8. v ∈ X(e)
9. x : Unit@i
⊢ v = X@e ∈ T ∈ ℙ

3
1. Info : Type
2. T : Type
3. es : EO+(Info)
4. X : EClass(T)
5. e : E
6. v : T
7. single-valued-classrel(es;X;T)
8. if e ∈b X then v = X@e ∈ T else False fi 
⊢ v ∈ X(e)

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  es  :  EO+(Info)
4.  X  :  EClass(T)
5.  e  :  E
6.  v  :  T
7.  single-valued-classrel(es;X;T)
\mvdash{}  uiff(v  \mmember{}  X(e);if  e  \mmember{}\msubb{}  X  then  v  =  X@e  else  False  fi  )


By

RepeatFor  2  ((D  0  THEN  Try  (Complete  (Auto))))

---

Home Index