Nuprl Lemma : sv-bag-only-filter

[A:Type]. ∀[b:bag(A)]. ∀[p:{x:A| x ↓∈ b}  ⟶ 𝔹].
  ∀x:A. (sv-bag-only([x∈b|p[x]]) x ∈ A) supposing ((↑p[x]) and x ↓∈ and (∀y:A. (y ↓∈  (↑p[y])  (y x ∈ A))))


Definitions occuring in Statement :  sv-bag-only: sv-bag-only(b) bag-member: x ↓∈ bs bag-filter: [x∈b|p[x]] bag: bag(T) assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] uimplies: supposing a subtype_rel: A ⊆B guard: {T} prop: so_apply: x[s] so_lambda: λ2x.t[x] implies:  Q uiff: uiff(P;Q) and: P ∧ Q rev_uimplies: rev_uimplies(P;Q) cand: c∧ B
Lemmas referenced :  bag-filter-wf2 subtype_rel_bag bag-member_wf assert_wf single-valued-bag-filter bag-member-size bag-member-filter2 bag-member-sv-bag-only sv-bag-only_wf all_wf equal_wf bool_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality equalityTransitivity hypothesis equalitySymmetry applyEquality setEquality cumulativity functionExtensionality setElimination rename dependent_set_memberEquality independent_isectElimination lambdaEquality sqequalRule dependent_functionElimination independent_functionElimination productElimination independent_pairFormation isect_memberEquality axiomEquality functionEquality universeEquality

\mforall{}[A:Type].  \mforall{}[b:bag(A)].  \mforall{}[p:\{x:A|  x  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  \mBbbB{}].
        (sv-bag-only([x\mmember{}b|p[x]])  =  x)  supposing 
              ((\muparrow{}p[x])  and 
              x  \mdownarrow{}\mmember{}  b  and 
              (\mforall{}y:A.  (y  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\muparrow{}p[y])  {}\mRightarrow{}  (y  =  x))))

Date html generated: 2017_10_01-AM-08_57_48
Last ObjectModification: 2017_07_26-PM-04_39_57

Theory : bags

Home Index