Step
*
1
1
2
of Lemma
extend-A-open-box_wf
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈bx.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
10. ∀i:ℕ||bx||. ∀j:ℕi. A-face-compatible(X;A;I;alpha;bx[j];bx[i])
11. f1 : A-face(X;A;I;alpha)
12. f2 : A-face(X;A;I;alpha)
13. z : Cname
14. (z ∈ I)
15. ¬(z ∈ J)
16. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
17. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
18. ¬(x = z ∈ Cname)
19. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
20. k : ℕ||[f1; [f2 / bx]]||
21. ¬(k = 0 ∈ ℤ)
⊢ ∀j:ℕk. A-face-compatible(X;A;I;alpha;[f1; [f2 / bx]][j];[f1; [f2 / bx]][k])
BY
{ CaseNat 1 `k' }
1
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈bx.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
10. ∀i:ℕ||bx||. ∀j:ℕi. A-face-compatible(X;A;I;alpha;bx[j];bx[i])
11. f1 : A-face(X;A;I;alpha)
12. f2 : A-face(X;A;I;alpha)
13. z : Cname
14. (z ∈ I)
15. ¬(z ∈ J)
16. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
17. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
18. ¬(x = z ∈ Cname)
19. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
20. k : ℕ||[f1; [f2 / bx]]||
21. ¬(k = 0 ∈ ℤ)
22. k = 1 ∈ ℤ
⊢ ∀j:ℕ1. A-face-compatible(X;A;I;alpha;[f1; [f2 / bx]][j];[f1; [f2 / bx]][1])
2
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : ℕ2
8. bx : A-face(X;A;I;alpha) List
9. (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
∧ (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
∧ (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈bx.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
10. ∀i:ℕ||bx||. ∀j:ℕi. A-face-compatible(X;A;I;alpha;bx[j];bx[i])
11. f1 : A-face(X;A;I;alpha)
12. f2 : A-face(X;A;I;alpha)
13. z : Cname
14. (z ∈ I)
15. ¬(z ∈ J)
16. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
17. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
18. ¬(x = z ∈ Cname)
19. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
20. k : ℕ||[f1; [f2 / bx]]||
21. ¬(k = 0 ∈ ℤ)
22. ¬(k = 1 ∈ ℤ)
⊢ ∀j:ℕk. A-face-compatible(X;A;I;alpha;[f1; [f2 / bx]][j];[f1; [f2 / bx]][k])
Latex:
Latex:
1. X : CubicalSet
2. A : \{X \mvdash{} \_\}
3. I : Cname List
4. alpha : X(I)
5. J : Cname List
6. x : nameset(I)
7. i : \mBbbN{}2
8. bx : A-face(X;A;I;alpha) List
9. (\mneg{}(x \mmember{} J))
\mwedge{} l\_subset(Cname;J;I)
\mwedge{} ((\mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}bx. A-face-name(f) = <y, c>))
\mwedge{} (\mexists{}f\mmember{}bx. A-face-name(f) = <x, i>)
\mwedge{} (\mforall{}f\mmember{}bx.\mneg{}(A-face-name(f) = <x, 1 - i>)))
\mwedge{} (\mforall{}f\mmember{}bx.(fst(f) \mmember{} [x / J]))
\mwedge{} (\mforall{}f1,f2\mmember{}bx. \mneg{}(A-face-name(f1) = A-face-name(f2)))
10. \mforall{}i:\mBbbN{}||bx||. \mforall{}j:\mBbbN{}i. A-face-compatible(X;A;I;alpha;bx[j];bx[i])
11. f1 : A-face(X;A;I;alpha)
12. f2 : A-face(X;A;I;alpha)
13. z : Cname
14. (z \mmember{} I)
15. \mneg{}(z \mmember{} J)
16. A-face-name(f1) = <z, 0>
17. A-face-name(f2) = <z, 1>
18. \mneg{}(x = z)
19. (\mforall{}f\mmember{}bx.A-face-compatible(X;A;I;alpha;f1;f) \mwedge{} A-face-compatible(X;A;I;alpha;f2;f))
20. k : \mBbbN{}||[f1; [f2 / bx]]||
21. \mneg{}(k = 0)
\mvdash{} \mforall{}j:\mBbbN{}k. A-face-compatible(X;A;I;alpha;[f1; [f2 / bx]][j];[f1; [f2 / bx]][k])
By
Latex:
CaseNat 1 `k'
Home
Index