### Nuprl Lemma : sub-bag-filter2

`∀T:Type. ∀p1,p2:T ⟶ 𝔹. ∀b,c:bag(T).`
`  (sub-bag(T;b;[x∈c|p1[x]]) `` sub-bag(T;b;[x∈c|p2[x]]) `` sub-bag(T;b;[x∈c|p1[x] ∧b p2[x]]))`

Proof

Definitions occuring in Statement :  sub-bag: `sub-bag(T;as;bs)` bag-filter: `[x∈b|p[x]]` bag: `bag(T)` band: `p ∧b q` bool: `𝔹` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` cand: `A c∧ B` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` uimplies: `b supposing a` prop: `ℙ` subtype_rel: `A ⊆r B` guard: `{T}`
Lemmas referenced :  sub-bag-filter band_wf assert_of_band bag-member_wf sub-bag_wf bag-filter_wf subtype_rel_bag assert_wf bag_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination sqequalRule lambdaEquality applyEquality hypothesis productElimination independent_functionElimination independent_pairFormation independent_isectElimination setEquality setElimination rename because_Cache functionEquality universeEquality

Latex:
\mforall{}T:Type.  \mforall{}p1,p2:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}b,c:bag(T).
(sub-bag(T;b;[x\mmember{}c|p1[x]])  {}\mRightarrow{}  sub-bag(T;b;[x\mmember{}c|p2[x]])  {}\mRightarrow{}  sub-bag(T;b;[x\mmember{}c|p1[x]  \mwedge{}\msubb{}  p2[x]]))

Date html generated: 2016_05_15-PM-02_45_22
Last ObjectModification: 2015_12_27-AM-09_37_27

Theory : bags

Home Index