---

Step * 2 2 of Lemma extend-name-morph_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. nameset(J) ⊆r extd-nameset([z2 / J])
8. i : nameset([z1 / I])
9. ¬(i = z1 ∈ Cname)
10. j : nameset([z1 / I])
11. j = z1 ∈ Cname
12. i ∈ nameset(I)
13. ↑isname(f i)
14. f i ∈ nameset(J)
15. True
16. z2 ∈ extd-nameset([z2 / J])
17. (f i) = z2 ∈ extd-nameset([z2 / J])
⊢ i = j ∈ nameset([z1 / I])
BY
{ (HypSubst' (-1) (-4) THEN MemTypeHD (-4) THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  f  :  name-morph(I;J)
4.  z1  :  Cname
5.  z2  :  Cname
6.  \mneg{}(z2  \mmember{}  J)
7.  nameset(J)  \msubseteq{}r  extd-nameset([z2  /  J])
8.  i  :  nameset([z1  /  I])
9.  \mneg{}(i  =  z1)
10.  j  :  nameset([z1  /  I])
11.  j  =  z1
12.  i  \mmember{}  nameset(I)
13.  \muparrow{}isname(f  i)
14.  f  i  \mmember{}  nameset(J)
15.  True
16.  z2  \mmember{}  extd-nameset([z2  /  J])
17.  (f  i)  =  z2
\mvdash{}  i  =  j


By

---

Latex:
(HypSubst'  (-1)  (-4)  THEN  MemTypeHD  (-4)  THEN  Auto)

---

Home Index