---

Step * 2 1 of Lemma poset-cat-arrow-filter-nil


1. I : Cname List
2. J : nameset(I) List
3. nameset(J) ⊆r nameset(I)
4. c1 : cat-ob(poset-cat(I))
5. c2 : cat-ob(poset-cat(I))
6. f : cat-arrow(poset-cat(I)) c1 c2
7. filter(λz.(c1 z =z c2 z);J) = [] ∈ ({x:nameset(J)| ↑(c1 x =z c2 x)}  List)
⊢ (∀j∈J.((c1 j) = 0 ∈ ℕ2) ∧ ((c2 j) = 1 ∈ ℕ2))
BY
{ (D 0 THENA Auto) }

1
1. I : Cname List
2. J : nameset(I) List
3. nameset(J) ⊆r nameset(I)
4. c1 : cat-ob(poset-cat(I))
5. c2 : cat-ob(poset-cat(I))
6. f : cat-arrow(poset-cat(I)) c1 c2
7. filter(λz.(c1 z =z c2 z);J) = [] ∈ ({x:nameset(J)| ↑(c1 x =z c2 x)}  List)
8. i : ℕ||J||
⊢ ((c1 J[i]) = 0 ∈ ℕ2) ∧ ((c2 J[i]) = 1 ∈ ℕ2)

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  J  :  nameset(I)  List
3.  nameset(J)  \msubseteq{}r  nameset(I)
4.  c1  :  cat-ob(poset-cat(I))
5.  c2  :  cat-ob(poset-cat(I))
6.  f  :  cat-arrow(poset-cat(I))  c1  c2
7.  filter(\mlambda{}z.(c1  z  =\msubz{}  c2  z);J)  =  []
\mvdash{}  (\mforall{}j\mmember{}J.((c1  j)  =  0)  \mwedge{}  ((c2  j)  =  1))


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index