### 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 ↓∈ b and (∀y:A. (y ↓∈ b `` (↑p[y]) `` (y = x ∈ A))))`

Proof

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: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` guard: `{T}` prop: `ℙ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` implies: `P `` Q` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)` cand: `A 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

Latex:
\mforall{}[A:Type].  \mforall{}[b:bag(A)].  \mforall{}[p:\{x:A|  x  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  \mBbbB{}].
\mforall{}x:A
(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