Nuprl Lemma : mset_union_wf_f

s:DSet. ∀a,b:FiniteSet{s}.  (a ⋃ b ∈ FiniteSet{s})


Proof




Definitions occuring in Statement :  mset_union: a ⋃ b finite_set: FiniteSet{s} all: x:A. B[x] member: t ∈ T dset: DSet
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] guard: {T} finite_set: FiniteSet{s} dset: DSet so_lambda: λ2x.t[x] subtype_rel: A ⊆B nat: so_apply: x[s] prop: squash: T true: True uimplies: supposing a iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q uiff: uiff(P;Q)
Lemmas referenced :  imax_lb iff_weakening_equal mset_count_union true_wf squash_wf nat_wf mset_count_wf le_wf all_wf set_car_wf mset_union_wf fset_properties dset_wf finite_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution hypothesis lemma_by_obid isectElimination thin hypothesisEquality dependent_functionElimination setElimination rename dependent_set_memberEquality sqequalRule lambdaEquality applyEquality natural_numberEquality imageElimination equalityTransitivity equalitySymmetry intEquality imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination because_Cache independent_pairFormation

Latex:
\mforall{}s:DSet.  \mforall{}a,b:FiniteSet\{s\}.    (a  \mcup{}  b  \mmember{}  FiniteSet\{s\})



Date html generated: 2016_05_16-AM-07_51_16
Last ObjectModification: 2016_01_16-PM-11_39_17

Theory : mset


Home Index