let X be set ; :: thesis: for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR

let P be a_partition of X; :: thesis: ex EqR being Equivalence_Relation of X st P = Class EqR

A1: ( X <> {} implies ex EqR being Equivalence_Relation of X st P = Class EqR )

let P be a_partition of X; :: thesis: ex EqR being Equivalence_Relation of X st P = Class EqR

A1: ( X <> {} implies ex EqR being Equivalence_Relation of X st P = Class EqR )

proof

( X = {} implies ex EqR being Equivalence_Relation of X st P = Class EqR )
defpred S_{1}[ object , object ] means ex A being Subset of X st

( A in P & $1 in A & $2 in A );

assume X <> {} ; :: thesis: ex EqR being Equivalence_Relation of X st P = Class EqR

A2: for x, y, z being object st S_{1}[x,y] & S_{1}[y,z] holds

S_{1}[x,z]

A8: for x being object st x in X holds

S_{1}[x,x]
_{1}[x,y] holds

S_{1}[y,x]
;

consider R being Equivalence_Relation of X such that

A12: for x, y being object holds

( [x,y] in R iff ( x in X & y in X & S_{1}[x,y] ) )
from EQREL_1:sch 1(A8, A11, A2);

take R ; :: thesis: P = Class R

end;( A in P & $1 in A & $2 in A );

assume X <> {} ; :: thesis: ex EqR being Equivalence_Relation of X st P = Class EqR

A2: for x, y, z being object st S

S

proof

A7:
union P = X
by Def4;
let x, y, z be object ; :: thesis: ( S_{1}[x,y] & S_{1}[y,z] implies S_{1}[x,z] )

given A being Subset of X such that A3: A in P and

A4: ( x in A & y in A ) ; :: thesis: ( not S_{1}[y,z] or S_{1}[x,z] )

given B being Subset of X such that A5: B in P and

A6: ( y in B & z in B ) ; :: thesis: S_{1}[x,z]

( A = B or A misses B ) by A3, A5, Def4;

hence S_{1}[x,z]
by A3, A4, A6, XBOOLE_0:3; :: thesis: verum

end;given A being Subset of X such that A3: A in P and

