---

Step * 1 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 : 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)} 
BY
{ ((MemTypeHD (-3) THENA Auto)
   THEN (MemTypeCD THENW Auto)
   THEN Try (ParallelOp -3)
   THEN (FunExt THENA Auto)
   THEN RenameVar `p' (-1)) }

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 = x ∈ (X ⟶ Y)
23. x:FUN(X;Y)
24. a ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
25. meqfun(d';X;x;a)
26. p : X
⊢ x p ∈ 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  :  Base
10.  x1  :  Base
11.  x  =  x1
12.  x  \mmember{}  \{f:X  {}\mrightarrow{}  Y|  f:FUN(X;Y)\} 
13.  x1  \mmember{}  \{f:X  {}\mrightarrow{}  Y|  f:FUN(X;Y)\} 
14.  meqfun(d';X;x;x1)
15.  a  :  Base
16.  a1  :  Base
17.  a  =  a1
18.  a  \mmember{}  \{f:X  {}\mrightarrow{}  A|  f:FUN(X;A)\} 
19.  a1  \mmember{}  \{f:X  {}\mrightarrow{}  A|  f:FUN(X;A)\} 
20.  meqfun(d';X;a;a1)
21.  x  =  a
22.  x  \mmember{}  \{f:X  {}\mrightarrow{}  Y|  f:FUN(X;Y)\} 
23.  a  \mmember{}  \{f:X  {}\mrightarrow{}  Y|  f:FUN(X;Y)\} 
24.  meqfun(d';X;x;a)
\mvdash{}  x  \mmember{}  \{f:X  {}\mrightarrow{}  A|  f:FUN(X;A)\} 


By

---

Latex:
((MemTypeHD  (-3)  THENA  Auto)
  THEN  (MemTypeCD  THENW  Auto)
  THEN  Try  (ParallelOp  -3)
  THEN  (FunExt  THENA  Auto)
  THEN  RenameVar  `p'  (-1))

---

Home Index