Nuprl Lemma : atomic_wf

[a:ℤ]. (atomic(a) ∈ ℙ)


Proof




Definitions occuring in Statement :  atomic: atomic(a) uall: [x:A]. B[x] prop: member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T atomic: atomic(a) prop: and: P ∧ Q subtype_rel: A ⊆B
Lemmas referenced :  not_wf equal-wf-base int_subtype_base assoced_wf reducible_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule productEquality extract_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesisEquality applyEquality hypothesis baseClosed natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry Error :universeIsType

Latex:
\mforall{}[a:\mBbbZ{}].  (atomic(a)  \mmember{}  \mBbbP{})



Date html generated: 2019_06_20-PM-02_22_45
Last ObjectModification: 2018_09_26-PM-05_49_10

Theory : num_thy_1


Home Index