### Nuprl Lemma : order_functionality_wrt_iff

`∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (R[x;y] `⇐⇒` R'[x;y])) `` (Order(T;x,y.R[x;y]) `⇐⇒` Order(T;x,y.R'[x;y])))`

Proof

Definitions occuring in Statement :  order: `Order(T;x,y.R[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` order: `Order(T;x,y.R[x; y])` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` uimplies: `b supposing a`
Lemmas referenced :  order_wf all_wf iff_wf anti_sym_wf refl_functionality_wrt_iff trans_functionality_wrt_iff iff_weakening_uiff anti_sym_functionality_wrt_iff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  lambdaFormation independent_pairFormation sqequalHypSubstitution cut introduction extract_by_obid isectElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality hypothesis Error :inhabitedIsType,  Error :functionIsType,  Error :universeIsType,  universeEquality because_Cache productElimination independent_functionElimination dependent_functionElimination promote_hyp independent_isectElimination

Latex:
\mforall{}[T:Type].  \mforall{}[R,R':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}x,y:T.    (R[x;y]  \mLeftarrow{}{}\mRightarrow{}  R'[x;y]))  {}\mRightarrow{}  (Order(T;x,y.R[x;y])  \mLeftarrow{}{}\mRightarrow{}  Order(T;x,y.R'[x;y])))

Date html generated: 2019_06_20-PM-00_29_30
Last ObjectModification: 2018_09_26-AM-11_53_43

Theory : rel_1

Home Index