---

Step * 1 of Lemma W_subtype


1. A1 : Type
2. A2 : Type
3. B1 : A1 ⟶ Type
4. B2 : A2 ⟶ Type
5. A1 ⊆r A2
6. ∀a:A1. (B2[a] ⊆r B1[a])
7. a : A1
8. f : B1[a] ⟶ W(A1;a.B1[a])
9. ∀b:B1[a]. (f b ∈ W(A2;a.B2[a]))
⊢ Wsup(a;f) ∈ W(A2;a.B2[a])
BY
{ (Auto THEN ExtWith [`b'] [⌜B1[a] ⟶ W(A1;a.B1[a])⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A1  :  Type
2.  A2  :  Type
3.  B1  :  A1  {}\mrightarrow{}  Type
4.  B2  :  A2  {}\mrightarrow{}  Type
5.  A1  \msubseteq{}r  A2
6.  \mforall{}a:A1.  (B2[a]  \msubseteq{}r  B1[a])
7.  a  :  A1
8.  f  :  B1[a]  {}\mrightarrow{}  W(A1;a.B1[a])
9.  \mforall{}b:B1[a].  (f  b  \mmember{}  W(A2;a.B2[a]))
\mvdash{}  Wsup(a;f)  \mmember{}  W(A2;a.B2[a])


By

---

Latex:
(Auto  THEN  ExtWith  [`b']  [\mkleeneopen{}B1[a]  {}\mrightarrow{}  W(A1;a.B1[a])\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index