---

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

No Annotations
∀I,K:Cname List. ∀f:name-morph(I;K). ∀z,x:Cname. ∀i:ℕ2.
  (f[z:=x] o (x:=i)) = ((z:=i) o f) ∈ name-morph([z / I];K) supposing (¬(x ∈ K)) ∧ (¬(z ∈ I))
BY
{ (Auto THEN BLemma `name-morphs-equal` THEN Auto) }

1
.....wf..... 
1. I : Cname List
2. K : Cname List
3. f : name-morph(I;K)
4. z : Cname
5. x : Cname
6. i : ℕ2
7. ¬(x ∈ K)
8. ¬(z ∈ I)
⊢ ((z:=i) o f) ∈ nameset([z / I]) ⟶ extd-nameset(K)

2
1. I : Cname List
2. K : Cname List
3. f : name-morph(I;K)
4. z : Cname
5. x : Cname
6. i : ℕ2
7. ¬(x ∈ K)
8. ¬(z ∈ I)
⊢ (f[z:=x] o (x:=i)) = ((z:=i) o f) ∈ (nameset([z / I]) ⟶ extd-nameset(K))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}z,x:Cname.  \mforall{}i:\mBbbN{}2.
    (f[z:=x]  o  (x:=i))  =  ((z:=i)  o  f)  supposing  (\mneg{}(x  \mmember{}  K))  \mwedge{}  (\mneg{}(z  \mmember{}  I))


By

---

Latex:
(Auto  THEN  BLemma  `name-morphs-equal`  THEN  Auto)

---

Home Index