let Y be non empty set ; :: thesis: '/\' ({} (PARTITIONS Y)) = %O Y

for x being set holds

( x in %O Y iff ex h being Function ex F being Subset-Family of Y st

( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} ) )

for x being set holds

( x in %O Y iff ex h being Function ex F being Subset-Family of Y st

( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} ) )

proof

hence
'/\' ({} (PARTITIONS Y)) = %O Y
by BVFUNC_2:def 1; :: thesis: verum
let x be set ; :: thesis: ( x in %O Y iff ex h being Function ex F being Subset-Family of Y st

( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} ) )

for d being set st d in {} (PARTITIONS Y) holds

h . d in d and

A3: x = Intersect F and

x <> {} ; :: thesis: x in %O Y

F = {} by A2, RELAT_1:42;

then x = Y by A3, SETFAM_1:def 9;

then x in {Y} by TARSKI:def 1;

hence x in %O Y by PARTIT1:def 8; :: thesis: verum

end;( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} ) )

hereby :: thesis: ( ex h being Function ex F being Subset-Family of Y st

( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} ) implies x in %O Y )

given h being Function, F being Subset-Family of Y such that A2:
( dom h = {} (PARTITIONS Y) & rng h = F )
and ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} ) implies x in %O Y )

reconsider h = {} as Function ;

assume x in %O Y ; :: thesis: ex h being Function ex F being Element of bool (bool Y) st

( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

then A1: x in {Y} by PARTIT1:def 8;

take h = h; :: thesis: ex F being Element of bool (bool Y) st

( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

take F = {} (bool Y); :: thesis: ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

thus dom h = {} (PARTITIONS Y) ; :: thesis: ( rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

thus rng h = F ; :: thesis: ( ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

thus for d being set st d in {} (PARTITIONS Y) holds

h . d in d ; :: thesis: ( x = Intersect F & x <> {} )

x = Y by A1, TARSKI:def 1;

hence x = Intersect F by SETFAM_1:def 9; :: thesis: x <> {}

thus x <> {} by A1, TARSKI:def 1; :: thesis: verum

end;assume x in %O Y ; :: thesis: ex h being Function ex F being Element of bool (bool Y) st

( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

then A1: x in {Y} by PARTIT1:def 8;

take h = h; :: thesis: ex F being Element of bool (bool Y) st

( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

take F = {} (bool Y); :: thesis: ( dom h = {} (PARTITIONS Y) & rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

thus dom h = {} (PARTITIONS Y) ; :: thesis: ( rng h = F & ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

thus rng h = F ; :: thesis: ( ( for d being set st d in {} (PARTITIONS Y) holds

h . d in d ) & x = Intersect F & x <> {} )

thus for d being set st d in {} (PARTITIONS Y) holds

h . d in d ; :: thesis: ( x = Intersect F & x <> {} )

x = Y by A1, TARSKI:def 1;

hence x = Intersect F by SETFAM_1:def 9; :: thesis: x <> {}

thus x <> {} by A1, TARSKI:def 1; :: thesis: verum

for d being set st d in {} (PARTITIONS Y) holds

h . d in d and

A3: x = Intersect F and

x <> {} ; :: thesis: x in %O Y

F = {} by A2, RELAT_1:42;

then x = Y by A3, SETFAM_1:def 9;

then x in {Y} by TARSKI:def 1;

hence x in %O Y by PARTIT1:def 8; :: thesis: verum