---

Step * 1 1 of Lemma path-comp-property_functionality


1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. f1 : Point(X ⟶ Y)
4. g1 : Point(Y ⟶ X)
5. ∀x:Point(X). g1(f1(x)) ≡ x
6. ∀y:Point(Y). f1(g1(y)) ≡ y
7. ∀f,g:Point(Path(X)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))
8. f : Point(Path(Y))
9. g : Point(Path(Y))
10. f@r1 ≡ g@r0
⊢ ∃h:Point(Path(Y)). path-comp-rel(Y;f;g;h)
BY
{ (InstHyp [⌜ss-comp(g1;f)⌝;⌜ss-comp(g1;g)⌝] (-4)⋅ THENA Auto) }

1
.....antecedent..... 
1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. f1 : Point(X ⟶ Y)
4. g1 : Point(Y ⟶ X)
5. ∀x:Point(X). g1(f1(x)) ≡ x
6. ∀y:Point(Y). f1(g1(y)) ≡ y
7. ∀f,g:Point(Path(X)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))
8. f : Point(Path(Y))
9. g : Point(Path(Y))
10. f@r1 ≡ g@r0
⊢ ss-comp(g1;f)@r1 ≡ ss-comp(g1;g)@r0

2
1. [X] : SeparationSpace
2. [Y] : SeparationSpace
3. f1 : Point(X ⟶ Y)
4. g1 : Point(Y ⟶ X)
5. ∀x:Point(X). g1(f1(x)) ≡ x
6. ∀y:Point(Y). f1(g1(y)) ≡ y
7. ∀f,g:Point(Path(X)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))
8. f : Point(Path(Y))
9. g : Point(Path(Y))
10. f@r1 ≡ g@r0
11. ∃h:Point(Path(X)). path-comp-rel(X;ss-comp(g1;f);ss-comp(g1;g);h)
⊢ ∃h:Point(Path(Y)). path-comp-rel(Y;f;g;h)

---

Latex:

---

Latex:

1.  [X]  :  SeparationSpace
2.  [Y]  :  SeparationSpace
3.  f1  :  Point(X  {}\mrightarrow{}  Y)
4.  g1  :  Point(Y  {}\mrightarrow{}  X)
5.  \mforall{}x:Point(X).  g1(f1(x))  \mequiv{}  x
6.  \mforall{}y:Point(Y).  f1(g1(y))  \mequiv{}  y
7.  \mforall{}f,g:Point(Path(X)).    (f@r1  \mequiv{}  g@r0  {}\mRightarrow{}  (\mexists{}h:Point(Path(X)).  path-comp-rel(X;f;g;h)))
8.  f  :  Point(Path(Y))
9.  g  :  Point(Path(Y))
10.  f@r1  \mequiv{}  g@r0
\mvdash{}  \mexists{}h:Point(Path(Y)).  path-comp-rel(Y;f;g;h)


By

---

Latex:
(InstHyp  [\mkleeneopen{}ss-comp(g1;f)\mkleeneclose{};\mkleeneopen{}ss-comp(g1;g)\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)

---

Home Index