---

Step * 1 of Lemma bsubmset_functionality_wrt_bsubmset


1. s : DSet
⊢ ∀a,a',b,b':MSet{s}.  ((↑(b ⊆b a)) ⇒ (↑(a' ⊆b b')) ⇒ (↑(a ⊆b a' ⇒b (b ⊆b b'))))
BY
{ ((RW mset_elimC 0) THENA (Auto THEN Unfold `uimplies` 0 THEN Auto)) }

1
1. s : DSet
⊢ ∀a,a',b,b':|s| List.
    ((↑(mk_mset(b) ⊆b mk_mset(a)))
    ⇒ (↑(mk_mset(a') ⊆b mk_mset(b')))
    ⇒ (↑(mk_mset(a) ⊆b mk_mset(a') ⇒b (mk_mset(b) ⊆b mk_mset(b')))))

---

Latex:

---

Latex:

1.  s  :  DSet
\mvdash{}  \mforall{}a,a',b,b':MSet\{s\}.    ((\muparrow{}(b  \msubseteq{}\msubb{}  a))  {}\mRightarrow{}  (\muparrow{}(a'  \msubseteq{}\msubb{}  b'))  {}\mRightarrow{}  (\muparrow{}(a  \msubseteq{}\msubb{}  a'  {}\mRightarrow{}\msubb{}  (b  \msubseteq{}\msubb{}  b'))))


By

---

Latex:
((RW  mset\_elimC  0)  THENA  (Auto  THEN  Unfold  `uimplies`  0  THEN  Auto))

---

Home Index