---

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


1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. es : EO+(Info)
6. e : E
7. F : Id ─→ bag(A) ─→ bag(B) ─→ bag(C)
8. X : EClass(A)
9. Y : EClass(B)
10. ∀as:bag(A). ∀bs:bag(B). ∀a:A. ∀b:B.
      (single-valued-bag(as;A)
      ⇒ single-valued-bag(bs;B)
      ⇒ a ↓∈ as
      ⇒ b ↓∈ bs
      ⇒ (↑bag-null(F loc(e) as bs) ⇐⇒ ↑bag-null(F loc(e) {a} {b})))
11. ∀as:bag(A). (↑bag-null(F loc(e) as {}))
12. ∀bs:bag(B). (↑bag-null(F loc(e) {} bs))
13. single-valued-classrel(es;X;A)
14. single-valued-classrel(es;Y;B)
15. ¬(#(F loc(e) (X es e) (Y es e)) = 0 ∈ ℤ)
16. ↑bag-null(F loc(e) (X es e) {})
17. ↑bag-null(F loc(e) {} (Y es e))
18. ¬((X es e) = {} ∈ bag(A))
19. ¬((Y es e) = {} ∈ bag(B))
20. ↑e ∈b X
21. ↑e ∈b Y
22. ↑e ∈b X
23. ↑e ∈b Y
24. X@e ↓∈ X es e ∧ Y@e ↓∈ Y es e
25. ↑bag-null(F loc(e) (X es e) (Y es e)) ⇐⇒ ↑bag-null(F loc(e) {X@e} {Y@e})
26. ¬↑bag-null(F loc(e) (X es e) (Y es e))
⊢ ¬↑bag-null(F loc(e) {X@e} {Y@e})
BY
{ (ProveProp1 THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  C  :  Type
5.  es  :  EO+(Info)
6.  e  :  E
7.  F  :  Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C)
8.  X  :  EClass(A)
9.  Y  :  EClass(B)
10.  \mforall{}as:bag(A).  \mforall{}bs:bag(B).  \mforall{}a:A.  \mforall{}b:B.
            (single-valued-bag(as;A)
            {}\mRightarrow{}  single-valued-bag(bs;B)
            {}\mRightarrow{}  a  \mdownarrow{}\mmember{}  as
            {}\mRightarrow{}  b  \mdownarrow{}\mmember{}  bs
            {}\mRightarrow{}  (\muparrow{}bag-null(F  loc(e)  as  bs)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}bag-null(F  loc(e)  \{a\}  \{b\})))
11.  \mforall{}as:bag(A).  (\muparrow{}bag-null(F  loc(e)  as  \{\}))
12.  \mforall{}bs:bag(B).  (\muparrow{}bag-null(F  loc(e)  \{\}  bs))
13.  single-valued-classrel(es;X;A)
14.  single-valued-classrel(es;Y;B)
15.  \mneg{}(\#(F  loc(e)  (X  es  e)  (Y  es  e))  =  0)
16.  \muparrow{}bag-null(F  loc(e)  (X  es  e)  \{\})
17.  \muparrow{}bag-null(F  loc(e)  \{\}  (Y  es  e))
18.  \mneg{}((X  es  e)  =  \{\})
19.  \mneg{}((Y  es  e)  =  \{\})
20.  \muparrow{}e  \mmember{}\msubb{}  X
21.  \muparrow{}e  \mmember{}\msubb{}  Y
22.  \muparrow{}e  \mmember{}\msubb{}  X
23.  \muparrow{}e  \mmember{}\msubb{}  Y
24.  X@e  \mdownarrow{}\mmember{}  X  es  e  \mwedge{}  Y@e  \mdownarrow{}\mmember{}  Y  es  e
25.  \muparrow{}bag-null(F  loc(e)  (X  es  e)  (Y  es  e))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}bag-null(F  loc(e)  \{X@e\}  \{Y@e\})
26.  \mneg{}\muparrow{}bag-null(F  loc(e)  (X  es  e)  (Y  es  e))
\mvdash{}  \mneg{}\muparrow{}bag-null(F  loc(e)  \{X@e\}  \{Y@e\})


By

---

Latex:
(ProveProp1  THEN  Auto)

---

Home Index