---

Step * 1 of Lemma mfun-class-strong-subtype


1. X : Type
2. Y : Type
3. d : metric(X)
4. d' : metric(Y)
5. A : Type
6. strong-subtype(A;Y)
7. ∀a:A. ∀x:Y.  (x ≡ a ⇒ (x ∈ A))
8. mfun-class(X;d;A;d') ⊆r mfun-class(X;d;Y;d')
9. x : mfun-class(X;d;Y;d')
10. a : mfun-class(X;d;A;d')
11. x = a ∈ mfun-class(X;d;Y;d')
⊢ x ∈ mfun-class(X;d;A;d')
BY
{ (DVar `x' THEN DVar `a' THEN (EqTypeHD (-1) THENA Auto) THEN EqTypeCD THEN Auto THEN All (Unfold `mfun`)) }

1
1. X : Type
2. Y : Type
3. d : metric(X)
4. d' : metric(Y)
5. A : Type
6. strong-subtype(A;Y)
7. ∀a:A. ∀x:Y.  (x ≡ a ⇒ (x ∈ A))
8. mfun-class(X;d;A;d') ⊆r mfun-class(X;d;Y;d')
9. x : Base
10. x1 : Base
11. x = x1 ∈ (f,g:{f:X ⟶ Y| f:FUN(X;Y)} //meqfun(d';X;f;g))
12. x ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
13. x1 ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
14. meqfun(d';X;x;x1)
15. a : Base
16. a1 : Base
17. a = a1 ∈ (f,g:{f:X ⟶ A| f:FUN(X;A)} //meqfun(d';X;f;g))
18. a ∈ {f:X ⟶ A| f:FUN(X;A)} 
19. a1 ∈ {f:X ⟶ A| f:FUN(X;A)} 
20. meqfun(d';X;a;a1)
21. x = a ∈ (f,g:{f:X ⟶ Y| f:FUN(X;Y)} //meqfun(d';X;f;g))
22. x ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
23. a ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
24. meqfun(d';X;x;a)
⊢ x ∈ {f:X ⟶ A| f:FUN(X;A)} 

2
1. X : Type
2. Y : Type
3. d : metric(X)
4. d' : metric(Y)
5. A : Type
6. strong-subtype(A;Y)
7. ∀a:A. ∀x:Y.  (x ≡ a ⇒ (x ∈ A))
8. mfun-class(X;d;A;d') ⊆r mfun-class(X;d;Y;d')
9. x : Base
10. x1 : Base
11. x = x1 ∈ (f,g:{f:X ⟶ Y| f:FUN(X;Y)} //meqfun(d';X;f;g))
12. x ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
13. x1 ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
14. meqfun(d';X;x;x1)
15. a : Base
16. a1 : Base
17. a = a1 ∈ (f,g:{f:X ⟶ A| f:FUN(X;A)} //meqfun(d';X;f;g))
18. a ∈ {f:X ⟶ A| f:FUN(X;A)} 
19. a1 ∈ {f:X ⟶ A| f:FUN(X;A)} 
20. meqfun(d';X;a;a1)
21. x = a ∈ (f,g:{f:X ⟶ Y| f:FUN(X;Y)} //meqfun(d';X;f;g))
22. x ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
23. a ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
24. meqfun(d';X;x;a)
⊢ x1 ∈ {f:X ⟶ A| f:FUN(X;A)} 

---

Latex:

---

Latex:

1.  X  :  Type
2.  Y  :  Type
3.  d  :  metric(X)
4.  d'  :  metric(Y)
5.  A  :  Type
6.  strong-subtype(A;Y)
7.  \mforall{}a:A.  \mforall{}x:Y.    (x  \mequiv{}  a  {}\mRightarrow{}  (x  \mmember{}  A))
8.  mfun-class(X;d;A;d')  \msubseteq{}r  mfun-class(X;d;Y;d')
9.  x  :  mfun-class(X;d;Y;d')
10.  a  :  mfun-class(X;d;A;d')
11.  x  =  a
\mvdash{}  x  \mmember{}  mfun-class(X;d;A;d')


By

---

Latex:
(DVar  `x'
  THEN  DVar  `a'
  THEN  (EqTypeHD  (-1)  THENA  Auto)
  THEN  EqTypeCD
  THEN  Auto
  THEN  All  (Unfold  `mfun`))

---

Home Index