Nuprl Lemma : sv-bag-only_wf

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


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

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

Date html generated: 2016_05_15-PM-02_43_11
Last ObjectModification: 2015_12_27-AM-09_38_54

Theory : bags

Home Index