Nuprl Lemma : int_lower_wf

[i:ℤ]. ({...i} ∈ Type)


Proof




Definitions occuring in Statement :  int_lower: {...i} uall: [x:A]. B[x] member: t ∈ T int: universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int_lower: {...i} prop:
Lemmas referenced :  le_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule setEquality intEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType

Latex:
\mforall{}[i:\mBbbZ{}].  (\{...i\}  \mmember{}  Type)



Date html generated: 2019_06_20-AM-11_23_32
Last ObjectModification: 2018_09_26-AM-10_58_18

Theory : arithmetic


Home Index