### Nuprl Lemma : bag-subtype2

`∀[A:Type]. ∀P:A ⟶ ℙ. ∀b:bag({x:A| P[x]} ). ∀x:{x:A| P[x]} .  (x ↓∈ b `⇐⇒` x ↓∈ b)`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag: `bag(T)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `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` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` so_apply: `x[s]` uimplies: `b supposing a` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` bag-member: `x ↓∈ bs` squash: `↓T` sq_stable: `SqStable(P)` exists: `∃x:A. B[x]` bag: `bag(T)` quotient: `x,y:A//B[x; y]` cand: `A c∧ B` permutation: `permutation(T;L1;L2)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` label: `...\$L... t` guard: `{T}`
Lemmas referenced :  bag-member_wf subtype_rel_bag set_wf bag_wf bag_to_squash_list sq_stable__bag-member member_wf list_wf subtype_rel_list permutation_wf permutation_inversion permute_list_wf list-eq-subtype2 quotient-member-eq permutation-equiv l_member-settype equal_wf list-subtype-bag subtype_rel_self l_member_wf permutation-strong-subtype strong-subtype-set2 bag-member-subtype
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality setElimination rename hypothesis applyEquality setEquality functionExtensionality because_Cache sqequalRule independent_isectElimination lambdaEquality dependent_set_memberEquality universeEquality functionEquality dependent_functionElimination productElimination independent_pairEquality imageElimination imageMemberEquality baseClosed instantiate independent_functionElimination promote_hyp equalitySymmetry hyp_replacement applyLambdaEquality pertypeElimination productEquality equalityTransitivity dependent_pairFormation

Latex:
\mforall{}[A:Type].  \mforall{}P:A  {}\mrightarrow{}  \mBbbP{}.  \mforall{}b:bag(\{x:A|  P[x]\}  ).  \mforall{}x:\{x:A|  P[x]\}  .    (x  \mdownarrow{}\mmember{}  b  \mLeftarrow{}{}\mRightarrow{}  x  \mdownarrow{}\mmember{}  b)

Date html generated: 2017_10_01-AM-08_56_31
Last ObjectModification: 2017_07_26-PM-04_38_53

Theory : bags

Home Index