---

Step * 2 1 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)
8. i : ℕ||J||
⊢ ((c1 J[i]) = 0 ∈ ℕ2) ∧ ((c2 J[i]) = 1 ∈ ℕ2)
BY
{ (InstLemma `poset-cat-arrow-not-equal` [⌜I⌝;⌜J[i]⌝;⌜c1⌝;⌜c2⌝;⌜f⌝]⋅ THEN Auto) }

1
.....antecedent..... 
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] ≠ c2 J[i]

---

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)  =  []
8.  i  :  \mBbbN{}||J||
\mvdash{}  ((c1  J[i])  =  0)  \mwedge{}  ((c2  J[i])  =  1)


By

---

Latex:
(InstLemma  `poset-cat-arrow-not-equal`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J[i]\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index