---

Step * of Lemma name-morph-domain-inject

∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  Inj(name-morph-domain(f;I);nameset(J);f)
BY
{ (Intros THEN RepeatFor 2 (((D 0 THENA Auto) THEN D -1))) }

1
1. [I] : Cname List
2. [J] : Cname List
3. [f] : name-morph(I;J)
4. a1 : Cname@i
5. [%1] : (a1 ∈ filter(λx.isname(f x);I))@i
6. a2 : Cname@i
7. [%2] : (a2 ∈ filter(λx.isname(f x);I))@i
⊢ ((f a1) = (f a2) ∈ nameset(J)) ⇒ (a1 = a2 ∈ name-morph-domain(f;I))

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].    Inj(name-morph-domain(f;I);nameset(J);f)


By

---

Latex:
(Intros  THEN  RepeatFor  2  (((D  0  THENA  Auto)  THEN  D  -1)))

---

Home Index