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: ā‡’ Q function: x:A āŸ¶ B[x] universe: Type
Definitions unfolded in proof :  all: āˆ€x:A. B[x] implies: ā‡’ Q uall: āˆ€[x:A]. B[x] member: t āˆˆ T so_lambda: Ī»2x.t[x] so_apply: x[s] iff: ā‡ā‡’ Q and: P āˆ§ Q rev_implies: ā‡ Q cand: cāˆ§ B uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) uimplies: supposing a prop: ā„™ subtype_rel: A āŠ†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