### Nuprl Lemma : bag-only_wf2

[T:Type]. ∀[b:bag(T)].  only(b) ∈ 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: 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: supposing a prop: subtype_rel: A ⊆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