### Nuprl Lemma : rel_star_functionality_wrt_rel_implies

`∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2 `` R1^* => R2^*)`

Proof

Definitions occuring in Statement :  rel_star: `R^*` rel_implies: `R1 => R2` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` rel_implies: `R1 => R2` all: `∀x:A. B[x]` member: `t ∈ T` infix_ap: `x f y` subtype_rel: `A ⊆r B` prop: `ℙ` guard: `{T}`
Lemmas referenced :  rel_star_monotonic rel_star_wf subtype_rel_self rel_implies_wf istype-universe
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  Error :universeIsType,  applyEquality sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule instantiate universeEquality because_Cache Error :inhabitedIsType,  Error :functionIsType,  dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (R1  =>  R2  {}\mRightarrow{}  rel\_star(T;  R1)  =>  rel\_star(T;  R2))

Date html generated: 2019_06_20-PM-02_02_22
Last ObjectModification: 2019_01_17-PM-10_04_01

Theory : relations2

Home Index