---

Step * of Lemma face-map-comp-id

No Annotations
∀A,B:Cname List. ∀g:name-morph(A;B). ∀x:nameset(A). ∀i:ℕ2.
  ((x:=i) o g) = g ∈ name-morph(A;B) supposing (¬↑isname(g x)) ∧ ((g x) = i ∈ ℕ2)
BY
{ (UnivCD THENA (Try ((D 0 THEN Try (FLemma `not-assert-isname` [-1]) THEN Auto)) THEN Auto)) }

1
1. A : Cname List
2. B : Cname List
3. g : name-morph(A;B)
4. x : nameset(A)
5. i : ℕ2
6. (¬↑isname(g x)) ∧ ((g x) = i ∈ ℕ2)
⊢ ((x:=i) o g) = g ∈ name-morph(A;B)

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  (Try  ((D  0  THEN  Try  (FLemma  `not-assert-isname`  [-1])  THEN  Auto))  THEN  Auto))

---

Home Index