let S be 1-sorted ; :: thesis: for D being ClosureSystem of S
for f being SetOp of the Sorts of D st ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
( f is reflexive & f is monotonic & f is idempotent )
let D be ClosureSystem of S; :: thesis: for f being SetOp of the Sorts of D st ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) holds
( f is reflexive & f is monotonic & f is idempotent )
let f be SetOp of the Sorts of D; :: thesis: ( ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) implies ( f is reflexive & f is monotonic & f is idempotent ) )
assume A1: for x being Element of Bool the Sorts of D holds f . x = Cl x ; :: thesis: ( f is reflexive & f is monotonic & f is idempotent )
set M = the Sorts of D;
A2: f is reflexive
proof
let x be Element of Bool the Sorts of D; :: according to CLOSURE2:def 10 :: thesis: x c=' f . x
consider F being SubsetFamily of the Sorts of D such that
A3: Cl x = meet |:F:| and
A4: F = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def22;
A5: for Z1 being ManySortedSet of the carrier of S st Z1 in F holds
x c=' Z1
proof
let Z1 be ManySortedSet of the carrier of S; :: thesis: ( Z1 in F implies x c=' Z1 )
assume Z1 in F ; :: thesis: x c=' Z1
then ex a being Element of Bool the Sorts of D st
( Z1 = a & x c=' a & a in the Family of D ) by A4;
hence x c=' Z1 ; :: thesis: verum
end;
f . x = meet |:F:| by A1, A3;
hence x c=' f . x by A5, Th24; :: thesis: verum
end;
A6: f is monotonic
proof
let x, y be Element of Bool the Sorts of D; :: according to CLOSURE2:def 11 :: thesis: ( x c=' y implies f . x c=' f . y )
assume A7: x c=' y ; :: thesis: f . x c=' f . y
consider Fy being SubsetFamily of the Sorts of D such that
A8: Cl y = meet |:Fy:| and
A9: Fy = { X where X is Element of Bool the Sorts of D : ( y c=' X & X in the Family of D ) } by Def22;
consider Fx being SubsetFamily of the Sorts of D such that
A10: Cl x = meet |:Fx:| and
A11: Fx = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def22;
|:Fy:| c=' |:Fx:|
proof
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S or |:Fy:| . i c= |:Fx:| . i )
assume A12: i in the carrier of S ; :: thesis: |:Fy:| . i c= |:Fx:| . i
thus |:Fy:| . i c= |:Fx:| . i :: thesis: verum
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in |:Fy:| . i or q in |:Fx:| . i )
assume A13: q in |:Fy:| . i ; :: thesis: q in |:Fx:| . i
per cases ( Fy is empty or not Fy is empty ) ;
suppose Fy is empty ; :: thesis: q in |:Fx:| . i
then reconsider Fy9 = Fy as empty SubsetFamily of the Sorts of D ;
|:Fy9:| . i is empty ;
hence q in |:Fx:| . i by A13; :: thesis: verum
end;
suppose not Fy is empty ; :: thesis: q in |:Fx:| . i
then |:Fy:| . i = { (e . i) where e is Element of Bool the Sorts of D : e in Fy } by A12, Th14;
then consider w being Element of Bool the Sorts of D such that
A14: q = w . i and
A15: w in Fy by A13;
A16: ex r being Element of Bool the Sorts of D st
( r = w & y c=' r & r in the Family of D ) by A9, A15;
then x c=' w by A7, PBOOLE:13;
then A17: w in Fx by A11, A16;
then |:Fx:| . i = { (e . i) where e is Element of Bool the Sorts of D : e in Fx } by A12, Th14;
hence q in |:Fx:| . i by A14, A17; :: thesis: verum
end;
end;
end;
end;
then meet |:Fx:| c=' meet |:Fy:| by MSSUBFAM:46;
then meet |:Fx:| c=' f . y by A1, A8;
hence f . x c=' f . y by A1, A10; :: thesis: verum
end;
f is idempotent
proof
let x be Element of Bool the Sorts of D; :: according to CLOSURE2:def 12 :: thesis: f . x = f . (f . x)
consider F being SubsetFamily of the Sorts of D such that
A18: Cl x = meet |:F:| and
A19: F = { X where X is Element of Bool the Sorts of D : ( x c=' X & X in the Family of D ) } by Def22;
F c= the Family of D
proof
let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in F or k in the Family of D )
assume k in F ; :: thesis: k in the Family of D
then ex q being Element of Bool the Sorts of D st
( k = q & x c=' q & q in the Family of D ) by A19;
hence k in the Family of D ; :: thesis: verum
end;
then A20: meet |:F:| in the Family of D by Def7;
thus f . x = meet |:F:| by A1, A18
.= f . (meet |:F:|) by A1, A20, Th38
.= f . (f . x) by A1, A18 ; :: thesis: verum
end;
hence ( f is reflexive & f is monotonic & f is idempotent ) by A2, A6; :: thesis: verum