Nuprl Lemma : comp_id_mon_wf

[T:Type]. ((<o,Id> monoid on T) ∈ IMonoid)


Proof




Definitions occuring in Statement :  comp_id_mon: (<o,Id> monoid on T) imon: IMonoid uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  comp_id_mon: (<o,Id> monoid on T) uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a assoc: Assoc(T;op) infix_ap: y ident: Ident(T;op;id) and: P ∧ Q tidentity: Id{T}
Lemmas referenced :  mk_imon btrue_wf compose_wf identity_wf comp_assoc comp_id_r comp_id_l
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution hypothesis axiomEquality equalityTransitivity equalitySymmetry universeEquality lemma_by_obid isectElimination thin functionEquality hypothesisEquality lambdaEquality because_Cache independent_isectElimination isect_memberEquality independent_pairFormation productElimination independent_pairEquality

Latex:
\mforall{}[T:Type].  ((<o,Id>  monoid  on  T)  \mmember{}  IMonoid)



Date html generated: 2016_05_15-PM-00_17_15
Last ObjectModification: 2015_12_26-PM-11_39_00

Theory : groups_1


Home Index