let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G = {A,B} & A <> B holds
CompF A,G = B
let G be Subset of (PARTITIONS Y); :: thesis: for A, B being a_partition of Y st G = {A,B} & A <> B holds
CompF A,G = B
let A, B be a_partition of Y; :: thesis: ( G = {A,B} & A <> B implies CompF A,G = B )
assume A1: ( G = {A,B} & A <> B ) ; :: thesis: CompF A,G = B
then A2: G \ {A} = ({A} \/ {B}) \ {A} by ENUMSET1:41
.= ({A} \ {A}) \/ ({B} \ {A}) by XBOOLE_1:42
.= ({A} \ {A}) \/ {B} by A1, ZFMISC_1:20 ;
A in {A} by TARSKI:def 1;
then {A} \ {A} = {} by ZFMISC_1:68;
then A3: CompF A,G = '/\' {B} by A2, BVFUNC_2:def 7;
A4: '/\' {B} c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' {B} or x in B )
assume x in '/\' {B} ; :: thesis: x in B
then consider h being Function, F being Subset-Family of Y such that
A5: ( dom h = {B} & rng h = F & ( for d being set st d in {B} holds
h . d in d ) & x = Intersect F & x <> {} ) by BVFUNC_2:def 1;
rng h = {(h . B)} by A5, FUNCT_1:14;
then A6: x = meet {(h . B)} by A5, SETFAM_1:def 10;
B in {B} by TARSKI:def 1;
then h . B in B by A5;
hence x in B by A6, SETFAM_1:11; :: thesis: verum

end;

B c= '/\' {B}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in '/\' {B} )
assume A7: x in B ; :: thesis: x in '/\' {B}
set h0 = B .--> x;
A8: ( dom (B .--> x) = {B} & rng (B .--> x) = {x} ) by FUNCOP_1:14, FUNCOP_1:19;
A9: for d being set st d in {B} holds
(B .--> x) . d in d

proof

let d be set ; :: thesis: ( d in {B} implies (B .--> x) . d in d )
assume d in {B} ; :: thesis: (B .--> x) . d in d
then d = B by TARSKI:def 1;
hence (B .--> x) . d in d by A7, FUNCOP_1:87; :: thesis: verum

end;

rng (B .--> x) c= bool Y

proof

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in rng (B .--> x) or m in bool Y )
assume m in rng (B .--> x) ; :: thesis: m in bool Y
then m = x by A8, TARSKI:def 1;
hence m in bool Y by A7; :: thesis: verum

end;

then reconsider F0 = rng (B .--> x) as Subset-Family of Y ;
meet F0 = Intersect F0 by A8, SETFAM_1:def 10;
then A10: x = Intersect F0 by A8, SETFAM_1:11;
x <> {} by A7, EQREL_1:def 6;
hence x in '/\' {B} by A8, A9, A10, BVFUNC_2:def 1; :: thesis: verum

end;

hence CompF A,G = B by A3, A4, XBOOLE_0:def 10; :: thesis: verum