Nuprl Lemma : transitive-closure-minimal-ext

[A:Type]. ∀[R,Q:A ⟶ A ⟶ ℙ].  (R =>  Trans(A;x,y.x y)  TC(R) => Q)


Proof




Definitions occuring in Statement :  transitive-closure: TC(R) rel_implies: R1 => R2 trans: Trans(T;x,y.E[x; y]) uall: [x:A]. B[x] prop: infix_ap: y implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  member: t ∈ T spreadn: spread3 transitive-closure-minimal
Lemmas referenced :  transitive-closure-minimal
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

Latex:
\mforall{}[A:Type].  \mforall{}[R,Q:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (R  =>  Q  {}\mRightarrow{}  Trans(A;x,y.x  Q  y)  {}\mRightarrow{}  TC(R)  =>  Q)



Date html generated: 2018_05_21-PM-00_51_42
Last ObjectModification: 2018_05_19-AM-06_40_14

Theory : relations2


Home Index