Nuprl Lemma : rel_plus_iff

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,z:T.  (x R+ ⇐⇒ ∃y:T. ((x (R^*) y) ∧ (y z)))


Proof




Definitions occuring in Statement :  rel_plus: R+ rel_star: R^* uall: [x:A]. B[x] prop: infix_ap: y all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T infix_ap: y prop: rev_implies:  Q exists: x:A. B[x] so_lambda: λ2x.t[x] so_apply: x[s] or: P ∨ Q cand: c∧ B uimplies: supposing a subtype_rel: A ⊆B
Lemmas referenced :  rel_plus_wf exists_wf and_wf rel_star_wf rel_plus_implies rel_star_weakening rel-plus-rel-star rel-star-rel-plus
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation applyEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule hypothesis productElimination lambdaEquality functionEquality cumulativity universeEquality dependent_functionElimination independent_functionElimination unionElimination dependent_pairFormation because_Cache independent_isectElimination productEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    \mforall{}x,z:T.    (x  R\msupplus{}  z  \mLeftarrow{}{}\mRightarrow{}  \mexists{}y:T.  ((x  rel\_star(T;  R)  y)  \mwedge{}  (y  R  z)))



Date html generated: 2016_05_14-PM-03_53_47
Last ObjectModification: 2015_12_26-PM-06_56_33

Theory : relations2


Home Index