Nuprl Lemma : rel-preserving_wf

`∀[T1,T2:Type]. ∀[R1:T1 ⟶ T1 ⟶ Type]. ∀[R2:T2 ⟶ T2 ⟶ Type]. ∀[f:T2 ⟶ T1].  (λx.f[x]:T2->T1 takes R2 into R1*) ∈ ℙ)`

Proof

Definitions occuring in Statement :  rel-preserving: `λx.f[x]:T2->T1 takes R2 into R1*)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` rel-preserving: `λx.f[x]:T2->T1 takes R2 into R1*)` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` infix_ap: `x f y` subtype_rel: `A ⊆r B` so_apply: `x[s]`
Lemmas referenced :  all_wf rel_star_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality functionEquality applyEquality hypothesis because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality cumulativity universeEquality

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[R1:T1  {}\mrightarrow{}  T1  {}\mrightarrow{}  Type].  \mforall{}[R2:T2  {}\mrightarrow{}  T2  {}\mrightarrow{}  Type].  \mforall{}[f:T2  {}\mrightarrow{}  T1].
(\mlambda{}x.f[x]:T2->T1  takes  R2  into  R1*)  \mmember{}  \mBbbP{})

Date html generated: 2016_05_15-PM-05_40_22
Last ObjectModification: 2015_12_27-PM-02_05_46

Theory : general

Home Index