Nuprl Lemma : rel-immediate-property
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (sum_of_torder(T;R) 
⇒ (∀x,y,x',y':T.  ((R x y) 
⇒ (R! y' y) 
⇒ ((R x y') ∨ (x = y' ∈ T)))))
Proof
Definitions occuring in Statement : 
sum_of_torder: sum_of_torder(T;R)
, 
rel-immediate: R!
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
or: P ∨ Q
, 
apply: f a
, 
function: x:A ⟶ B[x]
, 
universe: Type
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
prop: ℙ
, 
member: t ∈ T
, 
sum_of_torder: sum_of_torder(T;R)
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
uall: ∀[x:A]. B[x]
, 
rel-immediate: R!
, 
and: P ∧ Q
, 
or: P ∨ Q
, 
cand: A c∧ B
, 
subtype_rel: A ⊆r B
, 
not: ¬A
, 
false: False
Lemmas referenced : 
subtype_rel_self, 
rel-immediate_wf, 
sum_of_torder_wf
Rules used in proof : 
universeEquality, 
cumulativity, 
functionEquality, 
hypothesis, 
hypothesisEquality, 
thin, 
isectElimination, 
lemma_by_obid, 
cut, 
applyEquality, 
sqequalHypSubstitution, 
lambdaFormation, 
isect_memberFormation, 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalSubstitution, 
sqequalRule, 
productElimination, 
dependent_functionElimination, 
independent_functionElimination, 
inlFormation_alt, 
independent_pairFormation, 
productIsType, 
universeIsType, 
instantiate, 
introduction, 
extract_by_obid, 
because_Cache, 
unionElimination, 
equalityIstype, 
inhabitedIsType, 
inrFormation_alt, 
voidElimination
Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (sum\_of\_torder(T;R)  {}\mRightarrow{}  (\mforall{}x,y,x',y':T.    ((R  x  y)  {}\mRightarrow{}  (R!  y'  y)  {}\mRightarrow{}  ((R  x  y')  \mvee{}  (x  =  y')))))
Date html generated:
2020_05_20-AM-08_10_11
Last ObjectModification:
2020_01_17-PM-05_50_27
Theory : general
Home
Index