### Nuprl Lemma : bag-combine-member-wf

`∀[A,B:Type]. ∀[bs:bag(A)]. ∀[f:{a:A| a ↓∈ bs}  ⟶ bag(B)].  (⋃x∈bs.f[x] ∈ bag(B))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-combine: `⋃x∈bs.f[x]` bag: `bag(T)` 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 :  bag-combine: `⋃x∈bs.f[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_apply: `x[s]` prop: `ℙ`
Lemmas referenced :  bag-union_wf bag-map-member-wf bag_wf bag-member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality applyEquality setEquality functionEquality because_Cache universeEquality isect_memberFormation introduction sqequalRule axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[bs:bag(A)].  \mforall{}[f:\{a:A|  a  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  bag(B)].    (\mcup{}x\mmember{}bs.f[x]  \mmember{}  bag(B))

Date html generated: 2016_05_15-PM-02_47_06
Last ObjectModification: 2015_12_27-AM-09_36_24

Theory : bags

Home Index