Nuprl Lemma : sp_refl_cl_cancel

[T:Type]. ∀[r:T ⟶ T ⟶ ℙ].  ((ro\) <≡>{T} r) supposing (st_anti_sym(T;r) and irrefl(T;r))


Definitions occuring in Statement :  s_part: E\ refl_cl: Eo xxst_anti_sym: st_anti_sym(T;R) xxirrefl: irrefl(T;R) binrel_eqv: E <≡>{T} E' uimplies: supposing a uall: [x:A]. B[x] prop: function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T xxirrefl: irrefl(T;R) irrefl: Irrefl(T;x,y.E[x; y]) not: ¬A implies:  Q false: False subtype_rel: A ⊆B prop: xxst_anti_sym: st_anti_sym(T;R) st_anti_sym: StAntiSym(T;x,y.R[x; y]) all: x:A. B[x] and: P ∧ Q
Lemmas referenced :  and_wf binrel_le_antisymmetry s_part_wf refl_cl_wf sp_refl_cl_le_rel rel_le_sp_refl_cl xxst_anti_sym_wf xxirrefl_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality lambdaEquality dependent_functionElimination voidElimination applyEquality hypothesis universeEquality rename lemma_by_obid independent_functionElimination because_Cache independent_isectElimination functionEquality cumulativity

\mforall{}[T:Type].  \mforall{}[r:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((r\msupzero{}\mbackslash{})  <\mequiv{}>\{T\}  r)  supposing  (st\_anti\_sym(T;r)  and  irrefl(T;r))

Date html generated: 2016_05_15-PM-00_02_10
Last ObjectModification: 2015_12_26-PM-11_25_37

Theory : gen_algebra_1

Home Index