---

Step * of Lemma mset_count_bound_for_union

∀s,s':DSet. ∀n:ℕ. ∀e:|s| ⟶ MSet{s'}. ∀x:|s'|.
  ((∀y:|s|. ((x #∈ e[y]) ≤ n)) ⇒ (∀a:MSet{s}. ((x #∈ (msFor{<MSet{s'},⋃,0>} y ∈ a. e[y])) ≤ n)))
BY
{ ((RepD 
THENM OnVar `a' MoveToConcl 
THENM BLemma `mset_ind_a`) THEN Auto) }

1
1. s : DSet
2. s' : DSet
3. n : ℕ
4. e : |s| ⟶ MSet{s'}
5. x : |s'|
6. ∀y:|s|. ((x #∈ e[y]) ≤ n)
⊢ (x #∈ (msFor{<MSet{s'},⋃,0>} y ∈ 0{s}
           e[y])) ≤ n

2
1. s : DSet
2. s' : DSet
3. n : ℕ
4. e : |s| ⟶ MSet{s'}
5. x : |s'|
6. ∀y:|s|. ((x #∈ e[y]) ≤ n)
7. x1 : |s|
⊢ (x #∈ (msFor{<MSet{s'},⋃,0>} y ∈ mset_inj{s}(x1)
           e[y])) ≤ n

3
1. s : DSet
2. s' : DSet
3. n : ℕ
4. e : |s| ⟶ MSet{s'}
5. x : |s'|
6. ∀y:|s|. ((x #∈ e[y]) ≤ n)
7. ys : MSet{s}
8. ys' : MSet{s}
9. (x #∈ (msFor{<MSet{s'},⋃,0>} y ∈ ys
            e[y])) ≤ n
10. (x #∈ (msFor{<MSet{s'},⋃,0>} y ∈ ys'
             e[y])) ≤ n
⊢ (x #∈ (msFor{<MSet{s'},⋃,0>} y ∈ ys + ys'
           e[y])) ≤ n

---

Latex:

---

Latex:
\mforall{}s,s':DSet.  \mforall{}n:\mBbbN{}.  \mforall{}e:|s|  {}\mrightarrow{}  MSet\{s'\}.  \mforall{}x:|s'|.
    ((\mforall{}y:|s|.  ((x  \#\mmember{}  e[y])  \mleq{}  n))  {}\mRightarrow{}  (\mforall{}a:MSet\{s\}.  ((x  \#\mmember{}  (msFor\{<MSet\{s'\},\mcup{},0>\}  y  \mmember{}  a.  e[y]))  \mleq{}  n)))


By

---

Latex:
((RepD 
THENM  OnVar  `a'  MoveToConcl 
THENM  BLemma  `mset\_ind\_a`)  THEN  Auto)

---

Home Index