Step
*
1
2
2
1
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
⊢ ¬↑bag-null(F {X@e})
BY
{ (InstHyp [⌈X es e⌉;⌈X@e⌉] 8⋅ THENA Auto)⋅ }
1
.....antecedent..... 
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
⊢ single-valued-bag(X es e;A)
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})
⊢ ¬↑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
\mvdash{}  \mneg{}\muparrow{}bag-null(F  \{X@e\})
By
Latex:
(InstHyp  [\mkleeneopen{}X  es  e\mkleeneclose{};\mkleeneopen{}X@e\mkleeneclose{}]  8\mcdot{}  THENA  Auto)\mcdot{}
Home
Index