Nuprl Lemma : regextfun_wf2

[T:Type]. ∀[f:T ⟶ Set{i:l}]. ∀[w:W(T;x.set-dom(f x))].  (regextfun(f;w) ∈ Set{i:l})


Proof




Definitions occuring in Statement :  regextfun: regextfun(f;w) Set: Set{i:l} set-dom: set-dom(s) W: W(A;a.B[a]) uall: [x:A]. B[x] member: t ∈ T apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  sq_stable: SqStable(P) le: A ≤ B sq_type: SQType(T) cand: c∧ B pcw-step-agree: StepAgree(s;p1;w) isl: isl(x) pi2: snd(t) pcw-steprel: StepRel(s1;s2) param-W-rel: param-W-rel(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b];par;w) W-rel: W-rel(A;a.B[a];w) nat_plus: + pi1: fst(t) ext-family: F ≡ G so_apply: x[s1;s2;s3] so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2] so_lambda: λ2y.t[x; y] it: unit: Unit ext-eq: A ≡ B btrue: tt bfalse: ff ifthenelse: if then else fi  assert: b isr: isr(x) squash: T true: True less_than': less_than'(a;b) less_than: a < b spreadn: spread3 pcw-step: pcw-step(P;p.A[p];p,a.B[p; a];p,a,b.C[p; a; b]) cw-step: cw-step(A;a.B[a]) top: Top false: False exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A uimplies: supposing a or: P ∨ Q decidable: Dec(P) ge: i ≥  lelt: i ≤ j < k int_seg: {i..j-} nat: pcw-pp-barred: Barred(pp) implies:  Q prop: and: P ∧ Q guard: {T} all: x:A. B[x] Wsup: Wsup(a;b) regextfun: regextfun(f;w) so_apply: x[s] subtype_rel: A ⊆B so_lambda: λ2x.t[x] member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  sq_stable__le int_seg_subtype subtype_rel_function int_formula_prop_eq_lemma intformeq_wf decidable__equal_int int_subtype_base le_wf set_subtype_base nat_wf subtype_base_sq subtype_rel_dep_function pcw-steprel_wf param-co-W_wf it_wf unit_wf2 param-co-W-ext W-ext int_term_value_add_lemma itermAdd_wf add-subtract-cancel equal_wf true_wf false_wf less_than_wf top_wf lelt_wf decidable__lt int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermSubtract_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le nat_properties subtract_wf int_seg_wf subtype_rel_self W-elimination-facts mk-set_wf Set_wf set-subtype-coSet set-dom_wf W_wf
Rules used in proof :  applyLambdaEquality hyp_replacement productEquality unionEquality inlEquality dependent_pairEquality equalityElimination hypothesis_subsumption promote_hyp int_eqReduceTrueSq addEquality axiomEquality imageElimination baseClosed imageMemberEquality sqequalAxiom lessCases lambdaFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation approximateComputation independent_isectElimination unionElimination independent_pairFormation dependent_set_memberEquality rename setElimination natural_numberEquality functionExtensionality independent_functionElimination instantiate equalitySymmetry equalityTransitivity strong_bar_Induction productElimination dependent_functionElimination because_Cache universeEquality cumulativity functionEquality applyEquality lambdaEquality sqequalRule hypothesisEquality thin isectElimination extract_by_obid introduction hypothesis sqequalHypSubstitution cut isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  Set\{i:l\}].  \mforall{}[w:W(T;x.set-dom(f  x))].    (regextfun(f;w)  \mmember{}  Set\{i:l\})



Date html generated: 2018_07_29-AM-10_07_08
Last ObjectModification: 2018_07_20-PM-04_50_55

Theory : constructive!set!theory


Home Index