Nuprl Lemma : le_witness
∀[i,j:ℤ]. ∀[x:i ≤ j]. (x = <λx.x, Ax, Ax> ∈ (i ≤ j))
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
le: A ≤ B,
lambda: λx.A[x],
pair: <a, b>,
int: ℤ,
equal: s = t ∈ T,
axiom: Ax
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
prop: ℙ,
le: A ≤ B,
and: P ∧ Q,
not: ¬A,
implies: P ⇒ Q,
false: False
Lemmas referenced :
le_wf,
istype-int,
less_than'_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
hypothesis,
Error :universeIsType,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
Error :isect_memberEquality_alt,
axiomEquality,
because_Cache,
Error :inhabitedIsType,
productElimination,
equalityElimination,
independent_pairEquality,
Error :functionExtensionality_alt,
independent_functionElimination,
voidElimination
Latex:
\mforall{}[i,j:\mBbbZ{}]. \mforall{}[x:i \mleq{} j]. (x = <\mlambda{}x.x, Ax, Ax>)
Date html generated:
2019_06_20-AM-11_22_27
Last ObjectModification:
2018_10_01-PM-07_00_30
Theory : arithmetic
Home
Index