### Nuprl Lemma : cond_rel_implies_wf

`∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (when P, R1 => R2 ∈ ℙ)`

Proof

Definitions occuring in Statement :  cond_rel_implies: `when P, R1 => R2` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` cond_rel_implies: `when P, R1 => R2` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` infix_ap: `x f y` so_apply: `x[s]`
Lemmas referenced :  all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality functionEquality applyEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry Error :inhabitedIsType,  isect_memberEquality cumulativity universeEquality Error :functionIsType,  Error :universeIsType,  because_Cache

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (when  P,  R1  =>  R2  \mmember{}  \mBbbP{})

Date html generated: 2019_06_20-PM-00_30_30
Last ObjectModification: 2018_09_26-PM-00_39_28

Theory : relations

Home Index