A4: ( x in A & y in A ) ; :: thesis: ( not S

given B being Subset of X such that A5: B in P and

A6: ( y in B & z in B ) ; :: thesis: S

( A = B or A misses B ) by A3, A5, Def4;

hence S

A8: for x being object st x in X holds

S

proof

A11:
for x, y being object st S
let x be object ; :: thesis: ( x in X implies S_{1}[x,x] )

assume x in X ; :: thesis: S_{1}[x,x]

then consider Z being set such that

A9: x in Z and

A10: Z in P by A7, TARSKI:def 4;

reconsider A = Z as Subset of X by A10;

take A ; :: thesis: ( A in P & x in A & x in A )

thus ( A in P & x in A & x in A ) by A9, A10; :: thesis: verum

end;assume x in X ; :: thesis: S

then consider Z being set such that

A9: x in Z and

A10: Z in P by A7, TARSKI:def 4;

reconsider A = Z as Subset of X by A10;

take A ; :: thesis: ( A in P & x in A & x in A )

thus ( A in P & x in A & x in A ) by A9, A10; :: thesis: verum

S

consider R being Equivalence_Relation of X such that

A12: for x, y being object holds

( [x,y] in R iff ( x in X & y in X & S

take R ; :: thesis: P = Class R

now :: thesis: for A being Subset of X holds

( A in P iff A in Class R )

hence
P = Class R
by SETFAM_1:31; :: thesis: verum( A in P iff A in Class R )

let A be Subset of X; :: thesis: ( A in P iff A in Class R )

end;A13: now :: thesis: ( A in P implies A in Class R )

set x = the Element of A;

assume A14: A in P ; :: thesis: A in Class R

then A15: A <> {} by Def4;

then A16: the Element of A in X by TARSKI:def 3;

hence A in Class R by A16, Def3; :: thesis: verum

end;assume A14: A in P ; :: thesis: A in Class R

then A15: A <> {} by Def4;

then A16: the Element of A in X by TARSKI:def 3;

now :: thesis: for y being object holds

( y in A iff y in Class (R, the Element of A) )

then
A = Class (R, the Element of A)
by TARSKI:2;( y in A iff y in Class (R, the Element of A) )

let y be object ; :: thesis: ( y in A iff y in Class (R, the Element of A) )

end;A17: now :: thesis: ( y in Class (R, the Element of A) implies y in A )

assume
y in Class (R, the Element of A)
; :: thesis: y in A

then [y, the Element of A] in R by Th19;

then consider B being Subset of X such that

A18: ( B in P & y in B ) and

A19: the Element of A in B by A12;

A meets B by A15, A19, XBOOLE_0:3;

hence y in A by A14, A18, Def4; :: thesis: verum

end;then [y, the Element of A] in R by Th19;

then consider B being Subset of X such that

A18: ( B in P & y in B ) and

A19: the Element of A in B by A12;

A meets B by A15, A19, XBOOLE_0:3;

hence y in A by A14, A18, Def4; :: thesis: verum

now :: thesis: ( y in A implies y in Class (R, the Element of A) )

hence
( y in A iff y in Class (R, the Element of A) )
by A17; :: thesis: verumassume
y in A
; :: thesis: y in Class (R, the Element of A)

then [y, the Element of A] in R by A12, A14, A16;

hence y in Class (R, the Element of A) by Th19; :: thesis: verum

end;then [y, the Element of A] in R by A12, A14, A16;

hence y in Class (R, the Element of A) by Th19; :: thesis: verum

hence A in Class R by A16, Def3; :: thesis: verum

now :: thesis: ( A in Class R implies A in P )

hence
( A in P iff A in Class R )
by A13; :: thesis: verumassume
A in Class R
; :: thesis: A in P

then consider x being object such that

A20: x in X and

A21: A = Class (R,x) by Def3;

x in Class (R,x) by A20, Th20;

then [x,x] in R by Th19;

then consider B being Subset of X such that

A22: B in P and

A23: x in B and

x in B by A12;

end;then consider x being object such that

A20: x in X and

A21: A = Class (R,x) by Def3;

x in Class (R,x) by A20, Th20;

then [x,x] in R by Th19;

then consider B being Subset of X such that

A22: B in P and

A23: x in B and

x in B by A12;

now :: thesis: for y being object holds

( y in A iff y in B )

hence
A in P
by A22, TARSKI:2; :: thesis: verum( y in A iff y in B )

let y be object ; :: thesis: ( y in A iff y in B )

end;A24: now :: thesis: ( y in A implies y in B )

assume
y in A
; :: thesis: y in B

then [y,x] in R by A21, Th19;

then consider C being Subset of X such that

A25: ( C in P & y in C ) and

A26: x in C by A12;

B meets C by A23, A26, XBOOLE_0:3;

hence y in B by A22, A25, Def4; :: thesis: verum

end;then [y,x] in R by A21, Th19;

then consider C being Subset of X such that

A25: ( C in P & y in C ) and

A26: x in C by A12;

B meets C by A23, A26, XBOOLE_0:3;

hence y in B by A22, A25, Def4; :: thesis: verum

now :: thesis: ( y in B implies y in A )

hence
( y in A iff y in B )
by A24; :: thesis: verumassume
y in B
; :: thesis: y in A

then [y,x] in R by A12, A22, A23;

hence y in A by A21, Th19; :: thesis: verum

end;then [y,x] in R by A12, A22, A23;

hence y in A by A21, Th19; :: thesis: verum

proof

hence
ex EqR being Equivalence_Relation of X st P = Class EqR
by A1; :: thesis: verum
set EqR1 = the Equivalence_Relation of X;

assume A27: X = {} ; :: thesis: ex EqR being Equivalence_Relation of X st P = Class EqR

take the Equivalence_Relation of X ; :: thesis: P = Class the Equivalence_Relation of X

P = {} by A27;

hence P = Class the Equivalence_Relation of X by A27, Th31; :: thesis: verum

end;assume A27: X = {} ; :: thesis: ex EqR being Equivalence_Relation of X st P = Class EqR

take the Equivalence_Relation of X ; :: thesis: P = Class the Equivalence_Relation of X

P = {} by A27;

hence P = Class the Equivalence_Relation of X by A27, Th31; :: thesis: verum