---

Step * of Lemma face-map-comp2

No Annotations
∀A,B:Cname List. ∀g:name-morph(A;B). ∀x,y:nameset(A). ∀i,j:ℕ2.
  (g o ((g x:=i) o (g y:=j))) = (((x:=i) o (y:=j)) o g) ∈ name-morph(A;B-[g x; g y]) 
  supposing ((↑isname(g x)) ∧ (↑isname(g y))) ∧ (¬(x = y ∈ Cname))
BY
{ (Auto THEN ∀h:hyp. (FLemma `assert-isname` [h] 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)
⊢ (g o ((g x:=i) o (g y:=j))) = (((x:=i) o (y:=j)) o g) ∈ name-morph(A;B-[g x; g y])

---

Latex:

---

Latex:
No  Annotations
\mforall{}A,B:Cname  List.  \mforall{}g:name-morph(A;B).  \mforall{}x,y:nameset(A).  \mforall{}i,j:\mBbbN{}2.
    (g  o  ((g  x:=i)  o  (g  y:=j)))  =  (((x:=i)  o  (y:=j))  o  g) 
    supposing  ((\muparrow{}isname(g  x))  \mwedge{}  (\muparrow{}isname(g  y)))  \mwedge{}  (\mneg{}(x  =  y))


By

---

Latex:
(Auto  THEN  \mforall{}h:hyp.  (FLemma  `assert-isname`  [h]  THENA  Auto)  )

---

Home Index