### Nuprl Lemma : omral_dom_one

`∀g:OCMon. ∀r:CDRng.  ((¬(0 = 1 ∈ |r|)) `` (dom(11) = mset_inj{g↓oset}(e) ∈ FiniteSet{g↓oset}))`

Proof

Definitions occuring in Statement :  omral_one: `11` omral_dom: `dom(ps)` mset_inj: `mset_inj{s}(x)` finite_set: `FiniteSet{s}` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` equal: `s = t ∈ T` cdrng: `CDRng` rng_one: `1` rng_zero: `0` rng_car: `|r|` oset_of_ocmon: `g↓oset` ocmon: `OCMon` grp_id: `e`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` omral_one: `11` member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` ocmon: `OCMon` omon: `OMon` and: `P ∧ Q` abmonoid: `AbMon` mon: `Mon` so_lambda: `λ2x y.t[x; y]` infix_ap: `x f y` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` guard: `{T}` uimplies: `b supposing a` cdrng: `CDRng` crng: `CRng` rng: `Rng` grp_car: `|g|` pi1: `fst(t)` set_car: `|p|` oset_of_ocmon: `g↓oset` dset_of_mon: `g↓set` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` not: `¬A` false: `False` bfalse: `ff`
Lemmas referenced :  equal_wf squash_wf true_wf finite_set_wf oset_of_ocmon_wf ulinorder_wf grp_car_wf assert_wf grp_le_wf bool_wf grp_eq_wf band_wf qoset_subtype_dset poset_subtype_qoset loset_subtype_poset subtype_rel_transitivity loset_wf poset_wf qoset_wf dset_wf omral_dom_inj grp_id_wf rng_one_wf mset_inj_wf_f subtype_rel_self set_car_wf oset_of_ocmon_wf0 iff_weakening_equal not_wf rng_car_wf rng_zero_wf cdrng_wf ocmon_wf rng_eq_wf uiff_transitivity equal-wf-T-base eqtt_to_assert assert_of_rng_eq cdrng_subtype_drng iff_transitivity bnot_wf iff_weakening_uiff eqff_to_assert assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality setElimination rename dependent_set_memberEquality productElimination productEquality because_Cache functionEquality instantiate independent_isectElimination dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed independent_functionElimination unionElimination equalityElimination voidElimination independent_pairFormation impliesFunctionality

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.    ((\mneg{}(0  =  1))  {}\mRightarrow{}  (dom(11)  =  mset\_inj\{g\mdownarrow{}oset\}(e)))

Date html generated: 2018_05_22-AM-07_47_02
Last ObjectModification: 2018_05_19-AM-08_27_48

Theory : polynom_3

Home Index