---

Step * 1 4 2 1 1 of Lemma face-map-comp2

.....wf..... 
1. A : Cname List
2. B : Cname List
3. g : name-morph(A;B)
4. x : Cname
5. (x ∈ A)
6. y : Cname
7. (y ∈ A)
8. i : ℕ2
9. j : ℕ2
10. ↑isname(g x)
11. ↑isname(g y)
12. ¬(x = y ∈ Cname)
13. g y ∈ nameset(B)
14. g x ∈ nameset(B)
⊢ g ∈ name-morph(A-[x];B-[g x])
BY
{ (BLemma `name-morph_subtype_remove1` THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  A  :  Cname  List
2.  B  :  Cname  List
3.  g  :  name-morph(A;B)
4.  x  :  Cname
5.  (x  \mmember{}  A)
6.  y  :  Cname
7.  (y  \mmember{}  A)
8.  i  :  \mBbbN{}2
9.  j  :  \mBbbN{}2
10.  \muparrow{}isname(g  x)
11.  \muparrow{}isname(g  y)
12.  \mneg{}(x  =  y)
13.  g  y  \mmember{}  nameset(B)
14.  g  x  \mmember{}  nameset(B)
\mvdash{}  g  \mmember{}  name-morph(A-[x];B-[g  x])


By

---

Latex:
(BLemma  `name-morph\_subtype\_remove1`  THEN  Auto)

---

Home Index