---

Step * of Lemma subtype_rel_nested_set2

∀[A,B:Type]. ∀[P:B ⟶ ℙ]. ∀[Q:{b:B| P[b]}  ⟶ ℙ].  {b:{b:B| P[b]} | Q[b]}  ⊆r A supposing {b:B| P[b] ∧ Q[b]}  ⊆r A
BY
{ (Auto THEN UseTrans ⌜{b:B| P[b] ∧ Q[b]} ⌝⋅ THEN Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:B  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:\{b:B|  P[b]\}    {}\mrightarrow{}  \mBbbP{}].
    \{b:\{b:B|  P[b]\}  |  Q[b]\}    \msubseteq{}r  A  supposing  \{b:B|  P[b]  \mwedge{}  Q[b]\}    \msubseteq{}r  A


By

---

Latex:
(Auto  THEN  UseTrans  \mkleeneopen{}\{b:B|  P[b]  \mwedge{}  Q[b]\}  \mkleeneclose{}\mcdot{}  THEN  Auto  THEN  D  0  THEN  Auto)

---

Home Index