Nuprl Lemma : fpf-rename-cap3

[A,C,B:Type]. ∀[eqa:EqDecider(A)]. ∀[eqc,eqc':EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B]. ∀[a:A]. ∀[z:B]. ∀[c:C].
  (rename(r;f)(c)?z f(a)?z ∈ B) supposing ((c (r a) ∈ C) and Inj(A;C;r))


Definitions occuring in Statement :  fpf-rename: rename(r;f) fpf-cap: f(x)?z fpf: a:A fp-> B[a] deq: EqDecider(T) inject: Inj(A;B;f) uimplies: supposing a uall: [x:A]. B[x] apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] implies:  Q
Lemmas referenced :  equal_wf fpf-cap_wf inject_wf fpf_wf deq_wf fpf-rename-cap2 fpf-rename_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis thin hyp_replacement equalitySymmetry applyLambdaEquality extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality sqequalRule lambdaEquality because_Cache applyEquality functionExtensionality isect_memberEquality axiomEquality equalityTransitivity functionEquality universeEquality independent_isectElimination lambdaFormation dependent_functionElimination independent_functionElimination

\mforall{}[A,C,B:Type].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[eqc,eqc':EqDecider(C)].  \mforall{}[r:A  {}\mrightarrow{}  C].  \mforall{}[f:a:A  fp->  B].  \mforall{}[a:A].
\mforall{}[z:B].  \mforall{}[c:C].
    (rename(r;f)(c)?z  =  f(a)?z)  supposing  ((c  =  (r  a))  and  Inj(A;C;r))

Date html generated: 2018_05_21-PM-09_27_19
Last ObjectModification: 2018_02_09-AM-10_22_29

Theory : finite!partial!functions

Home Index