---

Step * 1 of Lemma name-morph-inv-eq-domain


1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. ∀[x:nameset(I)]. (name-morph-inv(I;f) (f x)) = x ∈ nameset(I) supposing ↑isname(f x)
5. x : name-morph-domain(f;I)
⊢ (name-morph-inv(I;f) (f x)) = x ∈ nameset(I)
BY
{ (D -1 THEN (RW ListC (-1) THENA Auto) THEN Reduce (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  f  :  name-morph(I;J)
4.  \mforall{}[x:nameset(I)].  (name-morph-inv(I;f)  (f  x))  =  x  supposing  \muparrow{}isname(f  x)
5.  x  :  name-morph-domain(f;I)
\mvdash{}  (name-morph-inv(I;f)  (f  x))  =  x


By

---

Latex:
(D  -1  THEN  (RW  ListC  (-1)  THENA  Auto)  THEN  Reduce  (-1)  THEN  Auto)

---

Home Index