let G be Group; :: thesis: for a being Element of G holds { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G

let a be Element of G; :: thesis: { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G

reconsider X = { ((a -con_map) " {x}) where x is Element of con_class a : verum } as set ;

A1: for y being object st y in union X holds

y in the carrier of G

y in union X

A9: for A being Subset of G st A in X holds

( A <> {} & ( for B being Subset of G holds

( not B in X or A = B or A misses B ) ) )

hence { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G by A8, A9, EQREL_1:def 4; :: thesis: verum

let a be Element of G; :: thesis: { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G

reconsider X = { ((a -con_map) " {x}) where x is Element of con_class a : verum } as set ;

A1: for y being object st y in union X holds

y in the carrier of G

proof

for y being object st y in the carrier of G holds
let x be object ; :: thesis: ( x in union X implies x in the carrier of G )

assume x in union X ; :: thesis: x in the carrier of G

then consider Y being set such that

A2: x in Y and

A3: Y in X by TARSKI:def 4;

ex z being Element of con_class a st (a -con_map) " {z} = Y by A3;

hence x in the carrier of G by A2; :: thesis: verum

end;assume x in union X ; :: thesis: x in the carrier of G

then consider Y being set such that

A2: x in Y and

A3: Y in X by TARSKI:def 4;

ex z being Element of con_class a st (a -con_map) " {z} = Y by A3;

hence x in the carrier of G by A2; :: thesis: verum

y in union X

proof

then A8:
union X = the carrier of G
by A1, TARSKI:2;
let x be object ; :: thesis: ( x in the carrier of G implies x in union X )

assume x in the carrier of G ; :: thesis: x in union X

then reconsider y = x as Element of G ;

consider z being Element of G such that

A4: z in con_class a and

A5: z = a |^ y by GROUP_3:82;

(a -con_map) . y = z by A5, Def2;

then A6: (a -con_map) . y in {z} by TARSKI:def 1;

dom (a -con_map) = the carrier of G by FUNCT_2:def 1;

then A7: y in (a -con_map) " {z} by A6, FUNCT_1:def 7;

(a -con_map) " {z} in X by A4;

hence x in union X by A7, TARSKI:def 4; :: thesis: verum

end;assume x in the carrier of G ; :: thesis: x in union X

then reconsider y = x as Element of G ;

consider z being Element of G such that

A4: z in con_class a and

A5: z = a |^ y by GROUP_3:82;

(a -con_map) . y = z by A5, Def2;

then A6: (a -con_map) . y in {z} by TARSKI:def 1;

dom (a -con_map) = the carrier of G by FUNCT_2:def 1;

then A7: y in (a -con_map) " {z} by A6, FUNCT_1:def 7;

(a -con_map) " {z} in X by A4;

hence x in union X by A7, TARSKI:def 4; :: thesis: verum

A9: for A being Subset of G st A in X holds

( A <> {} & ( for B being Subset of G holds

( not B in X or A = B or A misses B ) ) )

proof

X c= bool (union X)
by ZFMISC_1:82;
let A be Subset of G; :: thesis: ( A in X implies ( A <> {} & ( for B being Subset of G holds

( not B in X or A = B or A misses B ) ) ) )

assume A in X ; :: thesis: ( A <> {} & ( for B being Subset of G holds

( not B in X or A = B or A misses B ) ) )

then consider x being Element of con_class a such that

A10: A = (a -con_map) " {x} ;

a,x are_conjugated by GROUP_3:81;

then consider g being Element of G such that

A11: x = a |^ g by GROUP_3:74;

(a -con_map) . g = x by A11, Def2;

then A12: (a -con_map) . g in {x} by TARSKI:def 1;

A13: dom (a -con_map) = the carrier of G by FUNCT_2:def 1;

for B being Subset of G holds

( not B in X or A = B or A misses B )

( not B in X or A = B or A misses B ) ) ) by A10, A12, A13, FUNCT_1:def 7; :: thesis: verum

end;( not B in X or A = B or A misses B ) ) ) )

assume A in X ; :: thesis: ( A <> {} & ( for B being Subset of G holds

( not B in X or A = B or A misses B ) ) )

then consider x being Element of con_class a such that

A10: A = (a -con_map) " {x} ;

a,x are_conjugated by GROUP_3:81;

then consider g being Element of G such that

A11: x = a |^ g by GROUP_3:74;

(a -con_map) . g = x by A11, Def2;

then A12: (a -con_map) . g in {x} by TARSKI:def 1;

A13: dom (a -con_map) = the carrier of G by FUNCT_2:def 1;

for B being Subset of G holds

( not B in X or A = B or A misses B )

proof

hence
( A <> {} & ( for B being Subset of G holds
let B be Subset of G; :: thesis: ( not B in X or A = B or A misses B )

assume B in X ; :: thesis: ( A = B or A misses B )

then ex y being Element of con_class a st B = (a -con_map) " {y} ;

hence ( A = B or A misses B ) by A10, Th10; :: thesis: verum

end;assume B in X ; :: thesis: ( A = B or A misses B )

then ex y being Element of con_class a st B = (a -con_map) " {y} ;

hence ( A = B or A misses B ) by A10, Th10; :: thesis: verum

( not B in X or A = B or A misses B ) ) ) by A10, A12, A13, FUNCT_1:def 7; :: thesis: verum

hence { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G by A8, A9, EQREL_1:def 4; :: thesis: verum