---

Step * 2 2 of Lemma extend-name-morph-face-map


1. I : {Cname List}
2. K : Cname List
3. f : name-morph(I;K)
4. z : ℤ
5. 2 ≤ z
6. x : ℤ
7. 2 ≤ x
8. i : ℤ
9. 0 ≤ i
10. i < 2
11. ¬(x ∈ K)
12. ¬(z ∈ I)
13. x1 : ℤ
14. 2 ≤ x1
15. (x1 ∈ [z / I])
16. x1 = z ∈ ℤ
17. x1 = z ∈ ℤ
⊢ z = z ∈ Cname
BY
{ (D -2 THEN HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  \{Cname  List\}
2.  K  :  Cname  List
3.  f  :  name-morph(I;K)
4.  z  :  \mBbbZ{}
5.  2  \mleq{}  z
6.  x  :  \mBbbZ{}
7.  2  \mleq{}  x
8.  i  :  \mBbbZ{}
9.  0  \mleq{}  i
10.  i  <  2
11.  \mneg{}(x  \mmember{}  K)
12.  \mneg{}(z  \mmember{}  I)
13.  x1  :  \mBbbZ{}
14.  2  \mleq{}  x1
15.  (x1  \mmember{}  [z  /  I])
16.  x1  =  z
17.  x1  =  z
\mvdash{}  z  =  z


By

---

Latex:
(D  -2  THEN  HypSubst'  (-1)  0  THEN  Auto)

---

Home Index