let X be non empty set ; :: thesis: for B being non empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds

FinMeetCl B c= UniCl B

let B be non empty Subset-Family of X; :: thesis: ( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B implies FinMeetCl B c= UniCl B )

assume that

A1: for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB and

A2: X = union B ; :: thesis: FinMeetCl B c= UniCl B

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in FinMeetCl B or x in UniCl B )

assume A3: x in FinMeetCl B ; :: thesis: x in UniCl B

then reconsider x0 = x as Subset of X ;

consider Y being Subset-Family of X such that

A4: Y c= B and

A5: Y is finite and

A6: x0 = Intersect Y by A3, CANTOR_1:def 3;

defpred S_{1}[ Nat] means for Y being Subset-Family of X

for x being Subset of X st Y c= B & card Y = $1 & x = Intersect Y holds

x in UniCl B;

A7: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A7, A11);

reconsider CY = card Y as Nat by A5;

S_{1}[CY]
by A50;

hence x in UniCl B by A4, A6; :: thesis: verum

FinMeetCl B c= UniCl B

let B be non empty Subset-Family of X; :: thesis: ( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B implies FinMeetCl B c= UniCl B )

assume that

A1: for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB and

A2: X = union B ; :: thesis: FinMeetCl B c= UniCl B

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in FinMeetCl B or x in UniCl B )

assume A3: x in FinMeetCl B ; :: thesis: x in UniCl B

then reconsider x0 = x as Subset of X ;

consider Y being Subset-Family of X such that

A4: Y c= B and

A5: Y is finite and

A6: x0 = Intersect Y by A3, CANTOR_1:def 3;

defpred S

for x being Subset of X st Y c= B & card Y = $1 & x = Intersect Y holds

x in UniCl B;

A7: S

proof

A11:
for k being Nat st S
let Y be Subset-Family of X; :: thesis: for x being Subset of X st Y c= B & card Y = 0 & x = Intersect Y holds

x in UniCl B

let x be Subset of X; :: thesis: ( Y c= B & card Y = 0 & x = Intersect Y implies x in UniCl B )

assume that

Y c= B and

A8: card Y = 0 and

A9: x = Intersect Y ; :: thesis: x in UniCl B

Y = {} by A8;

then A10: x = X by A9, SETFAM_1:def 9;

reconsider x0 = x as set ;

thus x in UniCl B by A2, A10, CANTOR_1:def 1; :: thesis: verum

end;x in UniCl B

let x be Subset of X; :: thesis: ( Y c= B & card Y = 0 & x = Intersect Y implies x in UniCl B )

assume that

Y c= B and

A8: card Y = 0 and

A9: x = Intersect Y ; :: thesis: x in UniCl B

Y = {} by A8;

then A10: x = X by A9, SETFAM_1:def 9;

reconsider x0 = x as set ;

thus x in UniCl B by A2, A10, CANTOR_1:def 1; :: thesis: verum

S

proof

A50:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A12: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let Y be Subset-Family of X; :: thesis: for x being Subset of X st Y c= B & card Y = k + 1 & x = Intersect Y holds

x in UniCl B

let x be Subset of X; :: thesis: ( Y c= B & card Y = k + 1 & x = Intersect Y implies x in UniCl B )

assume that

A13: Y c= B and

A14: card Y = k + 1 and

A15: x = Intersect Y ; :: thesis: x in UniCl B

Y is finite set by A14;

then consider x1 being Element of Y, C being Subset of Y such that

A16: Y = C \/ {x1} and

A17: card C = k by A14, PRE_CIRC:24;

A18: ( C c= B & card C = k ) by A13, A17;

B c= bool X ;

then C c= bool X by A13;

then reconsider C0 = C as Subset-Family of X ;

end;assume A12: S

let Y be Subset-Family of X; :: thesis: for x being Subset of X st Y c= B & card Y = k + 1 & x = Intersect Y holds

