---

Step * of Lemma open_box_image_wf

∀[X:CubicalSet]. ∀[I,J,K:Cname List]. ∀[f:name-morph(I;K)]. ∀[x:nameset(I)]. ∀[i:ℕ2].
  ∀[bx:open_box(X;I;J;x;i)]. (open_box_image(X;I;K;f;bx) ∈ open_box(X;K;map(f;J);f x;i)) 
  supposing nameset([x / J]) ⊆r name-morph-domain(f;I)
BY
{ (Auto
   THEN (Assert ⌜∀x:nameset([x / J]). (f x ∈ nameset(K))⌝⋅
         THENA ((D 0 THENA Auto)
                THEN (GenConcl ⌜x1 = z ∈ name-morph-domain(f;I)⌝⋅ THENA Auto)
                THEN DVar `z'
                THEN (RW ListC (-2) THENA Auto)
                THEN Reduce (-2)
                THEN D -2
                THEN FLemma `assert-isname` [-2]
                THEN Auto)
         )
   THEN PromoteHyp (-1) 7
   THEN D -1
   THEN ((Assert ∀x:nameset(J). (f x ∈ nameset(K)) BY
                ParallelOp 7)
         THEN (Assert map(f;J) ∈ nameset(K) List BY
                     ((Assert f ∈ nameset(J) ⟶ nameset(K) BY
                             (ExtWith [`x'] [⌜Void ⟶ Void⌝]⋅ THEN Auto))
                      THEN (GenConcl ⌜J = L ∈ (nameset(J) List)⌝⋅ THENA (Unfold `nameset` 0 THEN Auto))
                      THEN Auto))
         THEN (Assert f x ∈ nameset(K) BY
                     (BHyp 7  THEN Auto))
         THEN (Assert nameset(map(f;J)) ⊆r nameset(K) BY
                     ((GenConclTerm ⌜map(f;J)⌝⋅ THENA Auto)
                      THEN All Thin
                      THEN D 0
                      THEN Auto
                      THEN RepeatFor 3 (D -1)
                      THEN HypSubst' (-1) 0
                      THEN Auto))
         THEN PromoteHyp (-1) 6)) }

1
1. X : CubicalSet
2. I : Cname List
3. J : Cname List
4. K : Cname List
5. f : name-morph(I;K)
6. nameset(map(f;J)) ⊆r nameset(K)
7. x : nameset(I)
8. ∀x:nameset([x / J]). (f x ∈ nameset(K))
9. i : ℕ2
10. nameset([x / J]) ⊆r name-morph-domain(f;I)
11. bx : I-face(X;I) List
12. adjacent-compatible(X;I;bx)
∧ (¬(x ∈ J))
∧ l_subset(Cname;J;I)
∧ ((∀y:nameset(J). ∀c:ℕ2.  (∃f∈bx. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))
  ∧ (∃f∈bx. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
  ∧ (∀f∈bx.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))
∧ (∀f∈bx.(fst(f) ∈ [x / J]))
∧ (∀f1,f2∈bx.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
13. ∀x:nameset(J). (f x ∈ nameset(K))
14. map(f;J) ∈ nameset(K) List
15. f x ∈ nameset(K)
⊢ open_box_image(X;I;K;f;bx) ∈ open_box(X;K;map(f;J);f x;i)

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,J,K:Cname  List].  \mforall{}[f:name-morph(I;K)].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
    \mforall{}[bx:open\_box(X;I;J;x;i)].  (open\_box\_image(X;I;K;f;bx)  \mmember{}  open\_box(X;K;map(f;J);f  x;i)) 
    supposing  nameset([x  /  J])  \msubseteq{}r  name-morph-domain(f;I)


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mforall{}x:nameset([x  /  J]).  (f  x  \mmember{}  nameset(K))\mkleeneclose{}\mcdot{}
              THENA  ((D  0  THENA  Auto)
                            THEN  (GenConcl  \mkleeneopen{}x1  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  DVar  `z'
                            THEN  (RW  ListC  (-2)  THENA  Auto)
                            THEN  Reduce  (-2)
                            THEN  D  -2
                            THEN  FLemma  `assert-isname`  [-2]
                            THEN  Auto)
              )
  THEN  PromoteHyp  (-1)  7
  THEN  D  -1
  THEN  ((Assert  \mforall{}x:nameset(J).  (f  x  \mmember{}  nameset(K))  BY
                            ParallelOp  7)
              THEN  (Assert  map(f;J)  \mmember{}  nameset(K)  List  BY
                                      ((Assert  f  \mmember{}  nameset(J)  {}\mrightarrow{}  nameset(K)  BY
                                                      (ExtWith  [`x']  [\mkleeneopen{}Void  {}\mrightarrow{}  Void\mkleeneclose{}]\mcdot{}  THEN  Auto))
                                        THEN  (GenConcl  \mkleeneopen{}J  =  L\mkleeneclose{}\mcdot{}  THENA  (Unfold  `nameset`  0  THEN  Auto))
                                        THEN  Auto))
              THEN  (Assert  f  x  \mmember{}  nameset(K)  BY
                                      (BHyp  7    THEN  Auto))
              THEN  (Assert  nameset(map(f;J))  \msubseteq{}r  nameset(K)  BY
                                      ((GenConclTerm  \mkleeneopen{}map(f;J)\mkleeneclose{}\mcdot{}  THENA  Auto)
                                        THEN  All  Thin
                                        THEN  D  0
                                        THEN  Auto
                                        THEN  RepeatFor  3  (D  -1)
                                        THEN  HypSubst'  (-1)  0
                                        THEN  Auto))
              THEN  PromoteHyp  (-1)  6))

---

Home Index