Nuprl Lemma : DCC-order-type_wf
DCC-order-type() ∈ DCC(WFO{i:l}();order-type-less())
Proof
Definitions occuring in Statement :
DCC-order-type: DCC-order-type(),
WFO: WFO{i:l}(),
order-type-less: order-type-less(),
DCC: DCC(T;<),
member: t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
DCC-order-type-less-ext
Lemmas referenced :
DCC-order-type-less-ext
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
instantiate,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
sqequalRule,
equalityTransitivity,
equalitySymmetry
Latex:
DCC-order-type() \mmember{} DCC(WFO\{i:l\}();order-type-less())
Date html generated:
2018_05_21-PM-07_14_36
Last ObjectModification:
2018_05_19-PM-04_45_34
Theory : general
Home
Index