### Nuprl Lemma : rel_plus-of-restriction

`∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].  R|P+ => R+|P`

Proof

Definitions occuring in Statement :  rel_plus: `R+` rel-restriction: `R|P` rel_implies: `R1 => R2` uall: `∀[x:A]. B[x]` prop: `ℙ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` implies: `P `` Q` rel-restriction: `R|P` rel_implies: `R1 => R2` infix_ap: `x f y` all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B`
Lemmas referenced :  rel_plus_minimal rel-restriction_wf rel_plus_wf and_wf rel-rel-plus restriction-of-transitive rel_plus_trans
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation functionEquality cumulativity hypothesisEquality universeEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis sqequalRule independent_functionElimination lambdaFormation productElimination independent_pairFormation applyEquality dependent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    R|P\msupplus{}  =>  R\msupplus{}|P

Date html generated: 2016_05_14-PM-03_55_32
Last ObjectModification: 2015_12_26-PM-06_55_38

Theory : relations2

Home Index