---

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


1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : Cname
5. (x ∈ I)
6. ↑isname(f x)
7. f x ∈ nameset(J)
8. λi.(isname(f i) ∧b (f i =z f x)) ∈ nameset(I) ⟶ 𝔹
9. I ∈ nameset(I) List
10. (x ∈ filter(λi.(isname(f i) ∧b (f i =z f x));I))
⊢ (name-morph-inv(I;f) (f x) ∈ filter(λi.(isname(f i) ∧b (f i =z f x));I))
⇒ ((name-morph-inv(I;f) (f x)) = x ∈ nameset(I))
BY
{ TACTIC:(Assert f x ∈ name-morph-range(f;I) BY
                MemTypeCD) }

1
.....aux..... 
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : Cname
5. (x ∈ I)
6. ↑isname(f x)
7. f x ∈ nameset(J)
8. λi.(isname(f i) ∧b (f i =z f x)) ∈ nameset(I) ⟶ 𝔹
9. I ∈ nameset(I) List
10. (x ∈ filter(λi.(isname(f i) ∧b (f i =z f x));I))
⊢ f x ∈ Cname

2
.....aux..... 
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : Cname
5. (x ∈ I)
6. ↑isname(f x)
7. f x ∈ nameset(J)
8. λi.(isname(f i) ∧b (f i =z f x)) ∈ nameset(I) ⟶ 𝔹
9. I ∈ nameset(I) List
10. (x ∈ filter(λi.(isname(f i) ∧b (f i =z f x));I))
⊢ ∃i:nameset(I). ((↑isname(f i)) ∧ ((f i) = (f x) ∈ Cname))

3
.....aux..... 
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : Cname
5. (x ∈ I)
6. ↑isname(f x)
7. f x ∈ nameset(J)
8. λi.(isname(f i) ∧b (f i =z f x)) ∈ nameset(I) ⟶ 𝔹
9. I ∈ nameset(I) List
10. (x ∈ filter(λi.(isname(f i) ∧b (f i =z f x));I))
11. x1 : Cname
⊢ istype(∃i:nameset(I). ((↑isname(f i)) ∧ ((f i) = x1 ∈ Cname)))

4
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : Cname
5. (x ∈ I)
6. ↑isname(f x)
7. f x ∈ nameset(J)
8. λi.(isname(f i) ∧b (f i =z f x)) ∈ nameset(I) ⟶ 𝔹
9. I ∈ nameset(I) List
10. (x ∈ filter(λi.(isname(f i) ∧b (f i =z f x));I))
11. f x ∈ name-morph-range(f;I)
⊢ (name-morph-inv(I;f) (f x) ∈ filter(λi.(isname(f i) ∧b (f i =z f x));I))
⇒ ((name-morph-inv(I;f) (f x)) = x ∈ nameset(I))

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  Cname  List
3.  f  :  name-morph(I;J)
4.  x  :  Cname
5.  (x  \mmember{}  I)
6.  \muparrow{}isname(f  x)
7.  f  x  \mmember{}  nameset(J)
8.  \mlambda{}i.(isname(f  i)  \mwedge{}\msubb{}  (f  i  =\msubz{}  f  x))  \mmember{}  nameset(I)  {}\mrightarrow{}  \mBbbB{}
9.  I  \mmember{}  nameset(I)  List
10.  (x  \mmember{}  filter(\mlambda{}i.(isname(f  i)  \mwedge{}\msubb{}  (f  i  =\msubz{}  f  x));I))
\mvdash{}  (name-morph-inv(I;f)  (f  x)  \mmember{}  filter(\mlambda{}i.(isname(f  i)  \mwedge{}\msubb{}  (f  i  =\msubz{}  f  x));I))
{}\mRightarrow{}  ((name-morph-inv(I;f)  (f  x))  =  x)


By

---

Latex:
TACTIC:(Assert  f  x  \mmember{}  name-morph-range(f;I)  BY
                            MemTypeCD)

---

Home Index