Nuprl Lemma : mrec-lt_transitivity
∀[L:MutualRectypeSpec]. ∀[x,y,z:mobj(L)]. (x < y ⇒ y < z ⇒ x < z)
Proof
Definitions occuring in Statement :
mrec-lt: x < y,
mobj: mobj(L),
mrec_spec: MutualRectypeSpec,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
mrec-lt: x < y,
prec_sub+: prec_sub+(P;lbl,p.a[lbl; p]),
member: t ∈ T,
prop: ℙ,
ext-eq: A ≡ B,
and: P ∧ Q,
mrec: mrec(L;i),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
mobj: mobj(L),
mkinds: mKinds,
uimplies: b supposing a,
prec: prec(lbl,p.a[lbl; p];i)
Lemmas referenced :
mrec-lt_wf,
mobj_wf,
mrec_spec_wf,
mobj-ext,
rel_plus_transitivity,
mrec_wf,
prec_sub_wf,
mrec-spec_wf,
istype-atom,
subtype_rel_self,
subtype_rel-equal,
mtype_wf,
mtype-sqequal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
Error :lambdaFormation_alt,
sqequalHypSubstitution,
Error :universeIsType,
cut,
introduction,
extract_by_obid,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
Error :inhabitedIsType,
productElimination,
sqequalRule,
productEquality,
atomEquality,
Error :lambdaEquality_alt,
applyEquality,
instantiate,
functionEquality,
cumulativity,
universeEquality,
Error :dependent_pairEquality_alt,
setElimination,
rename,
because_Cache,
independent_isectElimination,
independent_functionElimination
Latex:
\mforall{}[L:MutualRectypeSpec]. \mforall{}[x,y,z:mobj(L)]. (x < y {}\mRightarrow{} y < z {}\mRightarrow{} x < z)
Date html generated:
2019_06_20-PM-02_15_47
Last ObjectModification:
2019_02_26-AM-11_39_05
Theory : tuples
Home
Index