Nuprl Lemma : omral_one_wf

g:OCMon. ∀r:CDRng.  (11 ∈ |omral(g;r)|)


Proof




Definitions occuring in Statement :  omral_one: 11 omralist: omral(g;r) all: x:A. B[x] member: t ∈ T cdrng: CDRng ocmon: OCMon set_car: |p|
Definitions unfolded in proof :  omral_one: 11 all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] ocmon: OCMon abmonoid: AbMon mon: Mon cdrng: CDRng crng: CRng rng: Rng
Lemmas referenced :  omral_inj_wf grp_id_wf rng_one_wf cdrng_wf ocmon_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination setElimination rename hypothesis

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.    (11  \mmember{}  |omral(g;r)|)



Date html generated: 2016_05_16-AM-08_26_31
Last ObjectModification: 2015_12_28-PM-06_38_21

Theory : polynom_3


Home Index