---

Step * of Lemma name-morph-domain_subtype

∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  name-morph-domain(f;I) ≡ {x:nameset(I)| ↑isname(f x)} 
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto))) }

1
.....subterm..... T:t
1:n
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : name-morph-domain(f;I)@i
⊢ x ∈ {x:nameset(I)| ↑isname(f x)} 

2
.....subterm..... T:t
1:n
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : {x:nameset(I)| ↑isname(f x)} @i
⊢ x ∈ name-morph-domain(f;I)

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].    name-morph-domain(f;I)  \mequiv{}  \{x:nameset(I)|  \muparrow{}isname(f  x)\} 


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index