let x be object ; for f being Function holds
( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )
let f be Function; ( x in Union (disjoin f) iff ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )
thus
( x in Union (disjoin f) implies ( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] ) )
( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] implies x in Union (disjoin f) )proof
assume
x in Union (disjoin f)
;
( x `2 in dom f & x `1 in f . (x `2) & x = [(x `1),(x `2)] )
then consider X being
set such that A1:
x in X
and A2:
X in rng (disjoin f)
by TARSKI:def 4;
consider y being
object such that A3:
y in dom (disjoin f)
and A4:
X = (disjoin f) . y
by A2, FUNCT_1:def 3;
A5:
y in dom f
by A3, Def3;
then A6:
X = [:(f . y),{y}:]
by A4, Def3;
then A7:
x `1 in f . y
by A1, MCART_1:10;
x `2 in {y}
by A1, A6, MCART_1:10;
hence
(
x `2 in dom f &
x `1 in f . (x `2) &
x = [(x `1),(x `2)] )
by A1, A5, A6, A7, MCART_1:21, TARSKI:def 1;
verum
end;
assume that
A8:
x `2 in dom f
and
A9:
x `1 in f . (x `2)
and
A10:
x = [(x `1),(x `2)]
; x in Union (disjoin f)
A11:
(disjoin f) . (x `2) = [:(f . (x `2)),{(x `2)}:]
by A8, Def3;
A12:
dom f = dom (disjoin f)
by Def3;
x `2 in {(x `2)}
by TARSKI:def 1;
then A13:
x in [:(f . (x `2)),{(x `2)}:]
by A9, A10, ZFMISC_1:87;
[:(f . (x `2)),{(x `2)}:] in rng (disjoin f)
by A8, A11, A12, FUNCT_1:def 3;
hence
x in Union (disjoin f)
by A13, TARSKI:def 4; verum