Nuprl Lemma : pertype_wf

[R:Base ⟶ Base ⟶ ℙ]
  (pertype(R) ∈ Type) supposing ((∀x,y:Base.  (R[x;y]  R[y;x])) and (∀x,y,z:Base.  (R[x;y]  R[y;z]  R[x;z])))


Definitions occuring in Statement :  pertype: pertype(R) uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] implies:  Q member: t ∈ T function: x:A ⟶ B[x] base: Base universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: so_lambda: λ2x.t[x] implies:  Q so_apply: x[s1;s2] so_apply: x[s] subtype_rel: A ⊆B guard: {T} all: x:A. B[x]
Lemmas referenced :  all_wf base_wf subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry extract_by_obid isectElimination thin lambdaEquality functionEquality applyEquality hypothesisEquality isect_memberEquality because_Cache cumulativity universeEquality instantiate pertypeEquality dependent_functionElimination independent_functionElimination

\mforall{}[R:Base  {}\mrightarrow{}  Base  {}\mrightarrow{}  \mBbbP{}]
    (pertype(R)  \mmember{}  Type)  supposing 
          ((\mforall{}x,y:Base.    (R[x;y]  {}\mRightarrow{}  R[y;x]))  and 
          (\mforall{}x,y,z:Base.    (R[x;y]  {}\mRightarrow{}  R[y;z]  {}\mRightarrow{}  R[x;z])))

Date html generated: 2019_06_20-AM-11_29_51
Last ObjectModification: 2018_08_07-PM-02_29_01

Theory : per!type!1

Home Index