---

Step * 2 3 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. j ∈ nameset(I)
13. i ∈ nameset(I)
14. ↑isname(f i)
15. f i ∈ nameset(J)
16. ↑isname(f j)
17. f j ∈ nameset(J)
18. z2 ∈ extd-nameset([z2 / J])
19. (f i) = (f j) ∈ extd-nameset([z2 / J])
⊢ i = j ∈ nameset([z1 / I])
BY
{ ((DVar `f' THEN BackThruSomeHyp) THEN Auto) }

1
1. I : Cname List
2. J : Cname List
3. f : nameset(I) ⟶ extd-nameset(J)
4. ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
5. z1 : Cname
6. z2 : Cname
7. ¬(z2 ∈ J)
8. nameset(J) ⊆r extd-nameset([z2 / J])
9. i : nameset([z1 / I])
10. ¬(i = z1 ∈ Cname)
11. j : nameset([z1 / I])
12. ¬(j = z1 ∈ Cname)
13. j ∈ nameset(I)
14. i ∈ nameset(I)
15. ↑isname(f i)
16. f i ∈ nameset(J)
17. ↑isname(f j)
18. f j ∈ nameset(J)
19. z2 ∈ extd-nameset([z2 / J])
20. (f i) = (f j) ∈ extd-nameset([z2 / J])
⊢ (f i) = (f j) ∈ extd-nameset(J)

---

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.  \mneg{}(j  =  z1)
12.  j  \mmember{}  nameset(I)
13.  i  \mmember{}  nameset(I)
14.  \muparrow{}isname(f  i)
15.  f  i  \mmember{}  nameset(J)
16.  \muparrow{}isname(f  j)
17.  f  j  \mmember{}  nameset(J)
18.  z2  \mmember{}  extd-nameset([z2  /  J])
19.  (f  i)  =  (f  j)
\mvdash{}  i  =  j


By

---

Latex:
((DVar  `f'  THEN  BackThruSomeHyp)  THEN  Auto)

---

Home Index