[Apronus Home] [ProvenMath] [Set Theory]
play piano online
Play Piano Online

INFINITE UNION AND INTERSECTION

Theorem S.IS.1
If X is a set, T is a set such that T != O,
A:T->P(X), x:-X then 
(1) x:-u({A(t)|t:-T}) <=> \/(t:-T) x:-A(t),
(2) x:-n({A(t)|t:-T}) <=> /\(t:-T) x:-A(t).

Proof
Let E = {A(t) | t:-T}.
Notice that since T != O, E != O.
(1) 
By Definition S.A.3
x:-u(E) <=> \/(e) e:-E and x:-e <=>
(a) \/(e) e:-{A(t) | t:-T} and x:-e <=>
(b) \/(e)(e:-{y:-P(X) | \/(t:-T) A(t)=y} and x:-e ) <=>
(c) \/(e)( (e:-P(X) and \/(t:-T) A(t)=e) and x:-e ) <=>
(d) \/(e)\/(t:-T) A(t)=e and x:-e <=>
(e) \/(t:-T)\/(e) A(t)=e and x:-e <=>
(f) \/(t:-T) x:-A(t).

(a)<=>(b) by Definition S.C.15

(2)
By Definition S.I.2
x:-n(E) <=> x:-{a:-u(E) | /\(e:-E) a:-e} <=>
(g) x:-u(E) and /\(e:-E) x:-e <=>
(h) /\(e:-E) x:-e <=>
(i) /\(e) (e:-E => x:-e) <=>
(j) /\(e) (e:-P(X) and \/(t:-T) A(t)=e) => x:-e <=>
(k) /\(e) (\/(t:-T) A(t)=e)=> x:-e <=>
(l) /\(e)/\(t:-T) A(t)=e => x:-e <=>
(m) /\(t:-T)/\(e) A(t)=e => x:-e <=>
(n) /\(t:-T) x:-A(t).  

Theorem S.IS.2 - De Morgan's law
If X is a set, T is a set such that T != O, 
A:T->P(X) then 
X\u({A(t)|t:-T}) = n({X\A(t)|t:-T}).

Proof
Let L = X\u({A(t)|t:-T}).
Let R = n({X\A(t)|t:-T}).

We will show that R c L.
Suppose to the contrary that there exists x:-X
such that !(x:-L) and x:-R.
We have x:-u({A(t)|t:-T}) and x:-n({X\A(t)|t:-T}).
By Theorem S.SI.1 we have
\/(t:-T) x:-A(t)  and  /\(t:-T) x:-X\A(t).
Contradiction.
So we showed that R c L.

Now we will show that L c R.
Suppose to the contrary that there exists x:-X
such that x:-L and !(x:-R).
Then we have !(x:-u({A(t)|t:-T})
and !(x:-n({A(t)|t:-T})).
By Theorem S.SI.1 we have
!(\/(t:-T) x:-A(t)) and !(/\(t:-T) x:-X\A(t)).
/\(t:-T) !(x:-A(t)) and !(/\(t:-T) !(x:-A(t)).
Contradiction.
So we showed that L c R.

Thus L = R.

Theorem S.IS.3 - De Morgan's law
If X is a set, T is a set such that T != O, 
A:T->P(X) then 
X\n({A(t)|t:-T}) = u({X\A(t)|t:-T}).

Proof
Let B:T->P(X) such that B(t) = X\A(t).
By Theorem S.I.8 (3) X\A(t) = B(t).
By Theorem S.IS.3 we have
X\u({B(t)|t:-T}) = n({X\B(t)|t:-T}).
So X\(X\u({B(t)|t:-T}) = X\n({X\B(t)|t:-T}).
And then 
u({B(t)|t:-T}) = X\n({X\B(t)|t:-T}).
Thus u({X\A(t)|t:-T}) = X\n({A(t)|t:-T}.

Theorem S.IS.4
If X,Y are sets, f:X->Y and A,B c X
and T is a set, T!=O and A:T->P(X).
then 
(1) A c B => f(A) c f(B),
(2) f(A\B) c f(A)\f(B),
(3) u({f(A[t])|t:-T}) = f( u({A[t]|t:-T}) ),
(4) f( n({A[t]|t:-T}) ) c n({f(A[t])|t:-T}).

Proof
(1)
Assume that AcB.
Take y:-f(A). There exists x:-A such that f(x)=y.
Since A c B, x:-B. Thus y:-f(B).
We have shown that A c B. 

(2)
Take y:-f(A)\f(B). Then y:-f(A) and !(y:-f(B)).
So there exists x:-A such that and f(x)=y.
Since !(y:-f(B)), /\(z:-B) f(z)!=y. Hence f(x)!=y.
So x:-A\B. Thus y:-f(A\B).
We have shown that f(A)\f(B) c f(A\B).

(3)
y:- u({f(A[t])|t:-T}) <=> \/(t:-T) y:-f(A[t]) <=>
\/(t:-T)\/(x:-X)(x:-A[t] and f(x) = y) <=>
\/(x:-X)\/(t:-T)(x:-A[t] and f(x) = y)<=>
\/(x:-X)(\/(t:-T) x:-A[t]) and  f(x) = y <=>
\/(x:-X) x:-u({A[t]|t:-T) and f(x) = y <=>
y :- f(u({A[t]|t:-T})).
We have shown that u({f(A[t])|t:-T}) = f( u({A[t]|t:-T}) ).

(4)
Take any y:-f( n({A[t]|t:-T}) ).
Then there exist x:-n({A[t]|t:-T}) such that f(x) = y.
Take any d:-T.
Since x:-n({A[t]|t:-T}), x:-A[d].
Then y:-f(A[d]).
Since d:-T was arbitralily chosen, y:-n({f(A[t])|t:-T}).
We have shown that f( {(A[t])|t:-T} ) c n({f(A[t])|t:-T}).

Theorem S.IS.5
If X,M are sets such that M!=O and M c P(X)
then n(M) = {x:-X | /\(A:-M) x:-A}.

Proof
Let us recall that
n(M) = {x:-u(M) | /\(A:-M) x:-A}.

Take any y:-n(M).
We have that y:-u(M) and /\(A:-M) y:-A.
So we have B:-M such that y:-B.
Since M c P(X), B c X, and so y:-X.
Thus y:-{x:-X | /\(A:-M) y:-A}.
We showed that n(M) c {x:-X | /\(A:-M) x:-A}.

Take any y:-{x:-X | /\(A:-M) x:-A}.
We have that (*) /\(A:-M) y:-A.
Since M!=O we have some B:-M.
By (*) y:-B and so y:-u(M).
Thus y:-{x:-u(M) | /\(A:-M) x:-A}.
We showed that
{x:-X | /\(A:-M) x:-A} c {x:-u(M) | /\(A:-M) x:-A} = n(M).

So we showed that n(M) = {x:-X | /\(A:-M) x:-A}.
 

[Apronus Home] [Contact Page] [Provanmath Notation]