---

Step * of Lemma name-morph-one-one

∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[x,y:nameset(I)].
  (x = y ∈ Cname) supposing (((f x) = (f y) ∈ Cname) and (↑isname(f y)) and (↑isname(f x)))
BY
{ (RepeatFor 7 (Intro)
   THEN D 0
   THEN (FLemma `assert-isname` [6] THENA Auto)
   THEN (FLemma `assert-isname` [7] THENA Auto)
   THEN Auto) }

1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : nameset(I)
5. y : nameset(I)
6. ↑isname(f x)
7. ↑isname(f y)
8. (f x) = (f y) ∈ Cname
9. f x ∈ nameset(J)
10. f y ∈ nameset(J)
⊢ x = y ∈ Cname

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[x,y:nameset(I)].
    (x  =  y)  supposing  (((f  x)  =  (f  y))  and  (\muparrow{}isname(f  y))  and  (\muparrow{}isname(f  x)))


By

---

Latex:
(RepeatFor  7  (Intro)
  THEN  D  0
  THEN  (FLemma  `assert-isname`  [6]  THENA  Auto)
  THEN  (FLemma  `assert-isname`  [7]  THENA  Auto)
  THEN  Auto)

---

Home Index