### Nuprl Lemma : bag-only_wf2

`∀[T:Type]. ∀[b:bag(T)].  only(b) ∈ T supposing single-valued-bag(b;T) ∧ 0 < #(b)`

Proof

Definitions occuring in Statement :  single-valued-bag: `single-valued-bag(b;T)` bag-only: `only(bs)` bag-size: `#(bs)` bag: `bag(T)` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` and: `P ∧ Q` member: `t ∈ T` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  bag-only: `only(bs)` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ` and: `P ∧ Q`
Lemmas referenced :  and_wf single-valued-bag_wf less_than_wf bag-size_wf nat_wf bag_wf single-valued-bag-hd
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution hypothesis axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination thin hypothesisEquality natural_numberEquality applyEquality lambdaEquality setElimination rename isect_memberEquality because_Cache universeEquality independent_isectElimination productElimination

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].    only(b)  \mmember{}  T  supposing  single-valued-bag(b;T)  \mwedge{}  0  <  \#(b)

Date html generated: 2016_05_15-PM-02_49_07
Last ObjectModification: 2015_12_27-AM-09_35_13

Theory : bags

Home Index