### 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