### Nuprl 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)]))`

Proof

Definitions occuring in Statement :  finite_set: `FiniteSet{s}` mk_mset: `mk_mset(as)` mset: `MSet{s}` dislist: `DisList{s}` sq_stable: `SqStable(P)` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` function: `x:A ⟶ B[x]` dset: `DSet`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` finite_set: `FiniteSet{s}` rev_implies: `P `` Q` dislist: `DisList{s}` sq_stable: `SqStable(P)` dset: `DSet` subtype_rel: `A ⊆r B` nat: `ℕ` squash: `↓T` mset: `MSet{s}` quotient: `x,y:A//B[x; y]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` mk_mset: `mk_mset(as)` mset_count: `x #∈ a`
Lemmas referenced :  dislist_wf all_wf finite_set_wf mset_wf mk_mset_wf sq_stable_wf dset_wf mk_mset_wf2 sq_stable__all set_car_wf le_wf mset_count_wf nat_wf squash_wf sq_stable__squash list_wf subtype_quotient permr_wf permr_equiv_rel equal_wf equal-wf-base count_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis isectElimination sqequalRule lambdaEquality applyEquality functionExtensionality setElimination rename functionEquality cumulativity universeEquality independent_functionElimination natural_numberEquality because_Cache imageElimination imageMemberEquality baseClosed pointwiseFunctionalityForEquality pertypeElimination productElimination equalityTransitivity equalitySymmetry independent_isectElimination productEquality dependent_set_memberEquality

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)]))

Date html generated: 2017_10_01-AM-09_59_03
Last ObjectModification: 2017_03_03-PM-01_00_18

Theory : mset

Home Index