Nuprl Lemma : valuation-exists-ext
∀x:formula(). ∀v0:{a:formula()| a ⊆ x ∧ (↑pvar?(a))} ⟶ 𝔹. (∃f:{a:formula()| a ⊆ x} ⟶ 𝔹 [valuation(v0;x;f)])
Proof
Definitions occuring in Statement :
valuation: valuation(v0;x;f),
psub: a ⊆ b,
pvar?: pvar?(v),
formula: formula(),
assert: ↑b,
bool: 𝔹,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
and: P ∧ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
member: t ∈ T,
valuation-exists,
uniform-comp-nat-induction
Lemmas referenced :
valuation-exists,
uniform-comp-nat-induction
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}x:formula(). \mforall{}v0:\{a:formula()| a \msubseteq{} x \mwedge{} (\muparrow{}pvar?(a))\} {}\mrightarrow{} \mBbbB{}.
(\mexists{}f:\{a:formula()| a \msubseteq{} x\} {}\mrightarrow{} \mBbbB{} [valuation(v0;x;f)])
Date html generated:
2018_05_21-PM-08_54_13
Last ObjectModification:
2018_05_19-PM-05_06_52
Theory : general
Home
Index