---

Step * 1 of Lemma iota-identity2


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)
BY
{ ((MemTypeHD (-1) THENA Auto) THEN MemTypeCD THEN Auto) }

1
1. I : Cname List
2. x : Cname
3. i : ℕ2
4. ¬(x ∈ I)
5. 1 = 1 ∈ (nameset(I) ⟶ extd-nameset(I))
6. ∀i,j:nameset(I).  ((↑isname(1 i)) ⇒ (↑isname(1 j)) ⇒ ((1 i) = (1 j) ∈ extd-nameset(I)) ⇒ (i = j ∈ nameset(I)))
⊢ 1 = ((x:=i) o iota(x)) ∈ (nameset(I) ⟶ extd-nameset(I))

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  x  :  Cname
3.  i  :  \mBbbN{}2
4.  \mneg{}(x  \mmember{}  I)
5.  1  \mmember{}  name-morph(I;I)
\mvdash{}  1  =  ((x:=i)  o  iota(x))


By

---

Latex:
((MemTypeHD  (-1)  THENA  Auto)  THEN  MemTypeCD  THEN  Auto)

---

Home Index