---

Step * 1 of Lemma homeo-image-inverse

.....subterm..... T:t
1:n
1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. h : homeomorphic(X;dX;Y;dY)
6. A : Type
7. A ⊆r X
8. respects-equality(X;A)
9. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
10. x : homeo-image(homeo-image(A;Y;dY;h);X;dX;homeo-inv(h))
⊢ x ∈ A
BY
{ (RepeatFor 2 (D -1)
   THEN RepeatFor 2 (D -2)
   THEN DVar `h'
   THEN RepUR ``homeo-inv`` -1
   THEN Reduce -2
   THEN RepeatFor 2 (D 6)
   THEN DVar `f'
   THEN All (Unfold `is-mfun`)
   THEN (FHyp 8 [-2] THENA Auto)
   THEN RepUR ``so_apply`` -1
   THEN Auto
   THEN (InstHyp [⌜a@0⌝] 9⋅ THENA Auto)
   THEN (Assert a@0 ∈ X BY
               Auto)
   THEN (Assert x ≡ a@0 BY
               (RelRST THEN Auto))) }

1
1. X : Type
2. Y : Type
3. dX : metric(X)
4. dY : metric(Y)
5. f : X ⟶ Y
6. ∀x1,x2:X.  (x1 ≡ x2 ⇒ f[x1] ≡ f[x2])
7. h1 : Y ⟶ X
8. ∀x1,x2:Y.  (x1 ≡ x2 ⇒ h1[x1] ≡ h1[x2])
9. ∀x:X. h1 (f x) ≡ x
10. ∀y:Y. f (h1 y) ≡ y
11. A : Type
12. A ⊆r X
13. respects-equality(X;A)
14. ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A))
15. x : X
16. a : Y
17. a@0 : A
18. a ≡ f a@0
19. x ≡ h1 a
20. h1 a ≡ h1 (f a@0)
21. h1 (f a@0) ≡ a@0
22. a@0 ∈ X
23. x ≡ a@0
⊢ x ∈ A

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  X  :  Type
2.  Y  :  Type
3.  dX  :  metric(X)
4.  dY  :  metric(Y)
5.  h  :  homeomorphic(X;dX;Y;dY)
6.  A  :  Type
7.  A  \msubseteq{}r  X
8.  respects-equality(X;A)
9.  \mforall{}a:A.  \mforall{}x:X.    (x  \mequiv{}  a  {}\mRightarrow{}  (x  \mmember{}  A))
10.  x  :  homeo-image(homeo-image(A;Y;dY;h);X;dX;homeo-inv(h))
\mvdash{}  x  \mmember{}  A


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  RepeatFor  2  (D  -2)
  THEN  DVar  `h'
  THEN  RepUR  ``homeo-inv``  -1
  THEN  Reduce  -2
  THEN  RepeatFor  2  (D  6)
  THEN  DVar  `f'
  THEN  All  (Unfold  `is-mfun`)
  THEN  (FHyp  8  [-2]  THENA  Auto)
  THEN  RepUR  ``so\_apply``  -1
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}a@0\mkleeneclose{}]  9\mcdot{}  THENA  Auto)
  THEN  (Assert  a@0  \mmember{}  X  BY
                          Auto)
  THEN  (Assert  x  \mequiv{}  a@0  BY
                          (RelRST  THEN  Auto)))

---

Home Index