Step
*
1
2
2
1
2
2
of Lemma
member-eclass-simple-comb-1-iff
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : bag(A) ─→ bag(B)
7. X : EClass(A)
8. ∀as:bag(A). ∀x:A. (single-valued-bag(as;A)
⇒ x ↓∈ as
⇒ (↑bag-null(F as)
⇐⇒ ↑bag-null(F {x})))
9. ↑bag-null(F {})
10. single-valued-classrel(es;X;A)
11. ¬(#(F (X es e)) = 0 ∈ ℤ)
12. ¬((X es e) = {} ∈ bag(A))
13. ↑e ∈b X
14. ↑e ∈b X
15. X@e ↓∈ X es e
16. ↑bag-null(F (X es e))
⇐⇒ ↑bag-null(F {X@e})
⊢ ¬↑bag-null(F {X@e})
BY
{ Assert ⌈¬↑bag-null(F (X es e))⌉⋅ }
1
.....assertion.....
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : bag(A) ─→ bag(B)
7. X : EClass(A)
8. ∀as:bag(A). ∀x:A. (single-valued-bag(as;A)
⇒ x ↓∈ as
⇒ (↑bag-null(F as)
⇐⇒ ↑bag-null(F {x})))
9. ↑bag-null(F {})
10. single-valued-classrel(es;X;A)
11. ¬(#(F (X es e)) = 0 ∈ ℤ)
12. ¬((X es e) = {} ∈ bag(A))
13. ↑e ∈b X
14. ↑e ∈b X
15. X@e ↓∈ X es e
16. ↑bag-null(F (X es e))
⇐⇒ ↑bag-null(F {X@e})
⊢ ¬↑bag-null(F (X es e))
2
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : bag(A) ─→ bag(B)
7. X : EClass(A)
8. ∀as:bag(A). ∀x:A. (single-valued-bag(as;A)
⇒ x ↓∈ as
⇒ (↑bag-null(F as)
⇐⇒ ↑bag-null(F {x})))
9. ↑bag-null(F {})
10. single-valued-classrel(es;X;A)
11. ¬(#(F (X es e)) = 0 ∈ ℤ)
12. ¬((X es e) = {} ∈ bag(A))
13. ↑e ∈b X
14. ↑e ∈b X
15. X@e ↓∈ X es e
16. ↑bag-null(F (X es e))
⇐⇒ ↑bag-null(F {X@e})
17. ¬↑bag-null(F (X es e))
⊢ ¬↑bag-null(F {X@e})
Latex:
Latex:
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : 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 as) \mLeftarrow{}{}\mRightarrow{} \muparrow{}bag-null(F \{x\})))
9. \muparrow{}bag-null(F \{\})
10. single-valued-classrel(es;X;A)
11. \mneg{}(\#(F (X es e)) = 0)
12. \mneg{}((X es e) = \{\})
13. \muparrow{}e \mmember{}\msubb{} X
14. \muparrow{}e \mmember{}\msubb{} X
15. X@e \mdownarrow{}\mmember{} X es e
16. \muparrow{}bag-null(F (X es e)) \mLeftarrow{}{}\mRightarrow{} \muparrow{}bag-null(F \{X@e\})
\mvdash{} \mneg{}\muparrow{}bag-null(F \{X@e\})
By
Latex:
Assert \mkleeneopen{}\mneg{}\muparrow{}bag-null(F (X es e))\mkleeneclose{}\mcdot{}
Home
Index