Step
*
2
1
1
of Lemma
face-compatible-image
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
19. ¬(x = y ∈ Cname)
20. y ∈ nameset(I-[x])
21. x ∈ nameset(I-[y])
22. f ∈ name-morph(I-[x];K-[f x])
23. f ∈ name-morph(I-[y];K-[f y])
⊢ (f y:=f5)(f(f3)) = (f x:=f2)(f(f6)) ∈ X(K-[f x; f y])
BY
{ xxx(RWO "cube-set-restriction-comp" 0 THEN Try (QuickAuto))xxx }
1
.....wf.....
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
19. ¬(x = y ∈ Cname)
20. y ∈ nameset(I-[x])
21. x ∈ nameset(I-[y])
22. f ∈ name-morph(I-[x];K-[f x])
23. f ∈ name-morph(I-[y];K-[f y])
⊢ X(K-[f x; f y]) = X(K-[f x; f y]) ∈ Type
2
.....wf.....
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
19. ¬(x = y ∈ Cname)
20. y ∈ nameset(I-[x])
21. x ∈ nameset(I-[y])
22. f ∈ name-morph(I-[x];K-[f x])
23. f ∈ name-morph(I-[y];K-[f y])
⊢ K-[f x] ∈ Cname List
3
.....wf.....
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
19. ¬(x = y ∈ Cname)
20. y ∈ nameset(I-[x])
21. x ∈ nameset(I-[y])
22. f ∈ name-morph(I-[x];K-[f x])
23. f ∈ name-morph(I-[y];K-[f y])
⊢ K-[f x; f y] ∈ Cname List
4
.....wf.....
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
19. ¬(x = y ∈ Cname)
20. y ∈ nameset(I-[x])
21. x ∈ nameset(I-[y])
22. f ∈ name-morph(I-[x];K-[f x])
23. f ∈ name-morph(I-[y];K-[f y])
⊢ (f y:=f5) ∈ name-morph(K-[f x];K-[f x; f y])
5
.....wf.....
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
19. ¬(x = y ∈ Cname)
20. y ∈ nameset(I-[x])
21. x ∈ nameset(I-[y])
22. f ∈ name-morph(I-[x];K-[f x])
23. f ∈ name-morph(I-[y];K-[f y])
⊢ K-[f y] ∈ Cname List
6
.....wf.....
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
19. ¬(x = y ∈ Cname)
20. y ∈ nameset(I-[x])
21. x ∈ nameset(I-[y])
22. f ∈ name-morph(I-[x];K-[f x])
23. f ∈ name-morph(I-[y];K-[f y])
⊢ (f x:=f2) ∈ name-morph(K-[f y];K-[f x; f y])
7
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x ∈ I)
7. f2 : ℕ2
8. f3 : X(I-[x])
9. y : Cname
10. (y ∈ I)
11. f5 : ℕ2
12. f6 : X(I-[y])
13. ↑isname(f x)
14. ↑isname(f y)
15. (¬(x = y ∈ Cname)) ⇒ ((y:=f5)(f3) = (x:=f2)(f6) ∈ X(I-[x; y]))
16. f y ∈ nameset(K)
17. f x ∈ nameset(K)
18. ¬((f x) = (f y) ∈ Cname)
19. ¬(x = y ∈ Cname)
20. y ∈ nameset(I-[x])
21. x ∈ nameset(I-[y])
22. f ∈ name-morph(I-[x];K-[f x])
23. f ∈ name-morph(I-[y];K-[f y])
⊢ (f o (f y:=f5))(f3) = (f o (f x:=f2))(f6) ∈ X(K-[f x; f y])
Latex:
Latex:
1. X : CubicalSet
2. I : Cname List
3. K : Cname List
4. f : name-morph(I;K)
5. x : Cname
6. (x \mmember{} I)
7. f2 : \mBbbN{}2
8. f3 : X(I-[x])
9. y : Cname
10. (y \mmember{} I)
11. f5 : \mBbbN{}2
12. f6 : X(I-[y])
13. \muparrow{}isname(f x)
14. \muparrow{}isname(f y)
15. (\mneg{}(x = y)) {}\mRightarrow{} ((y:=f5)(f3) = (x:=f2)(f6))
16. f y \mmember{} nameset(K)
17. f x \mmember{} nameset(K)
18. \mneg{}((f x) = (f y))
19. \mneg{}(x = y)
20. y \mmember{} nameset(I-[x])
21. x \mmember{} nameset(I-[y])
22. f \mmember{} name-morph(I-[x];K-[f x])
23. f \mmember{} name-morph(I-[y];K-[f y])
\mvdash{} (f y:=f5)(f(f3)) = (f x:=f2)(f(f6))
By
Latex:
xxx(RWO "cube-set-restriction-comp" 0 THEN Try (QuickAuto))xxx
Home
Index