Nuprl Lemma : grp_car_subtype
|(<ℤ+>↓hgrp)| ⊆r ℕ
Proof
Definitions occuring in Statement : 
int_add_grp: <ℤ+>
, 
hgrp_of_ocgrp: g↓hgrp
, 
grp_car: |g|
, 
nat: ℕ
, 
subtype_rel: A ⊆r B
Definitions unfolded in proof : 
subtype_rel: A ⊆r B
, 
member: t ∈ T
, 
nat: ℕ
, 
hgrp_of_ocgrp: g↓hgrp
, 
grp_car: |g|
, 
pi1: fst(t)
, 
hgrp_car: |g|+
, 
int_add_grp: <ℤ+>
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
Lemmas referenced : 
grp_car_wf, 
hgrp_of_ocgrp_wf, 
int_add_grp_wf2, 
zero-le-nat, 
grp_car_inc, 
le_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaEquality, 
dependent_set_memberEquality, 
cut, 
hypothesisEquality, 
applyEquality, 
thin, 
sqequalHypSubstitution, 
sqequalRule, 
setElimination, 
rename, 
introduction, 
extract_by_obid, 
isectElimination, 
hypothesis, 
natural_numberEquality
Latex:
|(<\mBbbZ{}+>\mdownarrow{}hgrp)|  \msubseteq{}r  \mBbbN{}
Date html generated:
2019_10_15-AM-10_33_18
Last ObjectModification:
2018_09_18-PM-00_38_49
Theory : groups_1
Home
Index