### Nuprl Lemma : bag-member-filter-set

`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:{x:T| ↑P[x]} ]. ∀[bs:bag(T)].  uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs)`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-filter: `[x∈b|p[x]]` bag: `bag(T)` assert: `↑b` bool: `𝔹` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` sq_stable: `SqStable(P)` implies: `P `` Q` squash: `↓T` bag-member: `x ↓∈ bs` prop: `ℙ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` cand: `A c∧ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bag-filter: `[x∈b|p[x]]` true: `True`
Lemmas referenced :  sq_stable__bag-member bag-member_wf assert_wf bag-filter_wf bag_wf set_wf bool_wf bag-member-subtype bag-member-filter filter_type l_member_set2 member_filter equal_wf list-subtype-bag l_member_wf squash_wf true_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation setElimination thin rename extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis independent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination setEquality cumulativity applyEquality functionExtensionality dependent_set_memberEquality lambdaEquality because_Cache productElimination independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry functionEquality universeEquality independent_isectElimination dependent_functionElimination dependent_pairFormation productEquality natural_numberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:\{x:T|  \muparrow{}P[x]\}  ].  \mforall{}[bs:bag(T)].    uiff(x  \mdownarrow{}\mmember{}  [x\mmember{}bs|P[x]];x  \mdownarrow{}\mmember{}  bs)

Date html generated: 2017_10_01-AM-08_54_17
Last ObjectModification: 2017_07_26-PM-04_36_01

Theory : bags

Home Index