---

Step * 1 1 1 1 of Lemma length-open_box-ge-3


1. X : CubicalSet
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : open_box(X;I;J;x;i)
7. 3 < 1 + (||remove-repeats(CnameDeq;J)|| * 2)
8. CnameDeq ∈ EqDecider(nameset(I))
9. 1 < ||remove-repeats(CnameDeq;J)||
10. ¬(∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))
⊢ ∃x:nameset(I). ((x ∈ J) ∧ (∀y:nameset(I). y = x ∈ nameset(I) supposing (y ∈ J)))
BY
{ DVar `J' }

1
1. X : CubicalSet
2. I : Cname List
3. x : nameset(I)
4. i : ℕ2
5. box : open_box(X;I;[];x;i)
6. 3 < 1 + (||remove-repeats(CnameDeq;[])|| * 2)
7. CnameDeq ∈ EqDecider(nameset(I))
8. 1 < ||remove-repeats(CnameDeq;[])||
9. ¬(∃j1∈[]. (∃j2∈[]. ¬(j1 = j2 ∈ Cname)))
⊢ ∃x:nameset(I). ((x ∈ []) ∧ (∀y:nameset(I). y = x ∈ nameset(I) supposing (y ∈ [])))

2
1. X : CubicalSet
2. I : Cname List
3. u : nameset(I)
4. v : nameset(I) List
5. x : nameset(I)
6. i : ℕ2
7. box : open_box(X;I;[u / v];x;i)
8. 3 < 1 + (||remove-repeats(CnameDeq;[u / v])|| * 2)
9. CnameDeq ∈ EqDecider(nameset(I))
10. 1 < ||remove-repeats(CnameDeq;[u / v])||
11. ¬(∃j1∈[u / v]. (∃j2∈[u / v]. ¬(j1 = j2 ∈ Cname)))
⊢ ∃x:nameset(I). ((x ∈ [u / v]) ∧ (∀y:nameset(I). y = x ∈ nameset(I) supposing (y ∈ [u / v])))

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  I  :  Cname  List
3.  J  :  nameset(I)  List
4.  x  :  nameset(I)
5.  i  :  \mBbbN{}2
6.  box  :  open\_box(X;I;J;x;i)
7.  3  <  1  +  (||remove-repeats(CnameDeq;J)||  *  2)
8.  CnameDeq  \mmember{}  EqDecider(nameset(I))
9.  1  <  ||remove-repeats(CnameDeq;J)||
10.  \mneg{}(\mexists{}j1\mmember{}J.  (\mexists{}j2\mmember{}J.  \mneg{}(j1  =  j2)))
\mvdash{}  \mexists{}x:nameset(I).  ((x  \mmember{}  J)  \mwedge{}  (\mforall{}y:nameset(I).  y  =  x  supposing  (y  \mmember{}  J)))


By

---

Latex:
DVar  `J'

---

Home Index