### Nuprl Lemma : transitive-reflexive-closure_wf

`∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  (R^* ∈ A ⟶ A ⟶ ℙ)`

Proof

Definitions occuring in Statement :  transitive-reflexive-closure: `R^*` 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` transitive-reflexive-closure: `R^*` prop: `ℙ`
Lemmas referenced :  or_wf equal_wf transitive-closure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality hypothesis applyEquality functionExtensionality axiomEquality equalityTransitivity equalitySymmetry functionEquality universeEquality isect_memberEquality because_Cache

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (R\^{}*  \mmember{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{})

Date html generated: 2017_01_19-PM-02_17_38
Last ObjectModification: 2017_01_14-PM-04_22_25

Theory : relations2

Home Index