Step * of Lemma single-valued-bag-combine

`∀[A,B:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ bag(B)].`
`  (single-valued-bag(⋃x∈as.f[x];B)) supposing ((∀a:A. single-valued-bag(f[a];B)) and single-valued-bag(as;A))`
BY
`{ (Auto`
`   THEN D 0`
`   THEN Auto`
`   THEN BagMemberD (-2)`
`   THEN BagMemberD (-1)`
`   THEN SquashExRepD`
`   THEN Unfold `single-valued-bag` (-10)`
`   THEN (InstHyp [⌜x2⌝;⌜x1⌝] (-10)⋅ THENA Auto)`
`   THEN (InstHyp [⌜x1⌝] (-10)⋅ THENA Auto)`
`   THEN Unfold `single-valued-bag` (-1)`
`   THEN InstHyp [⌜x⌝;⌜y⌝] (-1)⋅`
`   THEN Auto) }`

Latex:

Latex:
\mforall{}[A,B:Type].  \mforall{}[as:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].
(single-valued-bag(\mcup{}x\mmember{}as.f[x];B))  supposing
((\mforall{}a:A.  single-valued-bag(f[a];B))  and
single-valued-bag(as;A))

By

Latex:
(Auto
THEN  D  0
THEN  Auto
THEN  BagMemberD  (-2)
THEN  BagMemberD  (-1)
THEN  SquashExRepD
THEN  Unfold  `single-valued-bag`  (-10)
THEN  (InstHyp  [\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]  (-10)\mcdot{}  THENA  Auto)
THEN  (InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (-10)\mcdot{}  THENA  Auto)
THEN  Unfold  `single-valued-bag`  (-1)
THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (-1)\mcdot{}
THEN  Auto)

Home Index