Nuprl Lemma : grp_car_inc
|(<ℤ+>↓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,
uall: ∀[x:A]. B[x],
hgrp_of_ocgrp: g↓hgrp,
grp_car: |g|,
pi1: fst(t),
guard: {T},
uimplies: b supposing a,
hgrp_car: |g|+,
grp_leq: a ≤ b,
int_add_grp: <ℤ+>,
grp_le: ≤b,
pi2: snd(t),
grp_id: e,
infix_ap: x f y,
uiff: uiff(P;Q),
and: P ∧ Q,
nat: ℕ,
prop: ℙ
Lemmas referenced :
grp_car_wf,
hgrp_of_ocgrp_wf,
int_add_grp_wf2,
hgrp_car_properties,
int_add_grp_wf,
mon_subtype_grp_sig,
grp_subtype_mon,
abgrp_subtype_grp,
subtype_rel_transitivity,
abgrp_wf,
grp_wf,
mon_wf,
grp_sig_wf,
assert_of_le_int,
le_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
sqequalRule,
applyEquality,
instantiate,
independent_isectElimination,
hypothesisEquality,
setElimination,
rename,
natural_numberEquality,
productElimination,
dependent_set_memberEquality
Latex:
|(<\mBbbZ{}+>\mdownarrow{}hgrp)| \msubseteq{}r \mBbbN{}
Date html generated:
2019_10_15-AM-10_33_13
Last ObjectModification:
2018_09_17-PM-06_24_04
Theory : groups_1
Home
Index