Nuprl Lemma : regextW_wf
∀[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[G:i:T ⟶ j:set-dom(f i) ⟶ T]. ∀[t:T]. (regextW(G;t) ∈ coW(T;x.set-dom(f x)))
Proof
Definitions occuring in Statement :
regextW: regextW(G;t),
set-dom: set-dom(s),
coSet: coSet{i:l},
coW: coW(A;a.B[a]),
uall: ∀[x:A]. B[x],
member: t ∈ T,
apply: f a,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
regextW: regextW(G;t),
so_lambda: λ2x.t[x],
so_apply: x[s],
Wsup: Wsup(a;b)
Lemmas referenced :
fix_wf_coW_parameter,
set-dom_wf,
coSet_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
thin,
instantiate,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
because_Cache,
cumulativity,
hypothesisEquality,
sqequalRule,
lambdaEquality,
applyEquality,
hypothesis,
isect_memberEquality,
dependent_pairEquality,
functionEquality,
universeEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[T:Type]. \mforall{}[f:T {}\mrightarrow{} coSet\{i:l\}]. \mforall{}[G:i:T {}\mrightarrow{} j:set-dom(f i) {}\mrightarrow{} T]. \mforall{}[t:T].
(regextW(G;t) \mmember{} coW(T;x.set-dom(f x)))
Date html generated:
2019_10_31-AM-06_34_24
Last ObjectModification:
2018_08_04-PM-04_13_56
Theory : constructive!set!theory
Home
Index