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 object ; :: 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:4;
then A8: x = meet {(h . B)} by A5, A7, SETFAM_1:def 9;
B in {B} by TARSKI:def 1;
then h . B in B by A6;
hence x in B by A8, SETFAM_1:10; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in '/\' {B} )
set h0 = B .--> x;
A10: dom (B .--> x) = {B} ;
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:72; :: thesis: verum

end;

A13: rng (B .--> x) = {x} by FUNCOP_1:8;
A14: x is set by TARSKI:1;
rng (B .--> x) c= bool Y

proof

let m be object ; :: 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 9;
then A15: x = Intersect F0 by A13, SETFAM_1:10, A14;
x <> {} by A11, EQREL_1:def 4;
hence x in '/\' {B} by A10, A12, A15, BVFUNC_2:def 1; :: thesis: verum

end;

A in {A} by TARSKI:def 1;
then A16: {A} \ {A} = {} by ZFMISC_1:60;
G \ {A} = ({A} \/ {B}) \ {A} by A1, ENUMSET1:1
.= ({A} \ {A}) \/ ({B} \ {A}) by XBOOLE_1:42
.= ({A} \ {A}) \/ {B} by A2, ZFMISC_1:14 ;
then CompF (A,G) = '/\' {B} by A16, BVFUNC_2:def 7;
hence CompF (A,G) = B by A3, A9; :: thesis: verum