let A be set ; for f being Function st A c= bool (dom f) & f is one-to-one holds
union ((" f) " A) = f .: (union A)
let f be Function; ( A c= bool (dom f) & f is one-to-one implies union ((" f) " A) = f .: (union A) )
assume that
A1:
A c= bool (dom f)
and
A2:
f is one-to-one
; union ((" f) " A) = f .: (union A)
A3:
f .: (union A) c= union ((" f) " A)
proof
let y be
set ;
TARSKI:def 3 ( not y in f .: (union A) or y in union ((" f) " A) )
assume
y in f .: (union A)
;
y in union ((" f) " A)
then consider x being
set such that A4:
x in dom f
and A5:
x in union A
and A6:
y = f . x
by FUNCT_1:def 6;
consider X being
set such that A7:
x in X
and A8:
X in A
by A5, TARSKI:def 4;
A9:
f " (f .: X) c= X
by A2, FUNCT_1:82;
A10:
f .: X c= rng f
by RELAT_1:111;
then
f .: X in bool (rng f)
;
then A11:
f .: X in dom (" f)
by Def2;
X c= f " (f .: X)
by A1, A8, FUNCT_1:76;
then
f " (f .: X) = X
by A9, XBOOLE_0:def 10;
then
(" f) . (f .: X) in A
by A8, A10, Def2;
then A12:
f .: X in (" f) " A
by A11, FUNCT_1:def 7;
y in f .: X
by A4, A6, A7, FUNCT_1:def 6;
hence
y in union ((" f) " A)
by A12, TARSKI:def 4;
verum
end;
union ((" f) " A) c= f .: (union A)
by Th31;
hence
union ((" f) " A) = f .: (union A)
by A3, XBOOLE_0:def 10; verum