Nuprl Lemma : all-large_wf

[P:ℕ ⟶ ℙ]. (∀large(n).P[n] ∈ ℙ)


Proof




Definitions occuring in Statement :  all-large: large(n).P[n] nat: uall: [x:A]. B[x] prop: so_apply: x[s] member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  all-large: large(n).P[n] uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] implies:  Q prop: nat: so_apply: x[s]
Lemmas referenced :  exists_wf nat_wf all_wf le_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality functionEquality setElimination rename hypothesisEquality applyEquality axiomEquality equalityTransitivity equalitySymmetry cumulativity universeEquality

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (\mforall{}large(n).P[n]  \mmember{}  \mBbbP{})



Date html generated: 2016_05_15-PM-05_29_19
Last ObjectModification: 2015_12_27-PM-02_11_18

Theory : general


Home Index