Step
*
of Lemma
all_fset_elim
∀s:DSet. ∀F:MSet{s} ⟶ ℙ.
((∀a:FiniteSet{s}. SqStable(F[a]))
⇒ (∀a:FiniteSet{s}. F[a]
⇐⇒ ∀a:DisList{s}. F[mk_mset(a)]))
BY
{ ((GenRepD) THENA Auto) }
1
1. s : DSet
2. F : MSet{s} ⟶ ℙ
3. ∀a:FiniteSet{s}. SqStable(F[a])
4. ∀a:FiniteSet{s}. F[a]
5. a : DisList{s}
⊢ F[mk_mset(a)]
2
1. s : DSet
2. F : MSet{s} ⟶ ℙ
3. ∀a:FiniteSet{s}. SqStable(F[a])
4. ∀a:DisList{s}. F[mk_mset(a)]
5. a : FiniteSet{s}
⊢ F[a]
Latex:
Latex:
\mforall{}s:DSet. \mforall{}F:MSet\{s\} {}\mrightarrow{} \mBbbP{}.
((\mforall{}a:FiniteSet\{s\}. SqStable(F[a])) {}\mRightarrow{} (\mforall{}a:FiniteSet\{s\}. F[a] \mLeftarrow{}{}\mRightarrow{} \mforall{}a:DisList\{s\}. F[mk\_mset(a)]))
By
Latex:
((GenRepD) THENA Auto)
Home
Index