Nuprl Lemma : empty-bag-iff-no-member

`∀[T:Type]. ∀[bs:bag(T)].  uiff(bs = {} ∈ bag(T);∀x:T. (¬x ↓∈ bs))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` empty-bag: `{}` bag: `bag(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` bag: `bag(T)` quotient: `x,y:A//B[x; y]` subtype_rel: `A ⊆r B` empty-bag: `{}` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` or: `P ∨ Q` cons: `[a / b]` bag-member: `x ↓∈ bs` exists: `∃x:A. B[x]` cand: `A c∧ B` squash: `↓T`
Lemmas referenced :  bag-member_wf equal-wf-T-base bag_wf all_wf not_wf bag-member-empty list-subtype-bag equal-wf-base list_wf permutation_wf quotient-member-eq permutation-equiv nil_wf permutation_inversion permutation-nil-iff equal_wf list-cases product_subtype_list cons_wf cons_member l_member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lambdaFormation thin hypothesis sqequalHypSubstitution independent_functionElimination voidElimination extract_by_obid isectElimination cumulativity hypothesisEquality equalityTransitivity equalitySymmetry sqequalRule lambdaEquality dependent_functionElimination because_Cache baseClosed productElimination independent_pairEquality isect_memberEquality axiomEquality universeEquality hyp_replacement applyLambdaEquality independent_isectElimination pointwiseFunctionalityForEquality functionEquality pertypeElimination applyEquality productEquality rename unionElimination promote_hyp hypothesis_subsumption dependent_pairFormation inlFormation imageMemberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    uiff(bs  =  \{\};\mforall{}x:T.  (\mneg{}x  \mdownarrow{}\mmember{}  bs))

Date html generated: 2017_10_01-AM-08_53_17
Last ObjectModification: 2017_07_26-PM-04_34_59

Theory : bags

Home Index