let I be non empty set ; for J being non-Empty TopSpace-yielding ManySortedSet of I
for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds
ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )
let J be non-Empty TopSpace-yielding ManySortedSet of I; for P being Subset of (product (Carrier J)) st P in FinMeetCl (product_prebasis J) holds
ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )
let P be Subset of (product (Carrier J)); ( P in FinMeetCl (product_prebasis J) implies ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) ) )
assume A1:
P in FinMeetCl (product_prebasis J)
; ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )
consider Y being Subset-Family of (product (Carrier J)) such that
A2:
( Y c= product_prebasis J & Y is finite & P = Intersect Y )
by A1, CANTOR_1:def 3;
per cases
( ( not Y is empty & meet Y <> {} ) or Y is empty or ( not Y is empty & meet Y = {} ) )
;
suppose A3:
( not
Y is
empty &
meet Y <> {} )
;
ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )then A4:
P = meet Y
by A2, SETFAM_1:def 9;
defpred S1[
object ,
object ]
means ex
i being
Element of
I ex
B being
Subset of
(J . i) st
( $2
= i &
B is
open & $1
= product ((Carrier J) +* (i,B)) );
A5:
for
x being
object st
x in Y holds
ex
i being
object st
(
i in I &
S1[
x,
i] )
proof
let x be
object ;
( x in Y implies ex i being object st
( i in I & S1[x,i] ) )
assume
x in Y
;
ex i being object st
( i in I & S1[x,i] )
then consider i being
set ,
T being
TopStruct ,
V being
Subset of
T such that A6:
(
i in I &
V is
open &
T = J . i &
x = product ((Carrier J) +* (i,V)) )
by A2, WAYBEL18:def 2;
take
i
;
( i in I & S1[x,i] )
thus
i in I
by A6;
S1[x,i]
reconsider j =
i as
Element of
I by A6;
reconsider V =
V as
Subset of
(J . j) by A6;
take
j
;
ex B being Subset of (J . j) st
( i = j & B is open & x = product ((Carrier J) +* (j,B)) )
take
V
;
( i = j & V is open & x = product ((Carrier J) +* (j,V)) )
thus
(
i = j &
V is
open &
x = product ((Carrier J) +* (j,V)) )
by A6;
verum
end; consider g being
Function of
Y,
I such that A7:
for
x being
object st
x in Y holds
S1[
x,
g . x]
from FUNCT_2:sch 1(A5);
set X =
{ (meet (g " {i})) where i is Element of I : g " {i} <> {} } ;
{ (meet (g " {i})) where i is Element of I : g " {i} <> {} } c= bool (product (Carrier J))
then reconsider X =
{ (meet (g " {i})) where i is Element of I : g " {i} <> {} } as
Subset-Family of
(product (Carrier J)) ;
take
X
;
ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )defpred S2[
object ,
object ]
means ex
i being
Element of
I st
( $2
= i & $1
= meet (g " {i}) &
g " {i} <> {} );
A9:
for
x being
object st
x in X holds
ex
i being
object st
(
i in I &
S2[
x,
i] )
consider f being
Function of
X,
I such that A11:
for
x being
object st
x in X holds
S2[
x,
f . x]
from FUNCT_2:sch 1(A9);
A12:
(
dom f = X &
rng f c= I )
by FUNCT_2:def 1;
for
x1,
x2 being
object st
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 holds
x1 = x2
then reconsider f =
f as
I -valued one-to-one Function by FUNCT_1:def 4;
take
f
;
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )A16:
for
i being
Element of
I for
S being non
empty set st
g " {i} <> {} &
S in g " {i} holds
ex
V being non
empty open Subset of
(J . i) st
S = product ((Carrier J) +* (i,V))
proof
let i be
Element of
I;
for S being non empty set st g " {i} <> {} & S in g " {i} holds
ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))let S be non
empty set ;
( g " {i} <> {} & S in g " {i} implies ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V)) )
assume a17:
(
g " {i} <> {} &
S in g " {i} )
;
ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))
then A17:
(
S in Y &
g . S in {i} )
by FUNCT_2:38;
then consider j being
set ,
T being
TopStruct ,
V being
Subset of
T such that A18:
(
j in I &
V is
open &
T = J . j )
and A19:
S = product ((Carrier J) +* (j,V))
by A2, WAYBEL18:def 2;
a20:
dom (Carrier J) = I
by PARTFUN1:def 2;
per cases
( V <> (Carrier J) . j or V = (Carrier J) . j )
;
suppose A21:
V <> (Carrier J) . j
;
ex V being non empty open Subset of (J . i) st S = product ((Carrier J) +* (i,V))A22:
not
V is
empty
by A19, a20, Th36, A18;
A23:
i = j
proof
g . S = i
by A17, TARSKI:def 1;
then consider k being
Element of
I,
B being
Subset of
(J . k) such that A24:
(
i = k &
B is
open )
and A25:
S = product ((Carrier J) +* (k,B))
by A7, a17;
not
B is
empty
by a20, A25, Th36;
hence
i = j
by A19, A18, a20, A21, A22, A24, A25, Th42;
verum
end; then reconsider V =
V as non
empty open Subset of
(J . i) by A19, a20, Th36, A18;
take
V
;
S = product ((Carrier J) +* (i,V))thus
S = product ((Carrier J) +* (i,V))
by A19, A23;
verum end; end;
end; A27:
not
X is
empty
A31:
for
x being
Element of
X st
x = meet (g " {(f . x)}) &
g " {(f . x)} <> {} &
x <> {} holds
ex
Z being
Subset-Family of
(J . (In ((f . x),I))) st
(
Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } &
Z is
open &
Z is
finite & not
Z is
empty &
x = product ((Carrier J) +* ((f . x),(meet Z))) )
proof
let x be
Element of
X;
( x = meet (g " {(f . x)}) & g " {(f . x)} <> {} & x <> {} implies ex Z being Subset-Family of (J . (In ((f . x),I))) st
( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) ) )
set i =
In (
(f . x),
I);
a32:
f . x in rng f
by A12, A27, FUNCT_1:3;
then A32:
In (
(f . x),
I)
= f . x
by SUBSET_1:def 8;
assume A33:
(
x = meet (g " {(f . x)}) &
g " {(f . x)} <> {} &
x <> {} )
;
ex Z being Subset-Family of (J . (In ((f . x),I))) st
( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )
set Z =
{ ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } ;
{ ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } c= bool the
carrier of
(J . (In ((f . x),I)))
then reconsider Z =
{ ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } as
Subset-Family of
(J . (In ((f . x),I))) ;
take
Z
;
( Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} } & Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )
thus
Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} }
;
( Z is open & Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )
for
A being
Subset of
(J . (In ((f . x),I))) st
A in Z holds
A is
open
hence
Z is
open
by TOPS_2:def 1;
( Z is finite & not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )
defpred S3[
object ,
object ]
means ex
V being
Subset of
(product (Carrier J)) st
( $1
= V & $2
= (proj (J,(In ((f . x),I)))) .: V );
A37:
for
y,
z1,
z2 being
object st
y in g " {(In ((f . x),I))} &
S3[
y,
z1] &
S3[
y,
z2] holds
z1 = z2
;
A38:
for
y being
object st
y in g " {(In ((f . x),I))} holds
ex
z being
object st
S3[
y,
z]
proof
let y be
object ;
( y in g " {(In ((f . x),I))} implies ex z being object st S3[y,z] )
assume
y in g " {(In ((f . x),I))}
;
ex z being object st S3[y,z]
then
y in Y
;
then reconsider V =
y as
Subset of
(product (Carrier J)) ;
take
(proj (J,(In ((f . x),I)))) .: V
;
S3[y,(proj (J,(In ((f . x),I)))) .: V]
take
V
;
( y = V & (proj (J,(In ((f . x),I)))) .: V = (proj (J,(In ((f . x),I)))) .: V )
thus
(
y = V &
(proj (J,(In ((f . x),I)))) .: V = (proj (J,(In ((f . x),I)))) .: V )
;
verum
end;
consider h being
Function such that A39:
(
dom h = g " {(In ((f . x),I))} & ( for
y being
object st
y in g " {(In ((f . x),I))} holds
S3[
y,
h . y] ) )
from FUNCT_1:sch 2(A37, A38);
a45:
for
y being
object holds
(
y in rng h iff
y in Z )
proof
let y be
object ;
( y in rng h iff y in Z )
hereby ( y in Z implies y in rng h )
end;
assume
y in Z
;
y in rng h
then consider V being
Subset of
(product (Carrier J)) such that A42:
(
y = (proj (J,(In ((f . x),I)))) .: V &
V in g " {(f . x)} )
;
A43:
V in dom h
by a32, SUBSET_1:def 8, A39, A42;
ex
V0 being
Subset of
(product (Carrier J)) st
(
V = V0 &
h . V = (proj (J,(In ((f . x),I)))) .: V0 )
by A32, A39, A42;
hence
y in rng h
by A42, A43, FUNCT_1:def 3;
verum
end;
then
rng h = Z
by TARSKI:2;
hence
Z is
finite
by A2, A39, FINSET_1:8;
( not Z is empty & x = product ((Carrier J) +* ((f . x),(meet Z))) )
h . the
Element of
g " {(f . x)} in rng h
by A32, A33, A39, FUNCT_1:3;
hence A46:
not
Z is
empty
by a45;
x = product ((Carrier J) +* ((f . x),(meet Z)))
a47:
dom (Carrier J) = I
by PARTFUN1:def 2;
then A47:
In (
(f . x),
I)
in dom (Carrier J)
;
for
y being
object holds
(
y in meet (g " {(In ((f . x),I))}) iff
y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) )
proof
let y be
object ;
( y in meet (g " {(In ((f . x),I))}) iff y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) )
hereby ( y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) implies y in meet (g " {(In ((f . x),I))}) )
assume A49:
y in meet (g " {(In ((f . x),I))})
;
y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z)))set S0 = the
Element of
g " {(In ((f . x),I))};
not the
Element of
g " {(In ((f . x),I))} is
empty
by A32, A33, A49, SETFAM_1:def 1;
then consider V0 being non
empty open Subset of
(J . (In ((f . x),I))) such that A50:
the
Element of
g " {(In ((f . x),I))} = product ((Carrier J) +* ((In ((f . x),I)),V0))
by A16, A32, A33;
y in product ((Carrier J) +* ((In ((f . x),I)),V0))
by A32, A33, A49, A50, SETFAM_1:def 1;
then consider f0 being
Function such that A51:
(
y = f0 &
dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),V0)) )
and A52:
for
z being
object st
z in dom ((Carrier J) +* ((In ((f . x),I)),V0)) holds
f0 . z in ((Carrier J) +* ((In ((f . x),I)),V0)) . z
by CARD_3:def 5;
now ex f0 being Function st
( y = f0 & dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds
f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z ) )take f0 =
f0;
( y = f0 & dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds
b2 . b3 in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b3 ) )thus
y = f0
by A51;
( dom f0 = dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) & ( for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds
b2 . b3 in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b3 ) )thus dom f0 =
dom (Carrier J)
by A51, FUNCT_7:30
.=
dom ((Carrier J) +* ((In ((f . x),I)),(meet Z)))
by FUNCT_7:30
;
for z being object st z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) holds
b2 . b3 in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b3let z be
object ;
( z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z))) implies b1 . b2 in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b2 )assume
z in dom ((Carrier J) +* ((In ((f . x),I)),(meet Z)))
;
b1 . b2 in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b2then A53:
z in dom (Carrier J)
by FUNCT_7:30;
per cases
( z <> In ((f . x),I) or z = In ((f . x),I) )
;
suppose A54:
z <> In (
(f . x),
I)
;
b1 . b2 in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b2then A55:
((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z =
(Carrier J) . z
by FUNCT_7:32
.=
((Carrier J) +* ((In ((f . x),I)),V0)) . z
by A54, FUNCT_7:32
;
z in dom ((Carrier J) +* ((In ((f . x),I)),V0))
by A53, FUNCT_7:30;
hence
f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z
by A52, A55;
verum end; suppose A56:
z = In (
(f . x),
I)
;
b1 . b2 in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . b2then A57:
((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z = meet Z
by A53, FUNCT_7:31;
for
S being
set st
S in Z holds
f0 . z in S
proof
let S be
set ;
( S in Z implies f0 . z in S )
assume
S in Z
;
f0 . z in S
then consider S1 being
Subset of
(product (Carrier J)) such that A58:
(
S = (proj (J,(In ((f . x),I)))) .: S1 &
S1 in g " {(f . x)} )
;
not
S1 is
empty
by A32, A49, A58, SETFAM_1:def 1;
then consider V1 being non
empty open Subset of
(J . (In ((f . x),I))) such that A59:
S1 = product ((Carrier J) +* ((In ((f . x),I)),V1))
by A16, A32, A58;
V1 c= the
carrier of
(J . (In ((f . x),I)))
;
then
V1 c= [#] (J . (In ((f . x),I)))
by STRUCT_0:def 3;
then A60:
V1 c= (Carrier J) . (In ((f . x),I))
by PENCIL_3:7;
proj (
J,
(In ((f . x),I)))
= proj (
(Carrier J),
(In ((f . x),I)))
by WAYBEL18:def 4;
then A61:
S = V1
by A58, A59, A60, a47, Th43;
y in S1
by A32, A49, A58, SETFAM_1:def 1;
then consider f1 being
Function such that A62:
(
y = f1 &
dom f1 = dom ((Carrier J) +* ((In ((f . x),I)),V1)) )
and A63:
for
a being
object st
a in dom ((Carrier J) +* ((In ((f . x),I)),V1)) holds
f1 . a in ((Carrier J) +* ((In ((f . x),I)),V1)) . a
by A59, CARD_3:def 5;
In (
(f . x),
I)
in dom ((Carrier J) +* ((In ((f . x),I)),V1))
by A47, FUNCT_7:30;
then
f1 . (In ((f . x),I)) in ((Carrier J) +* ((In ((f . x),I)),V1)) . (In ((f . x),I))
by A63;
hence
f0 . z in S
by A51, A56, A61, A62, a47, FUNCT_7:31;
verum
end; hence
f0 . z in ((Carrier J) +* ((In ((f . x),I)),(meet Z))) . z
by A57, A46, SETFAM_1:def 1;
verum end; end; end; hence
y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z)))
by CARD_3:def 5;
verum
end;
assume A64:
y in product ((Carrier J) +* ((In ((f . x),I)),(meet Z)))
;
y in meet (g " {(In ((f . x),I))})
for
S being
set st
S in g " {(In ((f . x),I))} holds
y in S
proof
let S be
set ;
( S in g " {(In ((f . x),I))} implies y in S )
assume A65:
S in g " {(In ((f . x),I))}
;
y in S
not
S is
empty
by A32, A33, A65, SETFAM_1:4;
then consider V being non
empty open Subset of
(J . (In ((f . x),I))) such that A66:
S = product ((Carrier J) +* ((In ((f . x),I)),V))
by A16, A65;
V c= the
carrier of
(J . (In ((f . x),I)))
;
then
V c= [#] (J . (In ((f . x),I)))
by STRUCT_0:def 3;
then A67:
V c= (Carrier J) . (In ((f . x),I))
by PENCIL_3:7;
proj (
J,
(In ((f . x),I)))
= proj (
(Carrier J),
(In ((f . x),I)))
by WAYBEL18:def 4;
then A68:
(proj (J,(In ((f . x),I)))) .: S = V
by a47, A66, A67, Th43;
S in Y
by A65;
then
V in Z
by A32, A65, A68;
then
product ((Carrier J) +* ((In ((f . x),I)),(meet Z))) c= product ((Carrier J) +* ((In ((f . x),I)),V))
by a47, Th38, SETFAM_1:3;
hence
y in S
by A64, A66;
verum
end;
hence
y in meet (g " {(In ((f . x),I))})
by A32, A33, SETFAM_1:def 1;
verum
end;
hence
x = product ((Carrier J) +* ((f . x),(meet Z)))
by A32, A33, TARSKI:2;
verum
end;
for
x being
object st
x in X holds
x in product_prebasis J
proof
let x be
object ;
( x in X implies x in product_prebasis J )
assume A69:
x in X
;
x in product_prebasis J
per cases
( x <> {} or x = {} )
;
suppose A70:
x <> {}
;
x in product_prebasis J
ex
i being
set ex
T being
TopStruct ex
V being
Subset of
T st
(
i in I &
V is
open &
T = J . i &
x = product ((Carrier J) +* (i,V)) )
proof
consider i being
Element of
I such that A71:
(
f . x = i &
x = meet (g " {i}) &
g " {i} <> {} )
by A11, A69;
consider Z being
Subset-Family of
(J . (In ((f . x),I))) such that
Z = { ((proj (J,(In ((f . x),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . x)} }
and A72:
(
Z is
open &
Z is
finite & not
Z is
empty )
and A73:
x = product ((Carrier J) +* ((f . x),(meet Z)))
by A31, A69, A70, A71;
set W =
meet Z;
take
i
;
ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) )
take
J . (In ((f . x),I))
;
ex V being Subset of (J . (In ((f . x),I))) st
( i in I & V is open & J . (In ((f . x),I)) = J . i & x = product ((Carrier J) +* (i,V)) )
take
meet Z
;
( i in I & meet Z is open & J . (In ((f . x),I)) = J . i & x = product ((Carrier J) +* (i,(meet Z))) )
thus
(
i in I &
meet Z is
open &
J . (In ((f . x),I)) = J . i &
x = product ((Carrier J) +* (i,(meet Z))) )
by A71, A73, A72, TOPS_2:20;
verum
end; hence
x in product_prebasis J
by A69, WAYBEL18:def 2;
verum end; end;
end; hence
X c= product_prebasis J
by TARSKI:def 3;
( X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )
for
x being
object holds
(
x in meet X iff
x in meet Y )
then A81:
meet X = meet Y
by TARSKI:2;
thus
X is
finite
( P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )thus
P = Intersect X
by A4, A27, A81, SETFAM_1:def 9;
( dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )thus
dom f = X
by FUNCT_2:def 1;
P = product ((Carrier J) +* (product_basis_selector (J,f)))set F =
(Carrier J) +* (product_basis_selector (J,f));
for
x being
object holds
(
x in meet X iff
x in product ((Carrier J) +* (product_basis_selector (J,f))) )
proof
let x be
object ;
( x in meet X iff x in product ((Carrier J) +* (product_basis_selector (J,f))) )
A92:
I =
I \/ (rng f)
by XBOOLE_1:12
.=
(dom (Carrier J)) \/ (rng f)
by PARTFUN1:def 2
.=
(dom (Carrier J)) \/ (dom (product_basis_selector (J,f)))
by PARTFUN1:def 2
.=
dom ((Carrier J) +* (product_basis_selector (J,f)))
by FUNCT_4:def 1
;
hereby ( x in product ((Carrier J) +* (product_basis_selector (J,f))) implies x in meet X )
assume A93:
x in meet X
;
x in product ((Carrier J) +* (product_basis_selector (J,f)))consider A0 being
object such that A94:
A0 in X
by A27, XBOOLE_0:def 1;
reconsider A0 =
A0 as
set by TARSKI:1;
consider i0 being
Element of
I such that A95:
(
f . A0 = i0 &
A0 = meet (g " {i0}) &
g " {i0} <> {} )
by A11, A94;
A0 <> {}
by A3, A81, A94, SETFAM_1:4;
then consider Z0 being
Subset-Family of
(J . (In ((f . A0),I))) such that
Z0 = { ((proj (J,(In ((f . A0),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A0)} }
and
(
Z0 is
open &
Z0 is
finite & not
Z0 is
empty )
and A96:
A0 = product ((Carrier J) +* ((f . A0),(meet Z0)))
by A31, A94, A95;
x in A0
by A93, A94, SETFAM_1:def 1;
then consider h being
Function such that A97:
(
x = h &
dom h = dom ((Carrier J) +* ((f . A0),(meet Z0))) )
and A98:
for
y being
object st
y in dom ((Carrier J) +* ((f . A0),(meet Z0))) holds
h . y in ((Carrier J) +* ((f . A0),(meet Z0))) . y
by A96, CARD_3:def 5;
A99:
dom h = I
by A97, PARTFUN1:def 2;
A100:
dom h = dom ((Carrier J) +* (product_basis_selector (J,f)))
by A92, A97, PARTFUN1:def 2;
for
y being
object st
y in dom ((Carrier J) +* (product_basis_selector (J,f))) holds
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y
proof
let y be
object ;
( y in dom ((Carrier J) +* (product_basis_selector (J,f))) implies h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y )
assume
y in dom ((Carrier J) +* (product_basis_selector (J,f)))
;
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y
then reconsider i =
y as
Element of
I by A92;
i in dom h
by A99;
then A101:
i in dom (Carrier J)
by A97, FUNCT_7:30;
per cases
( y in rng f or not y in rng f )
;
suppose A102:
y in rng f
;
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . ythen
y in dom (product_basis_selector (J,f))
by PARTFUN1:def 2;
then
((Carrier J) +* (product_basis_selector (J,f))) . y = (product_basis_selector (J,f)) . i
by FUNCT_4:13;
then A103:
((Carrier J) +* (product_basis_selector (J,f))) . y = (proj (J,i)) .: ((f ") . i)
by A102, Th54;
consider A being
object such that A104:
(
A in X &
f . A = i )
by A102, FUNCT_2:11;
reconsider A =
A as
set by TARSKI:1;
consider j being
Element of
I such that A105:
(
f . A = j &
A = meet (g " {j}) &
g " {j} <> {} )
by A11, A104;
A <> {}
by A3, A81, A104, SETFAM_1:4;
then consider Z being
Subset-Family of
(J . (In ((f . A),I))) such that
Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A)} }
and
(
Z is
open &
Z is
finite & not
Z is
empty )
and A106:
A = product ((Carrier J) +* ((f . A),(meet Z)))
by A31, A104, A105;
reconsider Z =
Z as
Subset-Family of
(J . i) by A104;
a107:
h in A
by A93, A97, A104, SETFAM_1:def 1;
dom ((Carrier J) +* ((f . A),(meet Z))) = I
by PARTFUN1:def 2;
then
h . i in ((Carrier J) +* ((f . A),(meet Z))) . i
by a107, A106, CARD_3:9;
then A108:
h . i in meet Z
by A104, A101, FUNCT_7:31;
ex
z being
object st
(
z in dom (proj (J,i)) &
z in meet (g " {i}) &
(proj (J,i)) . z = h . i )
proof
set z0 = the
Element of
product (Carrier J);
set z = the
Element of
product (Carrier J) +* (
i,
(h . i));
take
the
Element of
product (Carrier J) +* (
i,
(h . i))
;
( the Element of product (Carrier J) +* (i,(h . i)) in dom (proj (J,i)) & the Element of product (Carrier J) +* (i,(h . i)) in meet (g " {i}) & (proj (J,i)) . ( the Element of product (Carrier J) +* (i,(h . i))) = h . i )
meet Z c= the
carrier of
(J . i)
;
then
meet Z c= [#] (J . i)
by STRUCT_0:def 3;
then A109:
meet Z c= (Carrier J) . i
by PENCIL_3:7;
A110:
the
Element of
product (Carrier J) +* (
i,
(h . i))
in product ((Carrier J) +* (i,(meet Z)))
by A101, A108, Th37;
product ((Carrier J) +* (i,(meet Z))) c= product (Carrier J)
by A101, A109, Th39;
then
the
Element of
product (Carrier J) +* (
i,
(h . i))
in product (Carrier J)
by A110;
then A111:
the
Element of
product (Carrier J) +* (
i,
(h . i))
in dom (proj ((Carrier J),i))
by CARD_3:def 16;
hence
( the
Element of
product (Carrier J) +* (
i,
(h . i))
in dom (proj (J,i)) & the
Element of
product (Carrier J) +* (
i,
(h . i))
in meet (g " {i}) )
by A104, A105, A106, A101, A108, Th37, WAYBEL18:def 4;
(proj (J,i)) . ( the Element of product (Carrier J) +* (i,(h . i))) = h . i
A112:
i in dom the
Element of
product (Carrier J)
by A101, CARD_3:9;
thus (proj (J,i)) . ( the Element of product (Carrier J) +* (i,(h . i))) =
(proj ((Carrier J),i)) . ( the Element of product (Carrier J) +* (i,(h . i)))
by WAYBEL18:def 4
.=
( the Element of product (Carrier J) +* (i,(h . i))) . i
by A111, CARD_3:def 16
.=
h . i
by A112, FUNCT_7:31
;
verum
end; then
h . i in (proj (J,i)) .: (meet (g " {i}))
by FUNCT_1:def 6;
hence
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y
by A103, A105, A12, A104, FUNCT_1:34;
verum end; suppose
not
y in rng f
;
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . ythen
not
y in dom (product_basis_selector (J,f))
;
then A114:
((Carrier J) +* (product_basis_selector (J,f))) . y = (Carrier J) . y
by FUNCT_4:11;
reconsider Z0 =
Z0 as
Subset-Family of
(J . i0) by A95;
meet Z0 c= the
carrier of
(J . i0)
;
then
meet Z0 c= [#] (J . i0)
by STRUCT_0:def 3;
then A115:
meet Z0 c= (Carrier J) . i0
by PENCIL_3:7;
i0 in I
;
then
i0 in dom (Carrier J)
by PARTFUN1:def 2;
then A116:
product ((Carrier J) +* (i0,(meet Z0))) c= product (Carrier J)
by A115, Th39;
h in product ((Carrier J) +* (i0,(meet Z0)))
by A95, A97, A98, CARD_3:9;
hence
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y
by A114, A101, A116, CARD_3:9;
verum end; end;
end; hence
x in product ((Carrier J) +* (product_basis_selector (J,f)))
by A97, A100, CARD_3:def 5;
verum
end;
assume
x in product ((Carrier J) +* (product_basis_selector (J,f)))
;
x in meet X
then consider h being
Function such that A117:
(
h = x &
dom h = dom ((Carrier J) +* (product_basis_selector (J,f))) )
and A118:
for
y being
object st
y in dom ((Carrier J) +* (product_basis_selector (J,f))) holds
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y
by CARD_3:def 5;
for
A being
set st
A in X holds
h in A
proof
let A be
set ;
( A in X implies h in A )
assume A119:
A in X
;
h in A
then consider i being
Element of
I such that A120:
(
f . A = i &
A = meet (g " {i}) &
g " {i} <> {} )
by A11;
A121:
(f ") . i = A
by A12, A119, A120, FUNCT_1:34;
A <> {}
by A3, A81, A119, SETFAM_1:4;
then consider Z being
Subset-Family of
(J . (In ((f . A),I))) such that A122:
Z = { ((proj (J,(In ((f . A),I)))) .: V) where V is Subset of (product (Carrier J)) : V in g " {(f . A)} }
and
(
Z is
open &
Z is
finite & not
Z is
empty )
and A124:
A = product ((Carrier J) +* ((f . A),(meet Z)))
by A31, A119, A120;
A125:
dom h = dom ((Carrier J) +* ((f . A),(meet Z)))
by A92, A117, PARTFUN1:def 2;
for
y being
object st
y in dom ((Carrier J) +* ((f . A),(meet Z))) holds
h . y in ((Carrier J) +* ((f . A),(meet Z))) . y
proof
let y be
object ;
( y in dom ((Carrier J) +* ((f . A),(meet Z))) implies h . y in ((Carrier J) +* ((f . A),(meet Z))) . y )
assume A126:
y in dom ((Carrier J) +* ((f . A),(meet Z)))
;
h . y in ((Carrier J) +* ((f . A),(meet Z))) . y
per cases
( y <> i or y = i )
;
suppose
y <> i
;
h . y in ((Carrier J) +* ((f . A),(meet Z))) . ythen A127:
((Carrier J) +* ((f . A),(meet Z))) . y = (Carrier J) . y
by A120, FUNCT_7:32;
A128:
y in dom (Carrier J)
by A126, FUNCT_7:30;
A129:
h . y in ((Carrier J) +* (product_basis_selector (J,f))) . y
by A92, A118, A126;
per cases
( y in rng f or not y in rng f )
;
suppose A130:
y in rng f
;
h . y in ((Carrier J) +* ((f . A),(meet Z))) . ythen reconsider i0 =
y as
Element of
I ;
y in dom (product_basis_selector (J,f))
by A130, PARTFUN1:def 2;
then ((Carrier J) +* (product_basis_selector (J,f))) . y =
(product_basis_selector (J,f)) . i0
by FUNCT_4:13
.=
(proj (J,i0)) .: ((f ") . i0)
by A130, Th54
;
then
((Carrier J) +* (product_basis_selector (J,f))) . y c= rng (proj (J,i0))
by RELAT_1:111;
then
((Carrier J) +* (product_basis_selector (J,f))) . y c= rng (proj ((Carrier J),i0))
by WAYBEL18:def 4;
then
((Carrier J) +* (product_basis_selector (J,f))) . y c= (Carrier J) . i0
by A128, YELLOW17:3;
hence
h . y in ((Carrier J) +* ((f . A),(meet Z))) . y
by A127, A129;
verum end; end; end; suppose A131:
y = i
;
h . y in ((Carrier J) +* ((f . A),(meet Z))) . y
i in I
;
then a132:
i in dom (Carrier J)
by PARTFUN1:def 2;
A133:
i in rng f
by A12, A119, A120, FUNCT_1:def 3;
then
i in dom (product_basis_selector (J,f))
by PARTFUN1:def 2;
then A134:
((Carrier J) +* (product_basis_selector (J,f))) . i =
(product_basis_selector (J,f)) . i
by FUNCT_4:13
.=
(proj (J,i)) .: (meet (g " {i}))
by A120, A121, A133, Th54
;
reconsider G =
g " {i} as
Subset-Family of
(product (Carrier J)) by XBOOLE_1:1;
h . i in (proj (J,i)) .: (meet (g " {i}))
by A92, A118, A134;
then
h . i in meet { ((proj (J,i)) .: B) where B is Subset of (product (Carrier J)) : B in G }
by Th3, TARSKI:def 3;
hence
h . y in ((Carrier J) +* ((f . A),(meet Z))) . y
by A131, a132, FUNCT_7:31, A120, A122;
verum end; end;
end;
hence
h in A
by A124, A125, CARD_3:9;
verum
end;
hence
x in meet X
by A27, A117, SETFAM_1:def 1;
verum
end; hence
P = product ((Carrier J) +* (product_basis_selector (J,f)))
by A4, A81, TARSKI:2;
verum end; suppose A136:
Y is
empty
;
ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )reconsider f = the
empty Function as
I -valued one-to-one Function by XBOOLE_1:2, RELAT_1:38, RELAT_1:def 19;
take
Y
;
ex f being I -valued one-to-one Function st
( Y c= product_prebasis J & Y is finite & P = Intersect Y & dom f = Y & P = product ((Carrier J) +* (product_basis_selector (J,f))) )take
f
;
( Y c= product_prebasis J & Y is finite & P = Intersect Y & dom f = Y & P = product ((Carrier J) +* (product_basis_selector (J,f))) )thus
(
Y c= product_prebasis J &
Y is
finite &
P = Intersect Y )
by A2;
( dom f = Y & P = product ((Carrier J) +* (product_basis_selector (J,f))) )thus
dom f = Y
by A136;
P = product ((Carrier J) +* (product_basis_selector (J,f)))
product_basis_selector (
J,
f) is
empty
;
hence
P = product ((Carrier J) +* (product_basis_selector (J,f)))
by A2, A136, SETFAM_1:def 9;
verum end; suppose
( not
Y is
empty &
meet Y = {} )
;
ex X being Subset-Family of (product (Carrier J)) ex f being I -valued one-to-one Function st
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X & P = product ((Carrier J) +* (product_basis_selector (J,f))) )then A138:
P = {}
by A2, SETFAM_1:def 9;
set i = the
Element of
I;
set V = the
empty Subset of
(J . the Element of I);
a139:
dom (Carrier J) = I
by PARTFUN1:def 2;
then A140:
product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) = {}
by Th36;
then
product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) in product_prebasis J
by Th56;
then reconsider A =
product ((Carrier J) +* ( the Element of I, the empty Subset of (J . the Element of I))) as
Subset of
(product (Carrier J)) ;
set X =
{A};
set f =
A .--> the
Element of
I;
take
{A}
;
ex f being I -valued one-to-one Function st
( {A} c= product_prebasis J & {A} is finite & P = Intersect {A} & dom f = {A} & P = product ((Carrier J) +* (product_basis_selector (J,f))) )take
A .--> the
Element of
I
;
( {A} c= product_prebasis J & {A} is finite & P = Intersect {A} & dom (A .--> the Element of I) = {A} & P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) )thus
(
{A} c= product_prebasis J &
{A} is
finite )
by A140, Th56, ZFMISC_1:31;
( P = Intersect {A} & dom (A .--> the Element of I) = {A} & P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) )
{} in {A}
by A140, TARSKI:def 1;
then
meet {A} = {}
by SETFAM_1:4;
hence
P = Intersect {A}
by A138, SETFAM_1:def 9;
( dom (A .--> the Element of I) = {A} & P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) )thus dom (A .--> the Element of I) =
dom ({A} --> the Element of I)
by FUNCOP_1:def 9
.=
{A}
;
P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I))))set F =
(Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)));
ex
j being
object st
(
j in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) &
((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . j = {} )
proof
take
the
Element of
I
;
( the Element of I in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) & ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = {} )
the
Element of
I in (dom (Carrier J)) \/ (dom (product_basis_selector (J,(A .--> the Element of I))))
by a139, XBOOLE_1:7, TARSKI:def 3;
hence
the
Element of
I in dom ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I))))
by FUNCT_4:def 1;
((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . the Element of I = {}
the
Element of
I in { the Element of I}
by TARSKI:def 1;
then
the
Element of
I in rng ({A} --> the Element of I)
by FUNCOP_1:8;
then A142:
the
Element of
I in rng (A .--> the Element of I)
by FUNCOP_1:def 9;
then
the
Element of
I in dom (product_basis_selector (J,(A .--> the Element of I)))
by PARTFUN1:def 2;
hence ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I)))) . the
Element of
I =
(product_basis_selector (J,(A .--> the Element of I))) . the
Element of
I
by FUNCT_4:13
.=
(proj (J, the Element of I)) .: (((A .--> the Element of I) ") . the Element of I)
by A142, Th54
.=
(proj (J, the Element of I)) .: (( the Element of I .--> A) . the Element of I)
by NECKLACE:9
.=
(proj (J, the Element of I)) .: A
by FUNCOP_1:72
.=
{}
by A140
;
verum
end; then
{} in rng ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I))))
by FUNCT_1:def 3;
hence
P = product ((Carrier J) +* (product_basis_selector (J,(A .--> the Element of I))))
by A138, CARD_3:26;
verum end; end;