Step
*
2
3
1
of Lemma
extend-name-morph_wf
1. I : Cname List
2. J : Cname List
3. f : nameset(I) ⟶ extd-nameset(J)
4. ∀i,j:nameset(I). ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
5. z1 : Cname
6. z2 : Cname
7. ¬(z2 ∈ J)
8. nameset(J) ⊆r extd-nameset([z2 / J])
9. i : nameset([z1 / I])
10. ¬(i = z1 ∈ Cname)
11. j : nameset([z1 / I])
12. ¬(j = z1 ∈ Cname)
13. j ∈ nameset(I)
14. i ∈ nameset(I)
15. ↑isname(f i)
16. f i ∈ nameset(J)
17. ↑isname(f j)
18. f j ∈ nameset(J)
19. z2 ∈ extd-nameset([z2 / J])
20. (f i) = (f j) ∈ extd-nameset([z2 / J])
⊢ (f i) = (f j) ∈ extd-nameset(J)
BY
{ HypSubst' (-1) 0 }
1
1. I : Cname List
2. J : Cname List
3. f : nameset(I) ⟶ extd-nameset(J)
4. ∀i,j:nameset(I). ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset(J)) ⇒ (i = j ∈ nameset(I)))
5. z1 : Cname
6. z2 : Cname
7. ¬(z2 ∈ J)
8. nameset(J) ⊆r extd-nameset([z2 / J])
9. i : nameset([z1 / I])
10. ¬(i = z1 ∈ Cname)
11. j : nameset([z1 / I])
12. ¬(j = z1 ∈ Cname)
13. j ∈ nameset(I)
14. i ∈ nameset(I)
15. ↑isname(f i)
16. f i ∈ nameset(J)
17. ↑isname(f j)
18. f j ∈ nameset(J)
19. z2 ∈ extd-nameset([z2 / J])
20. (f i) = (f j) ∈ extd-nameset([z2 / J])
⊢ (f j) = (f j) ∈ extd-nameset(J)
Latex:
Latex:
1. I : Cname List
2. J : Cname List
3. f : nameset(I) {}\mrightarrow{} extd-nameset(J)
4. \mforall{}i,j:nameset(I). ((\muparrow{}isname(f i)) {}\mRightarrow{} (\muparrow{}isname(f j)) {}\mRightarrow{} ((f i) = (f j)) {}\mRightarrow{} (i = j))
5. z1 : Cname
6. z2 : Cname
7. \mneg{}(z2 \mmember{} J)
8. nameset(J) \msubseteq{}r extd-nameset([z2 / J])
9. i : nameset([z1 / I])
10. \mneg{}(i = z1)
11. j : nameset([z1 / I])
12. \mneg{}(j = z1)
13. j \mmember{} nameset(I)
14. i \mmember{} nameset(I)
15. \muparrow{}isname(f i)
16. f i \mmember{} nameset(J)
17. \muparrow{}isname(f j)
18. f j \mmember{} nameset(J)
19. z2 \mmember{} extd-nameset([z2 / J])
20. (f i) = (f j)
\mvdash{} (f i) = (f j)
By
Latex:
HypSubst' (-1) 0
Home
Index