Nuprl Lemma : ot-less-trans_wf
ot-less-trans() ∈ Trans(WFO{i:l}();x,y.order-type-less() x y)
Proof
Definitions occuring in Statement :
ot-less-trans: ot-less-trans(),
WFO: WFO{i:l}(),
order-type-less: order-type-less(),
trans: Trans(T;x,y.E[x; y]),
member: t ∈ T,
apply: f a
Definitions unfolded in proof :
member: t ∈ T,
order-type-less-transitive-ext
Lemmas referenced :
order-type-less-transitive-ext
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
instantiate,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
sqequalRule,
equalityTransitivity,
equalitySymmetry
Latex:
ot-less-trans() \mmember{} Trans(WFO\{i:l\}();x,y.order-type-less() x y)
Date html generated:
2018_05_21-PM-07_02_15
Last ObjectModification:
2018_05_19-PM-04_44_04
Theory : general
Home
Index