### Nuprl Lemma : bag-from-member-function

`∀[T:Type]`
`  ∀bs:bag(T). ∀P,Q:T ⟶ ℙ.`
`    ((∀i:T. Dec(Q[i]))`
`    `` (∀i:T. (i ↓∈ bs `` Q[i] `` P[i]))`
`    `` (∃b:bag(T). ((∀i:T. (i ↓∈ bs `` Q[i] `` i ↓∈ b)) ∧ (∀i:T. (i ↓∈ b `` P[i])))))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag: `bag(T)` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` exists: `∃x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` decidable: `Dec(P)` or: `P ∨ Q` decision: `Decision` so_apply: `x[s]` prop: `ℙ` uimplies: `b supposing a` top: `Top` and: `P ∧ Q` cand: `A c∧ B` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bag-member: `x ↓∈ bs` squash: `↓T`
Lemmas referenced :  bag_wf decidable_wf all_wf and_wf bag-member_wf dec2bool_decidable bag-member-filter assert_wf subtype_rel_bag top_wf not_wf subtype_rel_union dec2bool_wf bag-filter_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation rename dependent_pairFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality sqequalRule lambdaEquality applyEquality hypothesis universeEquality because_Cache independent_isectElimination isect_memberEquality voidElimination voidEquality setEquality setElimination introduction productElimination independent_pairFormation dependent_functionElimination independent_functionElimination imageElimination imageMemberEquality baseClosed functionEquality

Latex:
\mforall{}[T:Type]
\mforall{}bs:bag(T).  \mforall{}P,Q:T  {}\mrightarrow{}  \mBbbP{}.
((\mforall{}i:T.  Dec(Q[i]))
{}\mRightarrow{}  (\mforall{}i:T.  (i  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  Q[i]  {}\mRightarrow{}  P[i]))
{}\mRightarrow{}  (\mexists{}b:bag(T).  ((\mforall{}i:T.  (i  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  Q[i]  {}\mRightarrow{}  i  \mdownarrow{}\mmember{}  b))  \mwedge{}  (\mforall{}i:T.  (i  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  P[i])))))

Date html generated: 2016_05_15-PM-02_58_51
Last ObjectModification: 2016_01_16-AM-08_37_36

Theory : bags

Home Index