---

Step * of Lemma A-open-box-image_wf

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I,J,K:Cname List]. ∀[alpha:X(I)]. ∀[f:name-morph(I;K)]. ∀[x:nameset(I)]. ∀[i:ℕ2].
  ∀[bx:A-open-box(X;A;I;alpha;J;x;i)]
    (A-open-box-image(X;A;I;K;f;alpha;bx) ∈ A-open-box(X;A;K;f(alpha);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) 9
   THEN D -1
   THEN ((Assert ∀x:nameset(J). (f x ∈ nameset(K)) BY
                ParallelOp 9)
         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 9  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) 8)) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. I : Cname List
4. J : Cname List
5. K : Cname List
6. alpha : X(I)
7. f : name-morph(I;K)
8. nameset(map(f;J)) ⊆r nameset(K)
9. x : nameset(I)
10. ∀x:nameset([x / J]). (f x ∈ nameset(K))
11. i : ℕ2
12. nameset([x / J]) ⊆r name-morph-domain(f;I)
13. bx : A-face(X;A;I;alpha) List
14. A-adjacent-compatible(X;A;I;alpha;bx)
∧ (¬(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)))
15. ∀x:nameset(J). (f x ∈ nameset(K))
16. map(f;J) ∈ nameset(K) List
17. f x ∈ nameset(K)
⊢ A-open-box-image(X;A;I;K;f;alpha;bx) ∈ A-open-box(X;A;K;f(alpha);map(f;J);f x;i)

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[I,J,K:Cname  List].  \mforall{}[alpha:X(I)].  \mforall{}[f:name-morph(I;K)].
\mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
    \mforall{}[bx:A-open-box(X;A;I;alpha;J;x;i)]
        (A-open-box-image(X;A;I;K;f;alpha;bx)  \mmember{}  A-open-box(X;A;K;f(alpha);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)  9
  THEN  D  -1
  THEN  ((Assert  \mforall{}x:nameset(J).  (f  x  \mmember{}  nameset(K))  BY
                            ParallelOp  9)
              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  9    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)  8))

---

Home Index