Step
*
2
3
1
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. A-adjacent-compatible(X;A;I;alpha;bx)
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
13. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
14. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
15. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. f1 : A-face(X;A;I;alpha)
18. f2 : A-face(X;A;I;alpha)
19. z : Cname
20. (z ∈ I)
21. ¬(z ∈ J)
22. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
23. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
24. ¬(x = z ∈ Cname)
25. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
26. i1 : ℕ||[f1; [f2 / bx]]||
⊢ (fst([f1; [f2 / bx]][i1]) ∈ [x; [z / J]])
BY
{ (RenameVar `j' (-1) THEN CaseNat 0 `j' THEN Reduce 0) }
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. A-adjacent-compatible(X;A;I;alpha;bx)
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
13. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
14. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
15. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. f1 : A-face(X;A;I;alpha)
18. f2 : A-face(X;A;I;alpha)
19. z : Cname
20. (z ∈ I)
21. ¬(z ∈ J)
22. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
23. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
24. ¬(x = z ∈ Cname)
25. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
26. j : ℕ||[f1; [f2 / bx]]||
27. j = 0 ∈ ℤ
⊢ (fst(f1) ∈ [x; [z / J]])
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. A-adjacent-compatible(X;A;I;alpha;bx)
10. ¬(x ∈ J)
11. l_subset(Cname;J;I)
12. ∀y:nameset(J). ∀c:ℕ2. (∃f∈bx. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
13. (∃f∈bx. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
14. (∀f∈bx.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
15. (∀f1,f2∈bx. ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))
16. (∀f∈bx.(fst(f) ∈ [x / J]))
17. f1 : A-face(X;A;I;alpha)
18. f2 : A-face(X;A;I;alpha)
19. z : Cname
20. (z ∈ I)
21. ¬(z ∈ J)
22. A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2)
23. A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)
24. ¬(x = z ∈ Cname)
25. (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))
26. j : ℕ||[f1; [f2 / bx]]||
27. ¬(j = 0 ∈ ℤ)
⊢ (fst([f1; [f2 / bx]][j]) ∈ [x; [z / J]])
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. A-adjacent-compatible(X;A;I;alpha;bx)
10. \mneg{}(x \mmember{} J)
11. l\_subset(Cname;J;I)
12. \mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}bx. A-face-name(f) = <y, c>)
13. (\mexists{}f\mmember{}bx. A-face-name(f) = <x, i>)
14. (\mforall{}f\mmember{}bx.\mneg{}(A-face-name(f) = <x, 1 - i>))
15. (\mforall{}f1,f2\mmember{}bx. \mneg{}(A-face-name(f1) = A-face-name(f2)))
16. (\mforall{}f\mmember{}bx.(fst(f) \mmember{} [x / J]))
17. f1 : A-face(X;A;I;alpha)
18. f2 : A-face(X;A;I;alpha)
19. z : Cname
20. (z \mmember{} I)
21. \mneg{}(z \mmember{} J)
22. A-face-name(f1) = <z, 0>
23. A-face-name(f2) = <z, 1>
24. \mneg{}(x = z)
25. (\mforall{}f\mmember{}bx.A-face-compatible(X;A;I;alpha;f1;f) \mwedge{} A-face-compatible(X;A;I;alpha;f2;f))
26. i1 : \mBbbN{}||[f1; [f2 / bx]]||
\mvdash{} (fst([f1; [f2 / bx]][i1]) \mmember{} [x; [z / J]])
By
Latex:
(RenameVar `j' (-1) THEN CaseNat 0 `j' THEN Reduce 0)
Home
Index