---

Step * 1 2 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 = x1 ∈ (X ⟶ Y)
14. x1:FUN(X;Y)
15. meqfun(d';X;x;x1)
16. a : Base
17. a1 : Base
18. a = a1 ∈ (f,g:{f:X ⟶ A| f:FUN(X;A)} //meqfun(d';X;f;g))
19. a ∈ {f:X ⟶ A| f:FUN(X;A)} 
20. a1 ∈ {f:X ⟶ A| f:FUN(X;A)} 
21. meqfun(d';X;a;a1)
22. x = a ∈ (f,g:{f:X ⟶ Y| f:FUN(X;Y)} //meqfun(d';X;f;g))
23. x ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
24. a ∈ {f:X ⟶ Y| f:FUN(X;Y)} 
25. meqfun(d';X;x;a)
26. p : X
⊢ x1 p ∈ A
BY
{ Assert ⌜meqfun(d';X;x1;a)⌝⋅ }

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


By

---

Latex:
Assert  \mkleeneopen{}meqfun(d';X;x1;a)\mkleeneclose{}\mcdot{}

---

Home Index