x in UniCl B

let x be Subset of X; :: thesis: ( Y c= B & card Y = k + 1 & x = Intersect Y implies x in UniCl B )

assume that

A13: Y c= B and

A14: card Y = k + 1 and

A15: x = Intersect Y ; :: thesis: x in UniCl B

Y is finite set by A14;

then consider x1 being Element of Y, C being Subset of Y such that

A16: Y = C \/ {x1} and

A17: card C = k by A14, PRE_CIRC:24;

A18: ( C c= B & card C = k ) by A13, A17;

B c= bool X ;

then C c= bool X by A13;

then reconsider C0 = C as Subset-Family of X ;

per cases
( C = {} or C <> {} )
;

end;

suppose A19:
C = {}
; :: thesis: x in UniCl B

meet {x1} = x1
by SETFAM_1:10;

then A20: Intersect Y = x1 by A19, A16, SETFAM_1:def 9;

then x1 in bool X ;

then {x1} c= bool X by TARSKI:def 1;

then reconsider B0 = {x1} as Subset-Family of X ;

x1 in Y by A16;

then A21: ( {x1} c= Y & Y c= B ) by A13, TARSKI:def 1;

( x in B & B0 c= B & x = union B0 ) by A16, A21, A15, A20;

hence x in UniCl B by CANTOR_1:def 1; :: thesis: verum

end;then A20: Intersect Y = x1 by A19, A16, SETFAM_1:def 9;

then x1 in bool X ;

then {x1} c= bool X by TARSKI:def 1;

then reconsider B0 = {x1} as Subset-Family of X ;

x1 in Y by A16;

then A21: ( {x1} c= Y & Y c= B ) by A13, TARSKI:def 1;

( x in B & B0 c= B & x = union B0 ) by A16, A21, A15, A20;

hence x in UniCl B by CANTOR_1:def 1; :: thesis: verum

suppose A22:
C <> {}
; :: thesis: x in UniCl B

then
meet (C \/ {x1}) = (meet C) /\ (meet {x1})
by SETFAM_1:9;

then A23: meet Y = (meet C) /\ x1 by A16, SETFAM_1:10;

meet Y = Intersect Y by A16, SETFAM_1:def 9;

then A24: Intersect Y = (Intersect C0) /\ x1 by A22, A23, SETFAM_1:def 9;

Intersect Y in UniCl B

end;then A23: meet Y = (meet C) /\ x1 by A16, SETFAM_1:10;

meet Y = Intersect Y by A16, SETFAM_1:def 9;

then A24: Intersect Y = (Intersect C0) /\ x1 by A22, A23, SETFAM_1:def 9;

Intersect Y in UniCl B

proof

hence
x in UniCl B
by A15; :: thesis: verum
Intersect C0 in UniCl B
by A18, A12;

then consider Y2 being Subset-Family of X such that

A25: Y2 c= B and

A26: Intersect C0 = union Y2 by CANTOR_1:def 1;

end;then consider Y2 being Subset-Family of X such that

A25: Y2 c= B and

A26: Intersect C0 = union Y2 by CANTOR_1:def 1;

per cases
( Y2 is empty or not Y2 is empty )
;

end;

suppose A27:
Y2 is empty
; :: thesis: Intersect Y in UniCl B

{} c= X
;

then reconsider x0 = {} as Subset of X ;

A28: ( {} c= bool X & {} c= B & {} = union {} ) by ZFMISC_1:2;

then reconsider S = {} as Subset-Family of X ;

thus Intersect Y in UniCl B by A27, A24, A26, A28, CANTOR_1:def 1; :: thesis: verum

end;then reconsider x0 = {} as Subset of X ;

A28: ( {} c= bool X & {} c= B & {} = union {} ) by ZFMISC_1:2;

then reconsider S = {} as Subset-Family of X ;

thus Intersect Y in UniCl B by A27, A24, A26, A28, CANTOR_1:def 1; :: thesis: verum

