---

Step * of Lemma extend-name-morph_wf

No Annotations
∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[z1,z2:Cname].  f[z1:=z2] ∈ name-morph([z1 / I];[z2 / J]) supposing ¬(z2 ∈ J)
BY
{ (ProveWfLemma THEN MemTypeCD) }

1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. z1 : Cname
5. z2 : Cname
6. ¬(z2 ∈ J)
⊢ λx.if eq-cname(x;z1) then z2 else f x fi  ∈ nameset([z1 / I]) ⟶ extd-nameset([z2 / J])

2
.....set predicate..... 
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. z1 : Cname
5. z2 : Cname
6. ¬(z2 ∈ J)
⊢ ∀i,j:nameset([z1 / I]).
    ((↑isname((λx.if eq-cname(x;z1) then z2 else f x fi ) i))
    ⇒ (↑isname((λx.if eq-cname(x;z1) then z2 else f x fi ) j))
    ⇒ (((λx.if eq-cname(x;z1) then z2 else f x fi ) i)
       = ((λx.if eq-cname(x;z1) then z2 else f x fi ) j)
       ∈ extd-nameset([z2 / J]))
    ⇒ (i = j ∈ nameset([z1 / I])))

3
.....wf..... 
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. z1 : Cname
5. z2 : Cname
6. ¬(z2 ∈ J)
7. f1 : nameset([z1 / I]) ⟶ extd-nameset([z2 / J])
⊢ istype(∀i,j:nameset([z1 / I]).
           ((↑isname(f1 i))
           ⇒ (↑isname(f1 j))
           ⇒ ((f1 i) = (f1 j) ∈ extd-nameset([z2 / J]))
           ⇒ (i = j ∈ nameset([z1 / I]))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[z1,z2:Cname].
    f[z1:=z2]  \mmember{}  name-morph([z1  /  I];[z2  /  J])  supposing  \mneg{}(z2  \mmember{}  J)


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD)

---

Home Index