---

Step * of Lemma mset_mem_functionality_wrt_bsubmset

∀s:DSet. ∀a:FiniteSet{s}. ∀b:MSet{s}. ∀u:|s|.  ((↑(a ⊆b b)) ⇒ (↑(u ∈b a ⇒b (u ∈b b))))
BY
{ (Auto THEN (RW assert_pushdownC 0 THENA (Auto THEN Unfold `uimplies` 0 THEN Auto))) }

1
1. s : DSet@i'
2. a : FiniteSet{s}@i
3. b : MSet{s}@i
4. u : |s|@i
5. ↑(a ⊆b b)@i
⊢ ↑(u ∈b b) supposing ↑(u ∈b a)

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:FiniteSet\{s\}.  \mforall{}b:MSet\{s\}.  \mforall{}u:|s|.    ((\muparrow{}(a  \msubseteq{}\msubb{}  b))  {}\mRightarrow{}  (\muparrow{}(u  \mmember{}\msubb{}  a  {}\mRightarrow{}\msubb{}  (u  \mmember{}\msubb{}  b))))


By

---

Latex:
(Auto  THEN  (RW  assert\_pushdownC  0  THENA  (Auto  THEN  Unfold  `uimplies`  0  THEN  Auto)))

---

Home Index