suppose A29:
not Y2 is empty
; :: thesis: Intersect Y in UniCl B

set Y3 = { (y /\ x1) where y is Element of Y2 : verum } ;

{ (y /\ x1) where y is Element of Y2 : verum } c= bool X

A33: union Y3 = (union Y2) /\ x1

hence Intersect Y in UniCl B by YELLOW_9:15; :: thesis: verum

end;{ (y /\ x1) where y is Element of Y2 : verum } c= bool X

proof

then reconsider Y3 = { (y /\ x1) where y is Element of Y2 : verum } as Subset-Family of X ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (y /\ x1) where y is Element of Y2 : verum } or x in bool X )

assume A30: x in { (y /\ x1) where y is Element of Y2 : verum } ; :: thesis: x in bool X

then reconsider x = x as Element of { (y /\ x1) where y is Element of Y2 : verum } ;

consider y being Element of Y2 such that

A31: x = y /\ x1 by A30;

A32: x c= x1 by A31, XBOOLE_1:17;

( x1 in Y & Y c= bool X ) by A16;

then x1 c= X ;

then x c= X by A32;

hence x in bool X ; :: thesis: verum

end;assume A30: x in { (y /\ x1) where y is Element of Y2 : verum } ; :: thesis: x in bool X

then reconsider x = x as Element of { (y /\ x1) where y is Element of Y2 : verum } ;

consider y being Element of Y2 such that

A31: x = y /\ x1 by A30;

A32: x c= x1 by A31, XBOOLE_1:17;

( x1 in Y & Y c= bool X ) by A16;

then x1 c= X ;

then x c= X by A32;

hence x in bool X ; :: thesis: verum

A33: union Y3 = (union Y2) /\ x1

proof

assume x in (union Y2) /\ x1 ; :: thesis: x in union Y3

then A38: ( x in union Y2 & x in x1 ) by XBOOLE_0:def 4;

then consider a being set such that

A39: x in a and

A40: a in Y2 by TARSKI:def 4;

reconsider a = a as Element of Y2 by A40;

A41: x in a /\ x1 by A38, A39, XBOOLE_0:def 4;

a /\ x1 in Y3 ;

hence x in union Y3 by A41, TARSKI:def 4; :: thesis: verum

end;

A42:
Intersect Y = union Y3
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (union Y2) /\ x1 c= union Y3

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union Y2) /\ x1 or x in union Y3 )let x be object ; :: thesis: ( x in union Y3 implies x in (union Y2) /\ x1 )

assume A34: x in union Y3 ; :: thesis: x in (union Y2) /\ x1

consider a1 being set such that

A35: x in a1 and

A36: a1 in Y3 by A34, TARSKI:def 4;

consider x2 being Element of Y2 such that

A37: a1 = x2 /\ x1 by A36;

( x in a1 & a1 c= x2 & a1 c= x1 ) by A35, A37, XBOOLE_1:17;

then ( x in union Y2 & x in x1 ) by A29, TARSKI:def 4;

hence x in (union Y2) /\ x1 by XBOOLE_0:def 4; :: thesis: verum

end;assume A34: x in union Y3 ; :: thesis: x in (union Y2) /\ x1

consider a1 being set such that

A35: x in a1 and

A36: a1 in Y3 by A34, TARSKI:def 4;

consider x2 being Element of Y2 such that

A37: a1 = x2 /\ x1 by A36;

( x in a1 & a1 c= x2 & a1 c= x1 ) by A35, A37, XBOOLE_1:17;

then ( x in union Y2 & x in x1 ) by A29, TARSKI:def 4;

hence x in (union Y2) /\ x1 by XBOOLE_0:def 4; :: thesis: verum

assume x in (union Y2) /\ x1 ; :: thesis: x in union Y3

then A38: ( x in union Y2 & x in x1 ) by XBOOLE_0:def 4;

then consider a being set such that

