Step
*
2
2
of Lemma
member-eclass-simple-comb-2-iff
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. es : EO+(Info)
6. e : E
7. F : 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 as bs)
⇐⇒ ↑bag-null(F {a} {b})))
11. ∀as:bag(A). (↑bag-null(F as {}))
12. ∀bs:bag(B). (↑bag-null(F {} bs))
13. single-valued-classrel(es;X;A)
14. single-valued-classrel(es;Y;B)
15. ↑e ∈b X
16. ↑e ∈b Y
17. ¬↑bag-null(F {X@e} {Y@e})
⊢ single-valued-bag(Y es e;B)
BY
{ (RepUR ``single-valued-classrel classrel`` 14 THEN Unfold `single-valued-bag` 0 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 : 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 as bs) \mLeftarrow{}{}\mRightarrow{} \muparrow{}bag-null(F \{a\} \{b\})))
11. \mforall{}as:bag(A). (\muparrow{}bag-null(F as \{\}))
12. \mforall{}bs:bag(B). (\muparrow{}bag-null(F \{\} bs))
13. single-valued-classrel(es;X;A)
14. single-valued-classrel(es;Y;B)
15. \muparrow{}e \mmember{}\msubb{} X
16. \muparrow{}e \mmember{}\msubb{} Y
17. \mneg{}\muparrow{}bag-null(F \{X@e\} \{Y@e\})
\mvdash{} single-valued-bag(Y es e;B)
By
Latex:
(RepUR ``single-valued-classrel classrel`` 14 THEN Unfold `single-valued-bag` 0 THEN Auto)\mcdot{}
Home
Index