Step
*
of Lemma
bag-member-classfun-res
∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(T)]. ∀[e:E].
(X@e ↓∈ X es e) supposing (single-valued-classrel(es;X;T) and (↑e ∈b X))
BY
{ ((UnivCD THENA Auto)
THEN Duplicate (-1)
THEN (With ⌈e⌉ (D (-1))⋅ THENA Auto)
THEN All (RepUR ``classrel classfun-res classfun``)
THEN MoveToConcl (-1)
THEN (GenConcl ⌈(X es e) = b ∈ bag(T)⌉⋅ THENA Auto)
THEN Auto
THEN Fold `single-valued-bag` (-1)
THEN BLemma `bag-member-sv-bag-only`
THEN Auto
THEN (RevHypSubst' (-2) 0 THENA Auto)
THEN BLemma `member-eclass-iff-size`
THEN Auto) }
Latex:
\mforall{}[Info,T:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X:EClass(T)]. \mforall{}[e:E].
(X@e \mdownarrow{}\mmember{} X es e) supposing (single-valued-classrel(es;X;T) and (\muparrow{}e \mmember{}\msubb{} X))
By
((UnivCD THENA Auto)
THEN Duplicate (-1)
THEN (With \mkleeneopen{}e\mkleeneclose{} (D (-1))\mcdot{} THENA Auto)
THEN All (RepUR ``classrel classfun-res classfun``)
THEN MoveToConcl (-1)
THEN (GenConcl \mkleeneopen{}(X es e) = b\mkleeneclose{}\mcdot{} THENA Auto)
THEN Auto
THEN Fold `single-valued-bag` (-1)
THEN BLemma `bag-member-sv-bag-only`
THEN Auto
THEN (RevHypSubst' (-2) 0 THENA Auto)
THEN BLemma `member-eclass-iff-size`
THEN Auto)
Home
Index