---

Step * 1 of Lemma eclass-ext-classrel


1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. ∀es:EO+(Info). ∀e:E.  ((#(X es e) ≤ 1) ∧ (#(Y es e) ≤ 1))
6. ∀es:EO+(Info). ∀e:E. ∀v:T.  (v ∈ X(e) ⇐⇒ v ∈ Y(e))
7. es : EO+(Info)@i'
8. e : E@i
9. ((X es e) = {} ∈ bag(T)) ⇒ ((Y es e) = {} ∈ bag(T))
10. ((X es e) = {} ∈ bag(T)) ⇐ (Y es e) = {} ∈ bag(T)
11. #(X es e) = 1 ∈ ℤ@i
12. #(Y es e) = 1 ∈ ℤ@i
13. Y es e ~ {only(Y es e)}
14. x : T@i
15. only(Y es e) = x ∈ T@i
16. X es e ~ {only(X es e)}
17. x1 : T@i
18. only(X es e) = x1 ∈ T@i
⊢ x1 = x ∈ T
BY
{ (RevHypSubst (-1) 0 THEN Auto)⋅ }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. ∀es:EO+(Info). ∀e:E.  ((#(X es e) ≤ 1) ∧ (#(Y es e) ≤ 1))
6. ∀es:EO+(Info). ∀e:E. ∀v:T.  (v ∈ X(e) ⇐⇒ v ∈ Y(e))
7. es : EO+(Info)@i'
8. e : E@i
9. ((X es e) = {} ∈ bag(T)) ⇒ ((Y es e) = {} ∈ bag(T))
10. ((X es e) = {} ∈ bag(T)) ⇐ (Y es e) = {} ∈ bag(T)
11. #(X es e) = 1 ∈ ℤ@i
12. #(Y es e) = 1 ∈ ℤ@i
13. Y es e ~ {only(Y es e)}
14. x : T@i
15. only(Y es e) = x ∈ T@i
16. X es e ~ {only(X es e)}
17. x1 : T@i
18. only(X es e) = x1 ∈ T@i
⊢ only(X es e) = x ∈ T

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
4.  Y  :  EClass(T)
5.  \mforall{}es:EO+(Info).  \mforall{}e:E.    ((\#(X  es  e)  \mleq{}  1)  \mwedge{}  (\#(Y  es  e)  \mleq{}  1))
6.  \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}v:T.    (v  \mmember{}  X(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  Y(e))
7.  es  :  EO+(Info)@i'
8.  e  :  E@i
9.  ((X  es  e)  =  \{\})  {}\mRightarrow{}  ((Y  es  e)  =  \{\})
10.  ((X  es  e)  =  \{\})  \mLeftarrow{}{}  (Y  es  e)  =  \{\}
11.  \#(X  es  e)  =  1@i
12.  \#(Y  es  e)  =  1@i
13.  Y  es  e  \msim{}  \{only(Y  es  e)\}
14.  x  :  T@i
15.  only(Y  es  e)  =  x@i
16.  X  es  e  \msim{}  \{only(X  es  e)\}
17.  x1  :  T@i
18.  only(X  es  e)  =  x1@i
\mvdash{}  x1  =  x


By

(RevHypSubst  (-1)  0  THEN  Auto)\mcdot{}

---

Home Index