A39: x in a and

A40: a in Y2 by TARSKI:def 4;

reconsider a = a as Element of Y2 by A40;

A41: x in a /\ x1 by A38, A39, XBOOLE_0:def 4;

a /\ x1 in Y3 ;

hence x in union Y3 by A41, TARSKI:def 4; :: thesis: verum

proof

assume t in union Y3 ; :: thesis: t in Intersect Y

then ( t in union Y2 & t in x1 ) by A33, XBOOLE_0:def 4;

then ( t in meet C0 & t in x1 ) by A26, A22, SETFAM_1:def 9;

then t in (meet C0) /\ x1 by XBOOLE_0:def 4;

hence t in Intersect Y by A23, A16, SETFAM_1:def 9; :: thesis: verum

end;

Y3 c= UniCl B
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: union Y3 c= Intersect Y

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in union Y3 or t in Intersect Y )let t be object ; :: thesis: ( t in Intersect Y implies t in union Y3 )

assume t in Intersect Y ; :: thesis: t in union Y3

then A43: ( t in union Y2 & t in x1 ) by A24, A26, XBOOLE_0:def 4;

then consider t0 being set such that

A44: t in t0 and

A45: t0 in Y2 by TARSKI:def 4;

A46: t in t0 /\ x1 by A43, A44, XBOOLE_0:def 4;

t0 /\ x1 in Y3 by A45;

hence t in union Y3 by A46, TARSKI:def 4; :: thesis: verum

end;assume t in Intersect Y ; :: thesis: t in union Y3

then A43: ( t in union Y2 & t in x1 ) by A24, A26, XBOOLE_0:def 4;

then consider t0 being set such that

A44: t in t0 and

A45: t0 in Y2 by TARSKI:def 4;

A46: t in t0 /\ x1 by A43, A44, XBOOLE_0:def 4;

t0 /\ x1 in Y3 by A45;

hence t in union Y3 by A46, TARSKI:def 4; :: thesis: verum

assume t in union Y3 ; :: thesis: t in Intersect Y

then ( t in union Y2 & t in x1 ) by A33, XBOOLE_0:def 4;

then ( t in meet C0 & t in x1 ) by A26, A22, SETFAM_1:def 9;

then t in (meet C0) /\ x1 by XBOOLE_0:def 4;

hence t in Intersect Y by A23, A16, SETFAM_1:def 9; :: thesis: verum

proof

then
Intersect Y in UniCl (UniCl B)
by A42, CANTOR_1:def 1;
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Y3 or t in UniCl B )

assume t in Y3 ; :: thesis: t in UniCl B

then consider a being Element of Y2 such that

A47: t = a /\ x1 ;

reconsider a2 = a as Element of B by A29, A25;

reconsider x2 = x1 as Element of B by A13, A16;

consider BP being Subset of B such that

A48: a2 /\ x2 = union BP by A1;

reconsider ax = a2 /\ x2 as Subset of X ;

( BP c= B & B c= bool X ) ;

then A49: BP c= bool X ;

thus t in UniCl B by A47, A48, A49, CANTOR_1:def 1; :: thesis: verum

end;assume t in Y3 ; :: thesis: t in UniCl B

then consider a being Element of Y2 such that

A47: t = a /\ x1 ;

reconsider a2 = a as Element of B by A29, A25;

reconsider x2 = x1 as Element of B by A13, A16;

consider BP being Subset of B such that

A48: a2 /\ x2 = union BP by A1;

reconsider ax = a2 /\ x2 as Subset of X ;

( BP c= B & B c= bool X ) ;

then A49: BP c= bool X ;

thus t in UniCl B by A47, A48, A49, CANTOR_1:def 1; :: thesis: verum

hence Intersect Y in UniCl B by YELLOW_9:15; :: thesis: verum

reconsider CY = card Y as Nat by A5;

S

hence x in UniCl B by A4, A6; :: thesis: verum