Nuprl Lemma : unique-awf
∀[A,I:Type].
∀G:awf-system{i:l}(I;A)
(∃s:I ⟶ awf(A) [((∀i:I. ((s i) = (G s i) ∈ awf(A)))
∧ (∀s':I ⟶ awf(A). ((∀i:I. ((s' i) = (G s' i) ∈ awf(A))) ⇒ (s' = s ∈ (I ⟶ awf(A))))))])
Proof
Definitions occuring in Statement :
awf-system: awf-system{i:l}(I;A),
awf: awf(T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
awf-system: awf-system{i:l}(I;A),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
member: t ∈ T,
so_apply: x[s],
uimplies: b supposing a,
implies: P ⇒ Q,
subtype_rel: A ⊆r B,
or: P ∨ Q,
awf: awf(T),
and: P ∧ Q,
prop: ℙ,
cand: A c∧ B,
ext-eq: A ≡ B,
exists!: ∃!x:T. P[x],
exists: ∃x:A. B[x],
sq_exists: ∃x:A [B[x]],
squash: ↓T,
true: True,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q
Lemmas referenced :
unique-corec-solution,
list_wf,
continuous-monotone-union,
continuous-monotone-constant,
continuous-monotone-list,
continuous-monotone-id,
isect2_subtype_rel3,
top_wf,
subtype_rel_wf,
awf_wf,
set_wf,
corec_wf,
isect2_wf,
isect2_decomp,
corec-ext,
subtype_rel_self,
subtype_rel_dep_function,
equal_wf,
squash_wf,
true_wf,
iff_weakening_equal,
all_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
isect_memberFormation,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
lambdaEquality,
unionEquality,
hypothesisEquality,
hypothesis,
universeEquality,
independent_isectElimination,
dependent_functionElimination,
independent_functionElimination,
isect_memberEquality,
applyEquality,
instantiate,
because_Cache,
cumulativity,
functionEquality,
setElimination,
rename,
inlFormation,
equalityTransitivity,
equalitySymmetry,
isectEquality,
setEquality,
productEquality,
productElimination,
independent_pairFormation,
dependent_set_memberEquality,
functionExtensionality,
dependent_set_memberFormation,
imageElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed
Latex:
\mforall{}[A,I:Type].
\mforall{}G:awf-system\{i:l\}(I;A)
(\mexists{}s:I {}\mrightarrow{} awf(A) [((\mforall{}i:I. ((s i) = (G s i)))
\mwedge{} (\mforall{}s':I {}\mrightarrow{} awf(A). ((\mforall{}i:I. ((s' i) = (G s' i))) {}\mRightarrow{} (s' = s))))])
Date html generated:
2019_10_15-AM-11_33_46
Last ObjectModification:
2018_08_21-AM-01_09_23
Theory : general
Home
Index