---

Step * 1 5 of Lemma face-map-comp2


1. A : Cname List
2. B : Cname List
3. g : name-morph(A;B)
4. x : nameset(A)
5. y : nameset(A)
6. i : ℕ2
7. j : ℕ2
8. ↑isname(g x)
9. ↑isname(g y)
10. ¬(x = y ∈ Cname)
11. g y ∈ nameset(B)
12. g x ∈ nameset(B)
⊢ ∀x1:nameset(A). (((g o ((g x:=i) o (g y:=j))) x1) = ((((x:=i) o (y:=j)) o g) x1) ∈ extd-nameset(B-[g x; g y]))
BY
{ (D 0 THENA Auto) }

1
1. A : Cname List
2. B : Cname List
3. g : name-morph(A;B)
4. x : nameset(A)
5. y : nameset(A)
6. i : ℕ2
7. j : ℕ2
8. ↑isname(g x)
9. ↑isname(g y)
10. ¬(x = y ∈ Cname)
11. g y ∈ nameset(B)
12. g x ∈ nameset(B)
13. x1 : nameset(A)
⊢ ((g o ((g x:=i) o (g y:=j))) x1) = ((((x:=i) o (y:=j)) o g) x1) ∈ extd-nameset(B-[g x; g y])

---

Latex:

---

Latex:

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


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index