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 that
A1: G = {A,B} and
A2: A <> B ; :: thesis: CompF A,G = B
A3: '/\' {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
A4: dom h = {B} and
A5: rng h = F and
A6: for d being set st d in {B} holds
h . d in d and
A7: x = Intersect F and
x <> {} by BVFUNC_2:def 1;
rng h = {(h . B)} by A4, FUNCT_1:14;
then A8: x = meet {(h . B)} by A5, A7, SETFAM_1:def 10;
B in {B} by TARSKI:def 1;
then h . B in B by A6;
hence x in B by A8, SETFAM_1:11; :: thesis: verum

end;

A9: B c= '/\' {B}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in '/\' {B} )
set h0 = B .--> x;
A10: dom (B .--> x) = {B} by FUNCOP_1:19;
assume A11: x in B ; :: thesis: x in '/\' {B}
A12: 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 A11, FUNCOP_1:87; :: thesis: verum

end;

A13: rng (B .--> x) = {x} by FUNCOP_1:14;
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 A13, TARSKI:def 1;
hence m in bool Y by A11; :: thesis: verum

end;

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

end;

A in {A} by TARSKI:def 1;
then A15: {A} \ {A} = {} by ZFMISC_1:68;
G \ {A} = ({A} \/ {B}) \ {A} by A1, ENUMSET1:41
.= ({A} \ {A}) \/ ({B} \ {A}) by XBOOLE_1:42
.= ({A} \ {A}) \/ {B} by A2, ZFMISC_1:20 ;
then CompF A,G = '/\' {B} by A15, BVFUNC_2:def 7;
hence CompF A,G = B by A3, A9, XBOOLE_0:def 10; :: thesis: verum