---

Step * 1 of Lemma name-morph-domain-inject


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))
BY
{ (D 0
   THEN ∀h:hyp. ((RW ListC h THENM (Reduce h THEN D h THEN FLemma `assert-isname` [h+1])) THENA Complete (Auto)) 
   THEN Auto) }

1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. a1 : Cname@i
5. (a1 ∈ I)
6. ↑isname(f a1)
7. a2 : Cname@i
8. (a2 ∈ I)
9. ↑isname(f a2)
10. (f a1) = (f a2) ∈ nameset(J)@i
11. f a2 ∈ nameset(J)
12. f a1 ∈ nameset(J)
⊢ a1 = a2 ∈ name-morph-domain(f;I)

---

Latex:

---

Latex:

1.  [I]  :  Cname  List
2.  [J]  :  Cname  List
3.  [f]  :  name-morph(I;J)
4.  a1  :  Cname@i
5.  [\%1]  :  (a1  \mmember{}  filter(\mlambda{}x.isname(f  x);I))@i
6.  a2  :  Cname@i
7.  [\%2]  :  (a2  \mmember{}  filter(\mlambda{}x.isname(f  x);I))@i
\mvdash{}  ((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2)


By

---

Latex:
(D  0
  THEN  \mforall{}h:hyp.  ((RW  ListC  h  THENM  (Reduce  h  THEN  D  h  THEN  FLemma  `assert-isname`  [h+1]))
                              THENA  Complete  (Auto)
                              ) 
  THEN  Auto)

---

Home Index