Nuprl Lemma : oal_dom_neg

a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|.  (dom(--ps) dom(ps) ∈ FiniteSet{a})

Proof

Definitions occuring in Statement :  oal_neg: --ps oal_dom: dom(ps) oalist: oal(a;b) finite_set: FiniteSet{s} all: x:A. B[x] equal: t ∈ T abdgrp: AbDGrp loset: LOSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T subtype_rel: A ⊆B abdgrp: AbDGrp abgrp: AbGrp grp: Group{i} abdmonoid: AbDMon dmon: DMon uall: [x:A]. B[x] mon: Mon prop: so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a implies:  Q sq_stable: SqStable(P) squash: T finite_set: FiniteSet{s} loset: LOSet poset: POSet{i} qoset: QOSet dset: DSet nat: oal_dom: dom(ps) set_prod: s × t mk_dset: mk_dset(T, eq) set_car: |p| pi1: fst(t) oalist: oal(a;b) dset_set: dset_set dset_list: List dset_of_mon: g↓set iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q true: True guard: {T}
Lemmas referenced :  oal_dom_wf2 subtype_rel_sets mon_wf inverse_wf grp_car_wf grp_op_wf grp_id_wf grp_inv_wf comm_wf eqfun_p_wf grp_eq_wf set_wf sq_stable__comm set_car_wf all_wf le_wf mset_count_wf nat_wf oalist_wf abdgrp_wf loset_wf equal_mset_elim map_wf set_prod_wf dset_of_mon_wf oal_neg_wf permr_weakening equal_wf squash_wf true_wf list_wf dset_wf oal_neg_keys_invar iff_weakening_equal fset_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality applyEquality sqequalRule instantiate isectElimination setEquality hypothesis cumulativity setElimination rename because_Cache lambdaEquality independent_isectElimination independent_functionElimination imageMemberEquality baseClosed imageElimination dependent_set_memberEquality natural_numberEquality equalitySymmetry productElimination productEquality equalityTransitivity universeEquality

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDGrp.  \mforall{}ps:|oal(a;b)|.    (dom(--ps)  =  dom(ps))

Date html generated: 2017_10_01-AM-10_03_17
Last ObjectModification: 2017_03_03-PM-01_06_00

Theory : polynom_2

Home Index