Nuprl Lemma : name-morph_subtype_remove1

[I,J:Cname List]. ∀[x:Cname]. ∀[f:name-morph(I;J)].
  (f ∈ name-morph(I-[x];J-[f x])) supposing ((↑isname(f x)) and (x ∈ I))


Proof




Definitions occuring in Statement :  name-morph: name-morph(I;J) isname: isname(z) cname_deq: CnameDeq coordinate_name: Cname list-diff: as-bs l_member: (x ∈ l) cons: [a b] nil: [] list: List assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T apply: a
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a name-morph: name-morph(I;J) nameset: nameset(L) prop: uiff: uiff(P;Q) and: P ∧ Q all: x:A. B[x] subtype_rel: A ⊆B implies:  Q not: ¬A false: False iff: ⇐⇒ Q rev_implies:  Q sq_type: SQType(T) guard: {T} coordinate_name: Cname int_upper: {i...} satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top decidable: Dec(P) or: P ∨ Q le: A ≤ B squash: T cand: c∧ B so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  assert-isname nameset_wf l_member_wf coordinate_name_wf assert_wf isname_wf name-morph_wf list_wf nameset_subtype list-diff_wf cname_deq_wf cons_wf nil_wf list-diff-subset member-list-diff member_singleton equal_wf subtype_base_sq nameset_subtype_base satisfiable-full-omega-tt intformnot_wf intformeq_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma decidable__equal_int int_formula_prop_wf le_wf extd-nameset_wf nameset_subtype_extd-nameset decidable__assert set_subtype_base int_subtype_base not-assert-isname nsub2_subtype_extd-nameset all_wf extd-nameset_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename extract_by_obid isectElimination hypothesisEquality applyEquality functionExtensionality hypothesis dependent_set_memberEquality productElimination independent_isectElimination sqequalRule axiomEquality equalityTransitivity equalitySymmetry because_Cache isect_memberEquality lambdaFormation dependent_functionElimination independent_functionElimination independent_pairFormation promote_hyp instantiate cumulativity natural_numberEquality dependent_pairFormation lambdaEquality int_eqEquality intEquality voidElimination voidEquality unionElimination computeAll applyLambdaEquality imageMemberEquality baseClosed imageElimination functionEquality universeEquality

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[x:Cname].  \mforall{}[f:name-morph(I;J)].
    (f  \mmember{}  name-morph(I-[x];J-[f  x]))  supposing  ((\muparrow{}isname(f  x))  and  (x  \mmember{}  I))



Date html generated: 2017_10_05-AM-10_05_39
Last ObjectModification: 2017_07_28-AM-11_16_07

Theory : cubical!sets


Home Index