Nuprl Lemma : order-type-less_wf

order-type-less() ∈ WFO{i:l}() ⟶ WFO{i:l}() ⟶ ℙ'


Proof




Definitions occuring in Statement :  WFO: WFO{i:l}() order-type-less: order-type-less() prop: member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  WFO: WFO{i:l}() order-type-less: order-type-less() member: t ∈ T spreadn: spread3 uall: [x:A]. B[x] so_lambda: λ2x.t[x] prop: and: P ∧ Q so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] infix_ap: y so_apply: x[s] all: x:A. B[x] subtype_rel: A ⊆B
Lemmas referenced :  exists_wf order-preserving_wf infix_ap_wf all_wf DCC_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule lambdaEquality productElimination thin cut lemma_by_obid sqequalHypSubstitution isectElimination functionEquality cumulativity hypothesisEquality productEquality because_Cache instantiate universeEquality hypothesis applyEquality

Latex:
order-type-less()  \mmember{}  WFO\{i:l\}()  {}\mrightarrow{}  WFO\{i:l\}()  {}\mrightarrow{}  \mBbbP{}'



Date html generated: 2016_05_15-PM-04_13_32
Last ObjectModification: 2015_12_27-PM-02_59_30

Theory : general


Home Index