---

Step * of Lemma id-fun-subtype

∀[A,B:Type].  id-fun(B) ⊆r id-fun(A) supposing strong-subtype(A;B)
BY
{ ((UnivCD THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (FLemma `strong-subtype-implies` [3] THENA Auto)
   THEN PromoteHyp (-1) 3
   THEN D 4
   THEN All (Unfold `id-fun`)) }

1
1. A : Type
2. B : Type
3. ∀b:B. ∀a:A.  ((b = a ∈ B) ⇒ (b = a ∈ A))
4. A ⊆r B
5. {b:B| ∃a:A. (b = a ∈ B)}  ⊆r A
6. x : x:B ⟶ {y:B| x = y ∈ B} 
⊢ x ∈ x:A ⟶ {y:A| x = y ∈ A} 

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    id-fun(B)  \msubseteq{}r  id-fun(A)  supposing  strong-subtype(A;B)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (FLemma  `strong-subtype-implies`  [3]  THENA  Auto)
  THEN  PromoteHyp  (-1)  3
  THEN  D  4
  THEN  All  (Unfold  `id-fun`))

---

Home Index