---

Step * of Lemma iota-identity2

∀[I:Cname List]. ∀[x:Cname]. ∀[i:ℕ2].  ((x:=i) o iota(x)) = 1 ∈ name-morph(I;I) supposing ¬(x ∈ I)
BY
{ (Auto THEN Symmetry THEN (InstLemma `id-morph_wf` [⌜I⌝]⋅ THENA Auto)) }

1
1. I : Cname List
2. x : Cname
3. i : ℕ2
4. ¬(x ∈ I)
5. 1 ∈ name-morph(I;I)
⊢ 1 = ((x:=i) o iota(x)) ∈ name-morph(I;I)

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x:Cname].  \mforall{}[i:\mBbbN{}2].    ((x:=i)  o  iota(x))  =  1  supposing  \mneg{}(x  \mmember{}  I)


By

---

Latex:
(Auto  THEN  Symmetry  THEN  (InstLemma  `id-morph\_wf`  [\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index