---

Step * 1 of Lemma path-comp-fun


1. [T] : Type
2. [B] : SeparationSpace
3. ∀f,g:Point(Path(B)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(B)). path-comp-rel(B;f;g;h)))
4. f : Point(Path(T ⟶ B))
5. g : Point(Path(T ⟶ B))
6. f@r1 ≡ g@r0
⊢ ∃h:Point(Path(T ⟶ B)). path-comp-rel(T ⟶ B;f;g;h)
BY
{ ((Assert ∀x:T. (λt.(f t x) ∈ Point(Path(B))) BY
          (All (RWW "path-ss-point fun-ss-point")
           THEN Auto
           THEN DSetVars
           THEN (MemTypeCD THEN Auto)
           THEN Reduce 0
           THEN Auto
           THEN ∀h:hyp. (RWO "fun-ss-eq" h THEN Complete (Auto)) ))
   THEN (Assert ∀x:T. (λt.(g t x) ∈ Point(Path(B))) BY
               (All (RWW "path-ss-point fun-ss-point")
                THEN Auto
                THEN DSetVars
                THEN (MemTypeCD THEN Auto)
                THEN Reduce 0
                THEN Auto
                THEN ∀h:hyp. (RWO "fun-ss-eq" h THEN Complete (Auto)) ))
   THEN (Assert ∀x:T. ∃h:Point(Path(B)). path-comp-rel(B;λt.(f t x);λt.(g t x);h) BY
               (Intro
                THEN BHyp 3
                THEN Auto
                THEN (RWO  "fun-ss-eq" (-4) THENA Auto)
                THEN All (RepUR ``path-at``)
                THEN Auto))
   THEN (Skolemize (-1) `H' THENA Auto)) }

1
1. [T] : Type
2. [B] : SeparationSpace
3. ∀f,g:Point(Path(B)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(B)). path-comp-rel(B;f;g;h)))
4. f : Point(Path(T ⟶ B))
5. g : Point(Path(T ⟶ B))
6. f@r1 ≡ g@r0
7. ∀x:T. (λt.(f t x) ∈ Point(Path(B)))
8. ∀x:T. (λt.(g t x) ∈ Point(Path(B)))
9. ∀x:T. ∃h:Point(Path(B)). path-comp-rel(B;λt.(f t x);λt.(g t x);h)
10. H : x:T ⟶ Point(Path(B))
11. ∀x:T. path-comp-rel(B;λt.(f t x);λt.(g t x);H x)
⊢ ∃h:Point(Path(T ⟶ B)). path-comp-rel(T ⟶ B;f;g;h)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [B]  :  SeparationSpace
3.  \mforall{}f,g:Point(Path(B)).    (f@r1  \mequiv{}  g@r0  {}\mRightarrow{}  (\mexists{}h:Point(Path(B)).  path-comp-rel(B;f;g;h)))
4.  f  :  Point(Path(T  {}\mrightarrow{}  B))
5.  g  :  Point(Path(T  {}\mrightarrow{}  B))
6.  f@r1  \mequiv{}  g@r0
\mvdash{}  \mexists{}h:Point(Path(T  {}\mrightarrow{}  B)).  path-comp-rel(T  {}\mrightarrow{}  B;f;g;h)


By

---

Latex:
((Assert  \mforall{}x:T.  (\mlambda{}t.(f  t  x)  \mmember{}  Point(Path(B)))  BY
                (All  (RWW  "path-ss-point  fun-ss-point")
                  THEN  Auto
                  THEN  DSetVars
                  THEN  (MemTypeCD  THEN  Auto)
                  THEN  Reduce  0
                  THEN  Auto
                  THEN  \mforall{}h:hyp.  (RWO  "fun-ss-eq"  h  THEN  Complete  (Auto))  ))
  THEN  (Assert  \mforall{}x:T.  (\mlambda{}t.(g  t  x)  \mmember{}  Point(Path(B)))  BY
                          (All  (RWW  "path-ss-point  fun-ss-point")
                            THEN  Auto
                            THEN  DSetVars
                            THEN  (MemTypeCD  THEN  Auto)
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  \mforall{}h:hyp.  (RWO  "fun-ss-eq"  h  THEN  Complete  (Auto))  ))
  THEN  (Assert  \mforall{}x:T.  \mexists{}h:Point(Path(B)).  path-comp-rel(B;\mlambda{}t.(f  t  x);\mlambda{}t.(g  t  x);h)  BY
                          (Intro
                            THEN  BHyp  3
                            THEN  Auto
                            THEN  (RWO    "fun-ss-eq"  (-4)  THENA  Auto)
                            THEN  All  (RepUR  ``path-at``)
                            THEN  Auto))
  THEN  (Skolemize  (-1)  `H'  THENA  Auto))

---

Home Index