let X be set ; for A being Subset-Family of X holds UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)
let A be Subset-Family of X; UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)
per cases
( A = {} or A <> {} )
;
suppose
A <> {}
;
UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)then reconsider A =
A as non
empty Subset-Family of
X ;
A4:
UniCl (FinMeetCl (UniCl A)) c= UniCl (UniCl (FinMeetCl A))
proof
let x be
object ;
TARSKI:def 3 ( not x in UniCl (FinMeetCl (UniCl A)) or x in UniCl (UniCl (FinMeetCl A)) )
assume
x in UniCl (FinMeetCl (UniCl A))
;
x in UniCl (UniCl (FinMeetCl A))
then consider Y being
Subset-Family of
X such that A5:
Y c= FinMeetCl (UniCl A)
and A6:
x = union Y
by CANTOR_1:def 1;
Y c= UniCl (FinMeetCl A)
proof
let y be
object ;
TARSKI:def 3 ( not y in Y or y in UniCl (FinMeetCl A) )
reconsider yy =
y as
set by TARSKI:1;
assume
y in Y
;
y in UniCl (FinMeetCl A)
then consider Z being
Subset-Family of
X such that A7:
Z c= UniCl A
and A8:
Z is
finite
and A9:
y = Intersect Z
by A5, CANTOR_1:def 3;
per cases
( Z = {} or Z <> {} )
;
suppose A11:
Z <> {}
;
y in UniCl (FinMeetCl A)then A12:
y = meet Z
by A9, SETFAM_1:def 9;
set G =
{ (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z } ;
A13:
{ (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z } c= FinMeetCl A
then reconsider G =
{ (meet (rng f)) where f is Element of Funcs (Z,A) : for z being set st z in Z holds
f . z c= z } as
Subset-Family of
X by XBOOLE_1:1;
reconsider G =
G as
Subset-Family of
X ;
union G = yy
proof
let a be
object ;
TARSKI:def 3 ( not a in yy or a in union G )
assume A24:
a in yy
;
a in union G
defpred S1[
object ,
object ]
means ex
A,
B being
set st
(
A = $1 &
B = $2 &
a in B &
B c= A );
A25:
now for z being object st z in Z holds
ex w being object st
( w in A & S1[z,w] )let z be
object ;
( z in Z implies ex w being object st
( w in A & S1[z,w] ) )assume A26:
z in Z
;
ex w being object st
( w in A & S1[z,w] )reconsider zz =
z as
set by TARSKI:1;
A27:
a in zz
by A12, A24, SETFAM_1:def 1, A26;
consider C being
Subset-Family of
X such that A28:
C c= A
and A29:
z = union C
by A7, A26, CANTOR_1:def 1;
consider w being
set such that A30:
a in w
and A31:
w in C
by A27, A29, TARSKI:def 4;
reconsider w =
w as
object ;
take w =
w;
( w in A & S1[z,w] )thus
w in A
by A28, A31;
S1[z,w]thus
S1[
z,
w]
by A29, A30, A31, ZFMISC_1:74;
verum end;
consider f being
Function such that A32:
(
dom f = Z &
rng f c= A )
and A33:
for
z being
object st
z in Z holds
S1[
z,
f . z]
from FUNCT_1:sch 6(A25);
reconsider f =
f as
Element of
Funcs (
Z,
A)
by A32, FUNCT_2:def 2;
for
z being
set st
z in Z holds
f . z c= z
proof
let z be
set ;
( z in Z implies f . z c= z )
assume
z in Z
;
f . z c= z
then
S1[
z,
f . z]
by A33;
hence
f . z c= z
;
verum
end;
then A34:
meet (rng f) in G
;
then
a in meet (rng f)
by SETFAM_1:def 1;
hence
a in union G
by A34, TARSKI:def 4;
verum
end; hence
y in UniCl (FinMeetCl A)
by A13, CANTOR_1:def 1;
verum end; end;
end;
hence
x in UniCl (UniCl (FinMeetCl A))
by A6, CANTOR_1:def 1;
verum
end;
FinMeetCl A c= FinMeetCl (UniCl A)
by CANTOR_1:1, CANTOR_1:14;
then A36:
UniCl (FinMeetCl A) c= UniCl (FinMeetCl (UniCl A))
by CANTOR_1:9;
UniCl (UniCl (FinMeetCl A)) = UniCl (FinMeetCl A)
by Th15;
hence
UniCl (FinMeetCl (UniCl A)) = UniCl (FinMeetCl A)
by A4, A36;
verum end; end;