---

Step * 3 of Lemma extend-face-map-same


1. I : Cname List
2. x : Cname
3. y : Cname
4. i : ℕ2
5. ¬(y = x ∈ Cname)
6. ¬(y ∈ I)
⊢ (x:=i)[y:=y] = (x:=i) ∈ (nameset([y / I]) ⟶ extd-nameset([y / I]-[x]))
BY
{ ((FunExt THENA Auto)
   THEN RepUR ``extend-name-morph face-map`` 0
   THEN (BoolCase ⌜(x1 =z x)⌝⋅ THENA Auto)
   THEN (BoolCase ⌜eq-cname(x1;y)⌝⋅ THENA Auto)) }

1
1. I : {Cname List}
2. x : ℤ
3. 2 ≤ x
4. y : ℤ
5. 2 ≤ y
6. i : ℤ
7. 0 ≤ i
8. i < 2
9. ¬(y ∈ I)
10. x1 : ℤ
11. 2 ≤ x1
12. (x1 ∈ [y / I])
13. x1 = x ∈ ℤ
14. x1 = y ∈ ℤ
15. 2 ≤ x1
16. y = x ∈ ℤ
⊢ x = x ∈ Cname

2
1. I : Cname List
2. x : Cname
3. y : Cname
4. i : ℕ2
5. ¬(y = x ∈ Cname)
6. ¬(y ∈ I)
7. x1 : nameset([y / I])
8. ¬(x1 = y ∈ Cname)
9. x1 = x ∈ ℤ
⊢ i = i ∈ extd-nameset([y / I]-[x])

3
1. I : Cname List
2. x : Cname
3. y : Cname
4. i : ℕ2
5. ¬(y = x ∈ Cname)
6. ¬(y ∈ I)
7. x1 : nameset([y / I])
8. x1 ≠ x
9. x1 = y ∈ Cname
⊢ y = x1 ∈ extd-nameset([y / I]-[x])

4
1. I : Cname List
2. x : Cname
3. y : Cname
4. i : ℕ2
5. ¬(y = x ∈ Cname)
6. ¬(y ∈ I)
7. x1 : nameset([y / I])
8. ¬(x1 = y ∈ Cname)
9. x1 ≠ x
⊢ x1 = x1 ∈ extd-nameset([y / I]-[x])

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  Cname
3.  y  :  Cname
4.  i  :  \mBbbN{}2
5.  \mneg{}(y  =  x)
6.  \mneg{}(y  \mmember{}  I)
\mvdash{}  (x:=i)[y:=y]  =  (x:=i)


By

---

Latex:
((FunExt  THENA  Auto)
  THEN  RepUR  ``extend-name-morph  face-map``  0
  THEN  (BoolCase  \mkleeneopen{}(x1  =\msubz{}  x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}eq-cname(x1;y)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index