🚀 go-pugleaf

On Thu, 29 Apr 2004, Jordi Bataller i Mascarell wrote:

> u : union
> v : or
> E : exists
> A : forall
> == : equivalence
> => : implication
> belongsTo: an element belongs to a set
>
> I want to prove
>
> (1) a belongsTo (u i |: B_i) == (E i | : a belongsTo B_i)
>
> (a belongs to an infinite union of sets iff a belongs
>   to (at least) one of the sets)
>
a in \/{ B_i | i in I } iff some i in I with a in B_i
a in \/C iff some A in C with a in A

It's the definition!!!
\/C = { x | some A in C with x in A }
\/{ B_i | i in I } = { x | some B_i with x in B_i }

> using axiom:
> (2) a belongsTo (B u C) == (a belongsTo B) v (a belongsTo C)
>
a in B\/C iff a in B or a in C

Do that and you'll get to infinitely diddle around with
a in \/{ B_i } iff a in B1 or a in B2 or a in B3 or ....

> I can prove easily by induction:
> (3) (A k |: a belongsTo (u i |i<=k: B_i) == (E i |i<=k: a belongsTo B_i)

> (This is a restriction of (1) for *any* k)
> BUT (and this is the problem)
> how can I prove (3) => (1)

You can't.  You also need to desuade yourself of the notion that
just because some bunch of anythings is infinite, that it's countable,
1,2,3,....  No!  The set of real numbers is infinite and you can't list
them like that, not even with an infinite list.

> or generalize (3) into (1) ?
>
Use the appropiate definitions as included.

> (Of course (1) => (3))
>
Yes, \/{ A,B } = A \/ B;  \/{ A } = A;  \/nulset = nulset