let X' be set ; :: thesis: for F being Function holds (union (rng F)) /\ X' = union (rng (Intersect F,((dom F) --> X')))
let F be Function; :: thesis: (union (rng F)) /\ X' = union (rng (Intersect F,((dom F) --> X')))
set I = Intersect F,((dom F) --> X');
thus
(union (rng F)) /\ X' c= union (rng (Intersect F,((dom F) --> X')))
:: according to XBOOLE_0:def 10 :: thesis: union (rng (Intersect F,((dom F) --> X'))) c= (union (rng F)) /\ X'proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (union (rng F)) /\ X' or x in union (rng (Intersect F,((dom F) --> X'))) )
assume A1:
x in (union (rng F)) /\ X'
;
:: thesis: x in union (rng (Intersect F,((dom F) --> X')))
A2:
x in X'
by A1, XBOOLE_0:def 4;
x in union (rng F)
by A1, XBOOLE_0:def 4;
then consider Fx being
set such that A3:
x in Fx
and A4:
Fx in rng F
by TARSKI:def 4;
consider x1 being
set such that A5:
x1 in dom F
and A6:
F . x1 = Fx
by A4, FUNCT_1:def 5;
x1 in dom (Intersect F,((dom F) --> X'))
by A5, Th57;
then A7:
(Intersect F,((dom F) --> X')) . x1 in rng (Intersect F,((dom F) --> X'))
by FUNCT_1:def 5;
(Intersect F,((dom F) --> X')) . x1 = Fx /\ X'
by A5, A6, Th57;
then
x in (Intersect F,((dom F) --> X')) . x1
by A3, A2, XBOOLE_0:def 4;
hence
x in union (rng (Intersect F,((dom F) --> X')))
by A7, TARSKI:def 4;
:: thesis: verum
end;
thus
union (rng (Intersect F,((dom F) --> X'))) c= (union (rng F)) /\ X'
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in union (rng (Intersect F,((dom F) --> X'))) or x in (union (rng F)) /\ X' )
assume
x in union (rng (Intersect F,((dom F) --> X')))
;
:: thesis: x in (union (rng F)) /\ X'
then consider Ix being
set such that A8:
x in Ix
and A9:
Ix in rng (Intersect F,((dom F) --> X'))
by TARSKI:def 4;
consider x1 being
set such that A10:
x1 in dom (Intersect F,((dom F) --> X'))
and A11:
(Intersect F,((dom F) --> X')) . x1 = Ix
by A9, FUNCT_1:def 5;
A12:
x1 in dom F
by A10, Th57;
then A13:
F . x1 in rng F
by FUNCT_1:def 5;
A14:
(Intersect F,((dom F) --> X')) . x1 = (F . x1) /\ X'
by A12, Th57;
then
x in F . x1
by A8, A11, XBOOLE_0:def 4;
then A15:
x in union (rng F)
by A13, TARSKI:def 4;
x in X'
by A8, A11, A14, XBOOLE_0:def 4;
hence
x in (union (rng F)) /\ X'
by A15, XBOOLE_0:def 4;
:: thesis: verum
end;