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

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

Proof

Definitions occuring in Statement :  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]` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` guard: `{T}` so_apply: `x[s]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` implies: `P `` Q` all: `∀x:A. B[x]` and: `P ∧ Q` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` cand: `A c∧ B` quotient: `x,y:A//B[x; y]` bag: `bag(T)` exists: `∃x:A. B[x]` squash: `↓T` bag-member: `x ↓∈ bs` bag-filter: `[x∈b|p[x]]` sq_stable: `SqStable(P)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` true: `True` respects-equality: `respects-equality(S;T)`
Lemmas referenced :  bag-member_wf bool_wf bag_wf istype-universe list_wf assert_wf subtype_rel_bag list-subtype-bag bag-filter-wf2 permutation_wf l_member-bag-member filter_wf5 bag-member-evidence list-member-bag-member l_member_wf member_filter_2 member-permutation assert_witness sq_stable__uall istype-assert sq_stable__and sq_stable__bag-member sq_stable_from_decidable decidable__assert quotient-member-eq permutation-equiv iff_weakening_equal subtype-respects-equality subtype_rel_sets_simple squash_wf true_wf subtype_rel_self equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut functionIsType setIsType because_Cache universeIsType introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis instantiate universeEquality setEquality equalitySymmetry equalityTransitivity dependent_functionElimination dependent_set_memberEquality_alt rename setElimination inhabitedIsType independent_isectElimination applyEquality lambdaEquality_alt sqequalRule lambdaFormation_alt independent_pairFormation baseClosed imageMemberEquality equalityIsType1 productIsType independent_functionElimination pertypeElimination productElimination imageElimination productEquality isect_memberEquality_alt independent_pairEquality functionIsTypeImplies pointwiseFunctionalityForEquality promote_hyp equalityIstype sqequalBase functionEquality natural_numberEquality isectEquality hyp_replacement applyLambdaEquality

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

Date html generated: 2019_10_15-AM-11_02_35
Last ObjectModification: 2018_11_27-AM-00_30_22

Theory : bags

Home Index