Nuprl Lemma : grp_blt_wf

āˆ€[g:GrpSig]. āˆ€[a,b:|g|].  (a <b b āˆˆ š”¹)


Proof




Definitions occuring in Statement :  grp_blt: a <b b grp_car: |g| grp_sig: GrpSig bool: š”¹ uall: āˆ€[x:A]. B[x] member: t āˆˆ T
Definitions unfolded in proof :  grp_blt: a <b b uall: āˆ€[x:A]. B[x] member: t āˆˆ T oset_of_ocmon: gā†“oset dset_of_mon: gā†“set set_car: |p| pi1: fst(t)
Lemmas referenced :  set_blt_wf oset_of_ocmon_wf0 grp_car_wf grp_sig_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[g:GrpSig].  \mforall{}[a,b:|g|].    (a  <\msubb{}  b  \mmember{}  \mBbbB{})



Date html generated: 2016_05_15-PM-00_13_31
Last ObjectModification: 2015_12_26-PM-11_41_34

Theory : groups_1


Home Index