reconsider f = id (Bool M) as SetOp of M ;

take f ; :: thesis: ( f is algebraic & f is reflexive & f is monotonic & f is idempotent )

thus f is algebraic :: thesis: ( f is reflexive & f is monotonic & f is idempotent )

thus f is monotonic ; :: thesis: f is idempotent

thus f is idempotent ; :: thesis: verum

take f ; :: thesis: ( f is algebraic & f is reflexive & f is monotonic & f is idempotent )

thus f is algebraic :: thesis: ( f is reflexive & f is monotonic & f is idempotent )

proof

thus
f is reflexive
; :: thesis: ( f is monotonic & f is idempotent )
let x be Element of Bool M; :: according to CLOSURE3:def 3 :: thesis: ( x = f . x implies ex A being SubsetFamily of M st

( A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A ) )

assume x = f . x ; :: thesis: ex A being SubsetFamily of M st

( A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A )

set A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } ;

{ (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } c= Bool M

take A ; :: thesis: ( A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A )

thus A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } ; :: thesis: x = MSUnion A

let i be Element of I; :: according to PBOOLE:def 21 :: thesis: x . i = (MSUnion A) . i

thus x . i c= (MSUnion A) . i :: according to XBOOLE_0:def 10 :: thesis: (MSUnion A) . i c= x . i

assume v in (MSUnion A) . i ; :: thesis: v in x . i

then v in union { (ff . i) where ff is Element of Bool M : ff in A } by Def2;

then consider Y being set such that

A3: v in Y and

A4: Y in { (ff . i) where ff is Element of Bool M : ff in A } by TARSKI:def 4;

consider ff being Element of Bool M such that

A5: Y = ff . i and

A6: ff in A by A4;

consider a being Element of Bool M such that

A7: ff = f . a and

a is V45() and

support a is finite and

A8: a c= x by A6;

ff = a by A7;

then ff . i c= x . i by A8;

hence v in x . i by A3, A5; :: thesis: verum

end;( A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A ) )

assume x = f . x ; :: thesis: ex A being SubsetFamily of M st

( A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A )

set A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } ;

{ (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } c= Bool M

proof

then reconsider A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } as SubsetFamily of M ;
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } or v in Bool M )

assume v in { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } ; :: thesis: v in Bool M

then ex a being Element of Bool M st

( v = f . a & a is V45() & support a is finite & a c= x ) ;

hence v in Bool M ; :: thesis: verum

end;assume v in { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } ; :: thesis: v in Bool M

then ex a being Element of Bool M st

( v = f . a & a is V45() & support a is finite & a c= x ) ;

hence v in Bool M ; :: thesis: verum

take A ; :: thesis: ( A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A )

thus A = { (f . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } ; :: thesis: x = MSUnion A

let i be Element of I; :: according to PBOOLE:def 21 :: thesis: x . i = (MSUnion A) . i

thus x . i c= (MSUnion A) . i :: according to XBOOLE_0:def 10 :: thesis: (MSUnion A) . i c= x . i

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in (MSUnion A) . i or v in x . i )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x . i or y in (MSUnion A) . i )

assume y in x . i ; :: thesis: y in (MSUnion A) . i

then consider a being Element of Bool M such that

A1: y in a . i and

A2: ( a is V45() & support a is finite & a c= x ) by Th7;

a = f . a ;

then a in A by A2;

then a . i in { (g . i) where g is Element of Bool M : g in A } ;

then y in union { (g . i) where g is Element of Bool M : g in A } by A1, TARSKI:def 4;

hence y in (MSUnion A) . i by Def2; :: thesis: verum

end;assume y in x . i ; :: thesis: y in (MSUnion A) . i

then consider a being Element of Bool M such that

A1: y in a . i and

A2: ( a is V45() & support a is finite & a c= x ) by Th7;

a = f . a ;

then a in A by A2;

then a . i in { (g . i) where g is Element of Bool M : g in A } ;

then y in union { (g . i) where g is Element of Bool M : g in A } by A1, TARSKI:def 4;

hence y in (MSUnion A) . i by Def2; :: thesis: verum

assume v in (MSUnion A) . i ; :: thesis: v in x . i

then v in union { (ff . i) where ff is Element of Bool M : ff in A } by Def2;

then consider Y being set such that

A3: v in Y and

A4: Y in { (ff . i) where ff is Element of Bool M : ff in A } by TARSKI:def 4;

consider ff being Element of Bool M such that

A5: Y = ff . i and

A6: ff in A by A4;

consider a being Element of Bool M such that

A7: ff = f . a and

a is V45() and

support a is finite and

A8: a c= x by A6;

ff = a by A7;

then ff . i c= x . i by A8;

hence v in x . i by A3, A5; :: thesis: verum

thus f is monotonic ; :: thesis: f is idempotent

thus f is idempotent ; :: thesis: verum