Nuprl Lemma : rel_star_weakening

[T:Type]. ∀[x,y:T]. ∀[R:T ⟶ T ⟶ ℙ].  (R^*) supposing y ∈ T


Proof




Definitions occuring in Statement :  rel_star: R^* uimplies: supposing a uall: [x:A]. B[x] prop: infix_ap: y function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T rel_star: R^* infix_ap: y exists: x:A. B[x] nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: rel_exp: R^n ifthenelse: if then else fi  eq_int: (i =z j) btrue: tt
Lemmas referenced :  false_wf le_wf rel_exp_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction axiomEquality hypothesis thin rename sqequalRule dependent_pairFormation dependent_set_memberEquality natural_numberEquality independent_pairFormation lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality applyEquality functionEquality cumulativity universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:T].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    x  rel\_star(T;  R)  y  supposing  x  =  y



Date html generated: 2016_05_14-AM-06_04_07
Last ObjectModification: 2015_12_26-AM-11_33_24

Theory : relations


Home Index