### Nuprl Lemma : binrel_le_antisymmetry

`∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R ≡>{T} R') `` (R' ≡>{T} R) `` (R <≡>{T} R'))`

Proof

Definitions occuring in Statement :  binrel_le: `E ≡>{T} E'` binrel_eqv: `E <≡>{T} E'` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  binrel_eqv: `E <≡>{T} E'` binrel_le: `E ≡>{T} E'` uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` prop: `ℙ`
Lemmas referenced :  implies_antisymmetry subtype_rel_self istype-universe
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality independent_functionElimination hypothesis dependent_functionElimination Error :universeIsType,  instantiate universeEquality because_Cache Error :inhabitedIsType,  Error :functionIsType

Latex:
\mforall{}[T:Type].  \mforall{}[R,R':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((R  \mequiv{}>\{T\}  R')  {}\mRightarrow{}  (R'  \mequiv{}>\{T\}  R)  {}\mRightarrow{}  (R  <\mequiv{}>\{T\}  R'))

Date html generated: 2019_06_20-PM-02_02_24
Last ObjectModification: 2019_01_10-PM-09_36_19

Theory : relations2

Home Index