let X, Y be set ; Union (disjoin (Y --> X)) = [:X,Y:]
set f = Y --> X;
A1:
dom (Y --> X) = Y
;
thus
Union (disjoin (Y --> X)) c= [:X,Y:]
XBOOLE_0:def 10 [:X,Y:] c= Union (disjoin (Y --> X))proof
let x be
object ;
TARSKI:def 3 ( not x in Union (disjoin (Y --> X)) or x in [:X,Y:] )
assume
x in Union (disjoin (Y --> X))
;
x in [:X,Y:]
then consider Z being
set such that A2:
x in Z
and A3:
Z in rng (disjoin (Y --> X))
by TARSKI:def 4;
consider y being
object such that A4:
y in dom (disjoin (Y --> X))
and A5:
Z = (disjoin (Y --> X)) . y
by A3, FUNCT_1:def 3;
A6:
y in Y
by A1, A4, Def3;
then A7:
Z = [:((Y --> X) . y),{y}:]
by A1, A5, Def3;
A8:
(Y --> X) . y = X
by A6, FUNCOP_1:7;
{y} c= Y
by A6, ZFMISC_1:31;
then
Z c= [:X,Y:]
by A7, A8, ZFMISC_1:95;
hence
x in [:X,Y:]
by A2;
verum
end;
let x1, x2 be object ; RELAT_1:def 3 ( not [x1,x2] in [:X,Y:] or [x1,x2] in Union (disjoin (Y --> X)) )
assume A9:
[x1,x2] in [:X,Y:]
; [x1,x2] in Union (disjoin (Y --> X))
then A10:
x1 in X
by ZFMISC_1:87;
A11:
x2 in Y
by A9, ZFMISC_1:87;
then A12:
(Y --> X) . x2 = X
by FUNCOP_1:7;
A13:
(disjoin (Y --> X)) . x2 = [:((Y --> X) . x2),{x2}:]
by A1, A11, Def3;
A14:
x2 in dom (disjoin (Y --> X))
by A1, A11, Def3;
x2 in {x2}
by TARSKI:def 1;
then A15:
[x1,x2] in [:((Y --> X) . x2),{x2}:]
by A10, A12, ZFMISC_1:87;
[:((Y --> X) . x2),{x2}:] in rng (disjoin (Y --> X))
by A13, A14, FUNCT_1:def 3;
hence
[x1,x2] in Union (disjoin (Y --> X))
by A15, TARSKI:def 4; verum