---

Step * of Lemma name-comp_wf

∀[I,J,K:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)].  ((f o g) ∈ name-morph(I;K))
BY
{ (Auto THEN D -2 THEN D -1 THEN MemTypeCD) }

1
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : nameset(I) ⟶ extd-nameset(J)
5. ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
6. g : nameset(J) ⟶ extd-nameset(K)
7. ∀i,j:nameset(J).  ((↑isname(g i)) ⇒ (↑isname(g j)) ⇒ ((g i) = (g j) ∈ extd-nameset(K)) ⇒ (i = j ∈ nameset(J)))
⊢ (f o g) ∈ nameset(I) ⟶ extd-nameset(K)

2
.....set predicate..... 
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : nameset(I) ⟶ extd-nameset(J)
5. ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
6. g : nameset(J) ⟶ extd-nameset(K)
7. ∀i,j:nameset(J).  ((↑isname(g i)) ⇒ (↑isname(g j)) ⇒ ((g i) = (g j) ∈ extd-nameset(K)) ⇒ (i = j ∈ nameset(J)))
⊢ ∀i,j:nameset(I).
    ((↑isname((f o g) i))
    ⇒ (↑isname((f o g) j))
    ⇒ (((f o g) i) = ((f o g) j) ∈ extd-nameset(K))
    ⇒ (i = j ∈ nameset(I)))

3
.....wf..... 
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : nameset(I) ⟶ extd-nameset(J)
5. ∀i,j:nameset(I).  ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
6. g : nameset(J) ⟶ extd-nameset(K)
7. ∀i,j:nameset(J).  ((↑isname(g i)) ⇒ (↑isname(g j)) ⇒ ((g i) = (g j) ∈ extd-nameset(K)) ⇒ (i = j ∈ nameset(J)))
8. f1 : nameset(I) ⟶ extd-nameset(K)
⊢ ∀i,j:nameset(I).  ((↑isname(f1 i)) ⇒ (↑isname(f1 j)) ⇒ ((f1 i) = (f1 j) ∈ extd-nameset(K)) ⇒ (i = j ∈ nameset(I)))
  ∈ Type

---

Latex:

---

Latex:
\mforall{}[I,J,K:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[g:name-morph(J;K)].    ((f  o  g)  \mmember{}  name-morph(I;K))


By

---

Latex:
(Auto  THEN  D  -2  THEN  D  -1  THEN  MemTypeCD)

---

Home Index