Step
*
of Lemma
setmem-setunionfun
∀s:coSet{i:l}. ∀f:{x:coSet{i:l}| (x ∈ s)} ⟶ coSet{i:l}.
(set-function{i:l}(s; x.f[x])
⇒ (∀y:coSet{i:l}. ((y ∈ ⋃x∈s.f[x])
⇐⇒ ∃x:coSet{i:l}. ((x ∈ s) ∧ (y ∈ f[x])))))
BY
{ (Auto THEN (coSetD 1 THEN D 1) THEN RenameVar `g' 2) }
1
1. T : Type
2. g : T ⟶ coSet{i:l}
3. f : {x:coSet{i:l}| (x ∈ <T, g>)} ⟶ coSet{i:l}
4. set-function{i:l}(<T, g>; x.f[x])
5. y : coSet{i:l}
6. (y ∈ ⋃x∈<T, g>.f[x])
⊢ ∃x:coSet{i:l}. ((x ∈ <T, g>) ∧ (y ∈ f[x]))
2
1. T : Type
2. g : T ⟶ coSet{i:l}
3. f : {x:coSet{i:l}| (x ∈ <T, g>)} ⟶ coSet{i:l}
4. set-function{i:l}(<T, g>; x.f[x])
5. y : coSet{i:l}
6. ∃x:coSet{i:l}. ((x ∈ <T, g>) ∧ (y ∈ f[x]))
⊢ (y ∈ ⋃x∈<T, g>.f[x])
Latex:
Latex:
\mforall{}s:coSet\{i:l\}. \mforall{}f:\{x:coSet\{i:l\}| (x \mmember{} s)\} {}\mrightarrow{} coSet\{i:l\}.
(set-function\{i:l\}(s; x.f[x])
{}\mRightarrow{} (\mforall{}y:coSet\{i:l\}. ((y \mmember{} \mcup{}x\mmember{}s.f[x]) \mLeftarrow{}{}\mRightarrow{} \mexists{}x:coSet\{i:l\}. ((x \mmember{} s) \mwedge{} (y \mmember{} f[x])))))
By
Latex:
(Auto THEN (coSetD 1 THEN D 1) THEN RenameVar `g' 2)
Home
Index