Nuprl Lemma : le_antisymmetry

`∀[x,y:ℤ].  ((x ≤ y) `` (y ≤ x) `` (x = y ∈ ℤ))`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` le: `A ≤ B` implies: `P `` Q` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` or: `P ∨ Q` prop: `ℙ` less_than: `a < b` squash: `↓T` le: `A ≤ B` and: `P ∧ Q` not: `¬A` false: `False`
Lemmas referenced :  less-trichotomy le_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality unionElimination hypothesis isectElimination sqequalRule lambdaEquality axiomEquality intEquality isect_memberEquality because_Cache imageElimination productElimination independent_functionElimination voidElimination

Latex:
\mforall{}[x,y:\mBbbZ{}].    ((x  \mleq{}  y)  {}\mRightarrow{}  (y  \mleq{}  x)  {}\mRightarrow{}  (x  =  y))

Date html generated: 2019_06_20-AM-11_22_40
Last ObjectModification: 2018_08_17-AM-11_26_10

Theory : arithmetic

Home Index