Nuprl Lemma : predicate-or-shift_wf
∀[T:Type]. ∀[A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ∀[x:T]. (A[x] ∈ n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ)
Proof
Definitions occuring in Statement :
predicate-or-shift: A[x],
int_seg: {i..j-},
nat: ℕ,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
function: x:A ⟶ B[x],
natural_number: $n,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
predicate-or-shift: A[x],
prop: ℙ,
nat: ℕ
Lemmas referenced :
or_wf,
predicate-shift_wf,
int_seg_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
lambdaEquality,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
applyEquality,
hypothesisEquality,
universeEquality,
hypothesis,
functionEquality,
natural_numberEquality,
setElimination,
rename,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality,
because_Cache,
cumulativity
Latex:
\mforall{}[T:Type]. \mforall{}[A:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} \mBbbP{}]. \mforall{}[x:T]. (A[x] \mmember{} n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} \mBbbP{})
Date html generated:
2016_05_14-PM-04_07_15
Last ObjectModification:
2015_12_26-PM-07_55_09
Theory : fan-theorem
Home
Index