Nuprl Lemma : double-negation-shift_wf

A:ℕ ⟶ ℙ(DNSi.A[i] ∈ ℙ)


Proof




Definitions occuring in Statement :  double-negation-shift: DNSi.A[i] nat: prop: so_apply: x[s] all: x:A. B[x] member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T double-negation-shift: DNSi.A[i] implies:  Q prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  all_wf nat_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule functionEquality lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality applyEquality hypothesisEquality cumulativity universeEquality

Latex:
\mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  (DNSi.A[i]  \mmember{}  \mBbbP{})



Date html generated: 2016_05_15-PM-03_20_43
Last ObjectModification: 2015_12_27-PM-01_04_00

Theory : general


Home Index