Nuprl Lemma : single-valued-bag-filter

`∀[A:Type]. ∀[b:bag(A)]. ∀[p:{x:A| x ↓∈ b}  ⟶ 𝔹].`
`  single-valued-bag([x∈b|p[x]];A) supposing ∀x,y:A.  (x ↓∈ b `` y ↓∈ b `` (↑p[x]) `` (↑p[y]) `` (x = y ∈ A))`

Proof

Definitions occuring in Statement :  single-valued-bag: `single-valued-bag(b;T)` 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 :  all: `∀x:A. B[x]` member: `t ∈ T` implies: `P `` Q` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` prop: `ℙ` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` subtype_rel: `A ⊆r B` guard: `{T}` single-valued-bag: `single-valued-bag(b;T)`
Lemmas referenced :  bag-member-filter2 bag-member_wf bag-filter-wf2 subtype_rel_bag assert_wf all_wf equal_wf bool_wf bag_wf
Rules used in proof :  cut hypothesis sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin hypothesisEquality independent_functionElimination introduction extract_by_obid isectElimination because_Cache sqequalRule lambdaEquality applyEquality functionExtensionality setEquality cumulativity setElimination rename dependent_set_memberEquality productElimination independent_isectElimination equalityTransitivity equalitySymmetry functionEquality universeEquality isect_memberFormation lambdaFormation axiomEquality isect_memberEquality

Latex:
\mforall{}[A:Type].  \mforall{}[b:bag(A)].  \mforall{}[p:\{x:A|  x  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  \mBbbB{}].
single-valued-bag([x\mmember{}b|p[x]];A)
supposing  \mforall{}x,y:A.    (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  y  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\muparrow{}p[x])  {}\mRightarrow{}  (\muparrow{}p[y])  {}\mRightarrow{}  (x  =  y))

Date html generated: 2017_10_01-AM-08_57_37
Last ObjectModification: 2017_07_26-PM-04_39_42

Theory : bags

Home Index