### Nuprl Lemma : transitive-reflexive-closure-cases

`∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀x,y:A.  ((x R^* y) `` ((x = y ∈ A) ∨ (∃z:A. ((x R z) ∧ (z R^* y)))))`

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]` exists: `∃x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
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` prop: `ℙ` so_lambda: `λ2x.t[x]` and: `P ∧ Q` subtype_rel: `A ⊆r B` so_apply: `x[s]` guard: `{T}` exists: `∃x:A. B[x]` cand: `A c∧ B`
Lemmas referenced :  exists_wf transitive-reflexive-closure_wf transitive-closure-cases equal_wf transitive-closure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution sqequalRule unionElimination thin inlFormation hypothesis cut introduction extract_by_obid isectElimination cumulativity hypothesisEquality lambdaEquality productEquality applyEquality functionExtensionality universeEquality because_Cache inrFormation dependent_functionElimination independent_functionElimination functionEquality dependent_pairFormation independent_pairFormation productElimination promote_hyp

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

Date html generated: 2017_01_19-PM-02_17_41
Last ObjectModification: 2017_01_14-PM-04_28_39

Theory : relations2

Home Index