---

Step * of Lemma strong-subtype-iff-preserves-singleton

∀[A,B:Type].  uiff(strong-subtype(A;B);(A ⊆r B) ∧ (∀a:A. ({a:B} ⊆r {a:A})))
BY
{ (Unfold `strong-subtype` 0 THEN Auto THEN D 0 THEN Auto THEN D -1 THEN Auto) }

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

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

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    uiff(strong-subtype(A;B);(A  \msubseteq{}r  B)  \mwedge{}  (\mforall{}a:A.  (\{a:B\}  \msubseteq{}r  \{a:A\})))


By

---

Latex:
(Unfold  `strong-subtype`  0  THEN  Auto  THEN  D  0  THEN  Auto  THEN  D  -1  THEN  Auto)

---

Home Index