Nuprl Lemma : transitive-reflexive-closure_transitivity

`∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀x,y,z:A.  ((x R^* y) `` (y R^* z) `` (x R^* z))`

Proof

Definitions occuring in Statement :  transitive-reflexive-closure: `R^*` uall: `∀[x:A]. B[x]` prop: `ℙ` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` transitive-reflexive-closure: `R^*` infix_ap: `x f y` or: `P ∨ Q` member: `t ∈ T` subtype_rel: `A ⊆r B` prop: `ℙ` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` utrans: `UniformlyTrans(T;x,y.E[x; y])`
Lemmas referenced :  transitive-reflexive-closure_wf iff_weakening_equal equal_wf transitive-closure-transitive
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut hypothesis addLevel sqequalHypSubstitution sqequalRule unionElimination thin applyEquality introduction extract_by_obid isectElimination cumulativity hypothesisEquality functionExtensionality because_Cache lambdaEquality universeEquality equalityTransitivity equalitySymmetry independent_isectElimination productElimination independent_functionElimination levelHypothesis functionEquality inrFormation

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,y,z:A.    ((x  R\^{}*  y)  {}\mRightarrow{}  (y  R\^{}*  z)  {}\mRightarrow{}  (x  R\^{}*  z))

Date html generated: 2017_01_19-PM-02_17_45
Last ObjectModification: 2017_01_14-PM-04_59_10

Theory : relations2

Home Index