Nuprl Lemma : isMonomialOne_wf
∀[m:iMonomial()]. (isMonomialOne(m) ∈ 𝔹)
Proof
Definitions occuring in Statement :
isMonomialOne: isMonomialOne(m),
iMonomial: iMonomial(),
bool: 𝔹,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
isMonomialOne: isMonomialOne(m),
iMonomial: iMonomial(),
uimplies: b supposing a,
prop: ℙ,
int_nzero: ℤ-o
Lemmas referenced :
sorted_wf,
subtype_rel_self,
band_wf,
null_wf,
eq_int_wf,
iMonomial_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
spreadEquality,
sqequalHypSubstitution,
productElimination,
thin,
independent_pairEquality,
hypothesisEquality,
setElimination,
rename,
dependent_set_memberEquality,
hypothesis,
extract_by_obid,
isectElimination,
intEquality,
independent_isectElimination,
natural_numberEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[m:iMonomial()]. (isMonomialOne(m) \mmember{} \mBbbB{})
Date html generated:
2017_09_29-PM-05_52_08
Last ObjectModification:
2017_05_03-AM-11_26_54
Theory : omega
Home
Index