---

Step * of Lemma strong-subtype-set

∀[A,B:Type].  ∀[P:A ⟶ ℙ]. ∀[Q:B ⟶ ℙ].  strong-subtype({x:A| P[x]} ;{x:B| Q[x]} ) supposing ∀x:A. (P[x] ⇒ Q[x]) suppos\000Cing strong-subtype(A;B)
BY
{ (Auto THEN (FLemma `strong-subtype-implies` [3] THENA Auto) THEN D 3 THEN D 0) }

1
1. A : Type
2. B : Type
3. A ⊆r B
4. {b:B| ∃a:A. (b = a ∈ B)}  ⊆r A
5. P : A ⟶ ℙ
6. Q : B ⟶ ℙ
7. ∀x:A. (P[x] ⇒ Q[x])
8. ∀b:B. ∀a:A.  ((b = a ∈ B) ⇒ (b = a ∈ A))
⊢ {x:A| P[x]}  ⊆r {x:B| Q[x]} 

2
1. A : Type
2. B : Type
3. A ⊆r B
4. {b:B| ∃a:A. (b = a ∈ B)}  ⊆r A
5. P : A ⟶ ℙ
6. Q : B ⟶ ℙ
7. ∀x:A. (P[x] ⇒ Q[x])
8. ∀b:B. ∀a:A.  ((b = a ∈ B) ⇒ (b = a ∈ A))
9. {x:A| P[x]}  ⊆r {x:B| Q[x]} 
⊢ {b:{x:B| Q[x]} | ∃a:{x:A| P[x]} . (b = a ∈ {x:B| Q[x]} )}  ⊆r {x:A| P[x]} 

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:B  {}\mrightarrow{}  \mBbbP{}].    strong-subtype(\{x:A|  P[x]\}  ;\{x:B|  Q[x]\}  )  supposing  \mforall{}x:A.  (P[x]  {}\mRightarrow{}  Q[x]\000C) 
    supposing  strong-subtype(A;B)


By

---

Latex:
(Auto  THEN  (FLemma  `strong-subtype-implies`  [3]  THENA  Auto)  THEN  D  3  THEN  D  0)

---

Home Index