let X be non empty set ; ex f being Function of (BoolePoset X),(product (X --> (BoolePoset {0}))) st
( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
set XB = X --> (BoolePoset {0});
deffunc H1( set ) -> Element of K19(K20(X,{0,1})) = chi ($1,X);
consider f being Function such that
A1:
dom f = bool X
and
A2:
for Y being set st Y in bool X holds
f . Y = H1(Y)
from FUNCT_1:sch 5();
LattPOSet (BooleLatt {0}) = RelStr(# the carrier of (BooleLatt {0}),(LattRel (BooleLatt {0})) #)
by LATTICE3:def 2;
then A3: the carrier of (BoolePoset {0}) =
the carrier of (BooleLatt {0})
by YELLOW_1:def 2
.=
bool {{}}
by LATTICE3:def 1
.=
{0,1}
by CARD_1:49, ZFMISC_1:24
;
A4:
rng f c= product (Carrier (X --> (BoolePoset {0})))
LattPOSet (BooleLatt X) = RelStr(# the carrier of (BooleLatt X),(LattRel (BooleLatt X)) #)
by LATTICE3:def 2;
then A10: the carrier of (BoolePoset X) =
the carrier of (BooleLatt X)
by YELLOW_1:def 2
.=
bool X
by LATTICE3:def 1
;
A11:
the carrier of (product (X --> (BoolePoset {0}))) = product (Carrier (X --> (BoolePoset {0})))
by YELLOW_1:def 4;
then reconsider f = f as Function of (BoolePoset X),(product (X --> (BoolePoset {0}))) by A10, A1, A4, FUNCT_2:def 1, RELSET_1:4;
A12:
for A, B being Element of (BoolePoset X) holds
( A <= B iff f . A <= f . B )
proof
let A,
B be
Element of
(BoolePoset X);
( A <= B iff f . A <= f . B )
A13:
(
f . A = chi (
A,
X) &
f . B = chi (
B,
X) )
by A10, A2;
hereby ( f . A <= f . B implies A <= B )
assume
A <= B
;
f . A <= f . Bthen A14:
A c= B
by YELLOW_1:2;
for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (X --> (BoolePoset {0})) . i &
xi = (chi (A,X)) . i &
yi = (chi (B,X)) . i &
xi <= yi )
proof
let i be
object ;
( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi ) )
assume A15:
i in X
;
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
take R =
BoolePoset {0};
ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )
per cases
( i in A or not i in A )
;
suppose A16:
i in A
;
ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )reconsider xi = 1,
yi = 1 as
Element of
R by A3, TARSKI:def 2;
take
xi
;
ex yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )take
yi
;
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )thus
R = (X --> (BoolePoset {0})) . i
by A15, FUNCOP_1:7;
( xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )thus
xi = (chi (A,X)) . i
by A15, A16, FUNCT_3:def 3;
( yi = (chi (B,X)) . i & xi <= yi )thus
yi = (chi (B,X)) . i
by A14, A15, A16, FUNCT_3:def 3;
xi <= yithus
xi <= yi
;
verum end; suppose A17:
not
i in A
;
ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )thus
ex
xi,
yi being
Element of
R st
(
R = (X --> (BoolePoset {0})) . i &
xi = (chi (A,X)) . i &
yi = (chi (B,X)) . i &
xi <= yi )
verumproof
per cases
( i in B or not i in B )
;
suppose A18:
i in B
;
ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )reconsider xi =
0 ,
yi = 1 as
Element of
R by A3, TARSKI:def 2;
take
xi
;
ex yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )take
yi
;
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )thus
R = (X --> (BoolePoset {0})) . i
by A15, FUNCOP_1:7;
( xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )thus
xi = (chi (A,X)) . i
by A15, A17, FUNCT_3:def 3;
( yi = (chi (B,X)) . i & xi <= yi )thus
yi = (chi (B,X)) . i
by A15, A18, FUNCT_3:def 3;
xi <= yi
xi c= yi
;
hence
xi <= yi
by YELLOW_1:2;
verum end; suppose A19:
not
i in B
;
ex xi, yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )reconsider xi =
0 ,
yi =
0 as
Element of
R by A3, TARSKI:def 2;
take
xi
;
ex yi being Element of R st
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )take
yi
;
( R = (X --> (BoolePoset {0})) . i & xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )thus
R = (X --> (BoolePoset {0})) . i
by A15, FUNCOP_1:7;
( xi = (chi (A,X)) . i & yi = (chi (B,X)) . i & xi <= yi )thus
xi = (chi (A,X)) . i
by A15, A17, FUNCT_3:def 3;
( yi = (chi (B,X)) . i & xi <= yi )thus
yi = (chi (B,X)) . i
by A15, A19, FUNCT_3:def 3;
xi <= yithus
xi <= yi
;
verum end; end;
end; end; end;
end; hence
f . A <= f . B
by A11, A13, YELLOW_1:def 4;
verum
end;
assume
f . A <= f . B
;
A <= B
then consider h1,
h2 being
Function such that A20:
h1 = f . A
and A21:
h2 = f . B
and A22:
for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (X --> (BoolePoset {0})) . i &
xi = h1 . i &
yi = h2 . i &
xi <= yi )
by A11, YELLOW_1:def 4;
A c= B
proof
let i be
object ;
TARSKI:def 3 ( not i in A or i in B )
assume A23:
i in A
;
i in B
then consider R being
RelStr ,
xi,
yi being
Element of
R such that A24:
R = (X --> (BoolePoset {0})) . i
and A25:
xi = h1 . i
and A26:
yi = h2 . i
and A27:
xi <= yi
by A10, A22;
reconsider a =
xi,
b =
yi as
Element of
(BoolePoset {0}) by A10, A23, A24, FUNCOP_1:7;
A28:
a <= b
by A10, A23, A24, A27, FUNCOP_1:7;
A29:
xi =
(chi (A,X)) . i
by A10, A2, A20, A25
.=
1
by A10, A23, FUNCT_3:def 3
;
A30:
yi <> 0
A31:
R = BoolePoset {0}
by A10, A23, A24, FUNCOP_1:7;
(chi (B,X)) . i =
h2 . i
by A10, A2, A21
.=
1
by A3, A26, A31, A30, TARSKI:def 2
;
hence
i in B
by FUNCT_3:36;
verum
end;
hence
A <= B
by YELLOW_1:2;
verum
end;
product (Carrier (X --> (BoolePoset {0}))) c= rng f
proof
let z be
object ;
TARSKI:def 3 ( not z in product (Carrier (X --> (BoolePoset {0}))) or z in rng f )
assume
z in product (Carrier (X --> (BoolePoset {0})))
;
z in rng f
then consider g being
Function such that A32:
z = g
and A33:
dom g = dom (Carrier (X --> (BoolePoset {0})))
and A34:
for
y being
object st
y in dom (Carrier (X --> (BoolePoset {0}))) holds
g . y in (Carrier (X --> (BoolePoset {0}))) . y
by CARD_3:def 5;
set A =
g " {1};
A35:
g " {1} c= X
A36:
dom (chi ((g " {1}),X)) =
X
by FUNCT_3:def 3
.=
dom g
by A33, PARTFUN1:def 2
;
for
a being
object st
a in dom (chi ((g " {1}),X)) holds
(chi ((g " {1}),X)) . a = g . a
then z =
chi (
(g " {1}),
X)
by A32, A36, FUNCT_1:2
.=
f . (g " {1})
by A2, A35
;
hence
z in rng f
by A1, A35, FUNCT_1:def 3;
verum
end;
then A41:
rng f = the carrier of (product (X --> (BoolePoset {0})))
by A11;
take
f
; ( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )
for A, B being Element of (BoolePoset X) st f . A = f . B holds
A = B
then
f is one-to-one
;
hence
f is isomorphic
by A41, A12, WAYBEL_0:66; for Y being Subset of X holds f . Y = chi (Y,X)
thus
for Y being Subset of X holds f . Y = chi (Y,X)
by A2; verum