---

Step * of Lemma eclass-ext-classrel

∀[Info,T:Type]. ∀[X,Y:EClass(T)].
  uiff(X = Y ∈ EClass(T);∀es:EO+(Info). ∀e:E. ∀v:T.  (v ∈ X(e) ⇐⇒ v ∈ Y(e))) 
  supposing ∀es:EO+(Info). ∀e:E.  ((#(X es e) ≤ 1) ∧ (#(Y es e) ≤ 1))
BY
{ WithCumulativity((Auto
                    THEN BLemma `eclass-ext`
                    THEN Auto
                    THEN BLemma `equal-bag-size-le1`
                    THEN Auto
                    THEN Try ((BLemma `empty-bag-iff-no-member`
                               THEN Auto
                               THEN Fold `classrel` 0
                               THEN D 0
                               THEN Auto
                               THEN (RWO "6 6<" (-1) THENA Auto)
                               THEN Unfold `classrel` (-1)
                               THEN HypSubst (-3) (-1)
                               THEN Auto
                               THEN BagMemberD (-1))⋅)
                    THEN ElimBagSizeOne''
                    THEN Reduce 0)) }

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
⊢ x1 = x ∈ T

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X,Y:EClass(T)].
    uiff(X  =  Y;\mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}v:T.    (v  \mmember{}  X(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  Y(e))) 
    supposing  \mforall{}es:EO+(Info).  \mforall{}e:E.    ((\#(X  es  e)  \mleq{}  1)  \mwedge{}  (\#(Y  es  e)  \mleq{}  1))


By

WithCumulativity((Auto
                                    THEN  BLemma  `eclass-ext`
                                    THEN  Auto
                                    THEN  BLemma  `equal-bag-size-le1`
                                    THEN  Auto
                                    THEN  Try  ((BLemma  `empty-bag-iff-no-member`
                                                          THEN  Auto
                                                          THEN  Fold  `classrel`  0
                                                          THEN  D  0
                                                          THEN  Auto
                                                          THEN  (RWO  "6  6<"  (-1)  THENA  Auto)
                                                          THEN  Unfold  `classrel`  (-1)
                                                          THEN  HypSubst  (-3)  (-1)
                                                          THEN  Auto
                                                          THEN  BagMemberD  (-1))\mcdot{})
                                    THEN  ElimBagSizeOne''
                                    THEN  Reduce  0))

---

Home Index