thus
ex G being non empty a_partition of X st
for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
verumproof
set G =
{ (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } ;
{ (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } c= bool X
then reconsider G =
{ (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) where x is Element of X : verum } as
Subset-Family of
X ;
G is
a_partition of
X
proof
X c= union G
hence
union G = X
;
EQREL_1:def 4 for A being Subset of X st A in G holds
( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) )
let A be
Subset of
X;
( A in G implies ( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) ) )
consider T being
object such that A11:
T in F
by XBOOLE_0:def 1;
reconsider T =
T as
a_partition of
X by A11, Def7;
assume A12:
A in G
;
( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) )
then consider x being
Element of
X such that A13:
A = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
;
A14:
for
Y being
set st
Y in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
x in Y
EqClass (
x,
T)
in { (EqClass (x,S)) where S is a_partition of X : S in F }
by A11;
hence
A <> {}
by A13, A14, SETFAM_1:def 1;
for B being Subset of X holds
( not B in G or A = B or A misses B )
consider x being
Element of
X such that A15:
A = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
by A12;
let B be
Subset of
X;
( not B in G or A = B or A misses B )
assume
B in G
;
( A = B or A misses B )
then consider y being
Element of
X such that A16:
B = meet { (EqClass (y,S)) where S is a_partition of X : S in F }
;
thus
(
A = B or
A misses B )
verumproof
A17:
not
{ (EqClass (y,S)) where S is a_partition of X : S in F } is
empty
A19:
not
{ (EqClass (x,S)) where S is a_partition of X : S in F } is
empty
now ( not A meets B or A = B or A misses B )assume
A meets B
;
( A = B or A misses B )then consider c being
object such that A21:
(
c in A &
c in B )
by XBOOLE_0:3;
c in (meet { (EqClass (x,S)) where S is a_partition of X : S in F } ) /\ (meet { (EqClass (y,S)) where S is a_partition of X : S in F } )
by A15, A16, A21, XBOOLE_0:def 4;
then A22:
c in meet ( { (EqClass (x,S)) where S is a_partition of X : S in F } \/ { (EqClass (y,S)) where S is a_partition of X : S in F } )
by A19, A17, SETFAM_1:9;
A25:
for
T being
a_partition of
X st
T in F holds
ex
A being
object st
(
A in EqClass (
x,
T) &
A in EqClass (
y,
T) )
proof
let T be
a_partition of
X;
( T in F implies ex A being object st
( A in EqClass (x,T) & A in EqClass (y,T) ) )
assume A26:
T in F
;
ex A being object st
( A in EqClass (x,T) & A in EqClass (y,T) )
take
c
;
( c in EqClass (x,T) & c in EqClass (y,T) )
thus
(
c in EqClass (
x,
T) &
c in EqClass (
y,
T) )
by A24, A23, A26;
verum
end; A27:
for
T being
a_partition of
X st
T in F holds
EqClass (
x,
T)
meets EqClass (
y,
T)
A28:
{ (EqClass (y,S)) where S is a_partition of X : S in F } c= { (EqClass (x,S)) where S is a_partition of X : S in F }
proof
let A be
object ;
TARSKI:def 3 ( not A in { (EqClass (y,S)) where S is a_partition of X : S in F } or A in { (EqClass (x,S)) where S is a_partition of X : S in F } )
assume
A in { (EqClass (y,S)) where S is a_partition of X : S in F }
;
A in { (EqClass (x,S)) where S is a_partition of X : S in F }
then consider T being
a_partition of
X such that A29:
T in F
and A30:
A = EqClass (
y,
T)
by Lm3;
A = EqClass (
x,
T)
by A27, A29, A30, Th41;
hence
A in { (EqClass (x,S)) where S is a_partition of X : S in F }
by A29;
verum
end;
{ (EqClass (x,S)) where S is a_partition of X : S in F } c= { (EqClass (y,S)) where S is a_partition of X : S in F }
proof
let A be
object ;
TARSKI:def 3 ( not A in { (EqClass (x,S)) where S is a_partition of X : S in F } or A in { (EqClass (y,S)) where S is a_partition of X : S in F } )
assume
A in { (EqClass (x,S)) where S is a_partition of X : S in F }
;
A in { (EqClass (y,S)) where S is a_partition of X : S in F }
then consider T being
a_partition of
X such that A31:
T in F
and A32:
A = EqClass (
x,
T)
by Lm3;
A = EqClass (
y,
T)
by A27, A31, A32, Th41;
hence
A in { (EqClass (y,S)) where S is a_partition of X : S in F }
by A31;
verum
end; hence
(
A = B or
A misses B )
by A15, A16, A28, XBOOLE_0:def 10;
verum end;
hence
(
A = B or
A misses B )
;
verum
end;
end;
then reconsider G =
G as non
empty a_partition of
X ;
take
G
;
for x being Element of X holds EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }
for
x being
Element of
X holds
EqClass (
x,
G)
= meet { (EqClass (x,S)) where S is a_partition of X : S in F }
hence
for
x being
Element of
X holds
EqClass (
x,
G)
= meet { (EqClass (x,S)) where S is a_partition of X : S in F }
;
verum
end;