---

Step * 2 3 1 1 of Lemma member-eclass-simple-loc-comb-1-iff


1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : Id ─→ bag(A) ─→ bag(B)
7. X : EClass(A)
8. ∀as:bag(A). ∀x:A.  (single-valued-bag(as;A) ⇒ x ↓∈ as ⇒ (↑bag-null(F loc(e) as) ⇐⇒ ↑bag-null(F loc(e) {x})))
9. ↑bag-null(F loc(e) {})
10. single-valued-classrel(es;X;A)
11. ↑e ∈b X
12. ¬↑bag-null(F loc(e) {X@e})
13. ↑bag-null(F loc(e) (X es e)) ⇐⇒ ↑bag-null(F loc(e) {X@e})
⊢ ¬↑bag-null(F loc(e) (X es e))
BY
{ (RWO "13<" 12 THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  es  :  EO+(Info)
5.  e  :  E
6.  F  :  Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)
7.  X  :  EClass(A)
8.  \mforall{}as:bag(A).  \mforall{}x:A.
          (single-valued-bag(as;A)  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  (\muparrow{}bag-null(F  loc(e)  as)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}bag-null(F  loc(e)  \{x\})))
9.  \muparrow{}bag-null(F  loc(e)  \{\})
10.  single-valued-classrel(es;X;A)
11.  \muparrow{}e  \mmember{}\msubb{}  X
12.  \mneg{}\muparrow{}bag-null(F  loc(e)  \{X@e\})
13.  \muparrow{}bag-null(F  loc(e)  (X  es  e))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}bag-null(F  loc(e)  \{X@e\})
\mvdash{}  \mneg{}\muparrow{}bag-null(F  loc(e)  (X  es  e))


By

---

Latex:
(RWO  "13<"  12  THEN  Auto)

---

Home Index