### Nuprl Lemma : bag-filter-wf2

`∀[T:Type]. ∀[bs:bag(T)]. ∀[p:{b:T| b ↓∈ bs}  ⟶ 𝔹].  ([x∈bs|p[x]] ∈ bag({x:{b:T| b ↓∈ bs} | ↑p[x]} ))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-filter: `[x∈b|p[x]]` bag: `bag(T)` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]`
Lemmas referenced :  bag-filter_wf bag-member_wf bag-subtype bool_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin setEquality hypothesisEquality hypothesis sqequalRule lambdaEquality applyEquality cumulativity dependent_functionElimination equalityTransitivity equalitySymmetry axiomEquality functionEquality isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].  \mforall{}[p:\{b:T|  b  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  \mBbbB{}].    ([x\mmember{}bs|p[x]]  \mmember{}  bag(\{x:\{b:T|  b  \mdownarrow{}\mmember{}  bs\}  |  \muparrow{}p[x]\}  )\000C)

Date html generated: 2016_05_15-PM-02_47_12
Last ObjectModification: 2015_12_27-AM-09_36_19

Theory : bags

Home Index