---

Step * of Lemma bmsexists_char

∀s:DSet. ∀f:|s| ⟶ 𝔹. ∀a:MSet{s}.  ((∃x:|s|. ((↑(x ∈b a)) ∧ (↑f[x]))) ⇒ (↑(∃b{s} x ∈ a. f[x])))
BY
{ ((CDToVarThen `a' (\i. 
  CSquash THENM UseEqWitness Ax 
  THENM msetD i THENM EqTypeCD) ) THENA Auto) }

1
1. s : DSet
2. f : |s| ⟶ 𝔹
3. as : |s| List
4. bs : |s| List
5. as ≡(|s|) bs
⊢ (∃x:|s|. ((↑(x ∈b as)) ∧ (↑f[x]))) ⇒ (↑(∃b{s} x ∈ as. f[x]))

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}f:|s|  {}\mrightarrow{}  \mBbbB{}.  \mforall{}a:MSet\{s\}.    ((\mexists{}x:|s|.  ((\muparrow{}(x  \mmember{}\msubb{}  a))  \mwedge{}  (\muparrow{}f[x])))  {}\mRightarrow{}  (\muparrow{}(\mexists{}\msubb{}\{s\}  x  \mmember{}  a.  f[x])))


By

---

Latex:
((CDToVarThen  `a'  (\mbackslash{}i. 
    CSquash  THENM  UseEqWitness  Ax 
    THENM  msetD  i  THENM  EqTypeCD)  )  THENA  Auto)

---

Home Index