let n, k be natural number ; :: thesis: for X being infinite set
for P being a_partition of the_subsets_of_card n,X st card P = k holds
ex H being Subset of X st
( not H is finite & H is_homogeneous_for P )
let X be infinite set ; :: thesis: for P being a_partition of the_subsets_of_card n,X st card P = k holds
ex H being Subset of X st
( not H is finite & H is_homogeneous_for P )
let P be a_partition of the_subsets_of_card n,X; :: thesis: ( card P = k implies ex H being Subset of X st
( not H is finite & H is_homogeneous_for P ) )
assume Z:
card P = k
; :: thesis: ex H being Subset of X st
( not H is finite & H is_homogeneous_for P )
then
P,k are_equipotent
by CARD_1:def 5;
then consider F1 being Function such that
A2:
( F1 is one-to-one & dom F1 = P & rng F1 = k )
by WELLORD2:def 4;
reconsider F1 = F1 as Function of P,k by A2, FUNCT_2:3;
set F = F1 * (proj P);
reconsider F = F1 * (proj P) as Function of the_subsets_of_card n,X,k ;
A3:
k <> 0
by Z;
consider H being Subset of X such that
A4:
( not H is finite & F | (the_subsets_of_card n,H) is constant )
by A3, Th14;
take
H
; :: thesis: ( not H is finite & H is_homogeneous_for P )
thus
not H is finite
by A4; :: thesis: H is_homogeneous_for P
consider h being Element of the_subsets_of_card n,H;
A5:
the_subsets_of_card n,H c= the_subsets_of_card n,X
by Lm1;
A6:
not the_subsets_of_card n,H is empty
by A4;
then
h in the_subsets_of_card n,H
;
then reconsider h = h as Element of the_subsets_of_card n,X by A5;
set E = EqClass h,P;
reconsider E = EqClass h,P as Element of P by EQREL_1:def 8;
for x being set st x in the_subsets_of_card n,H holds
x in E
proof
let x be
set ;
:: thesis: ( x in the_subsets_of_card n,H implies x in E )
assume A7:
x in the_subsets_of_card n,
H
;
:: thesis: x in E
then reconsider x' =
x as
Element of
the_subsets_of_card n,
X by A5;
A8:
h in E
by EQREL_1:def 8;
k <> {}
by Z;
then A9:
dom F = the_subsets_of_card n,
X
by FUNCT_2:def 1;
x' in (dom F) /\ (the_subsets_of_card n,H)
by A9, A7, XBOOLE_0:def 4;
then A10:
x' in dom (F | (the_subsets_of_card n,H))
by RELAT_1:90;
h in (dom F) /\ (the_subsets_of_card n,H)
by A9, A6, XBOOLE_0:def 4;
then A11:
h in dom (F | (the_subsets_of_card n,H))
by RELAT_1:90;
A12:
F . x' =
(F | (the_subsets_of_card n,H)) . x'
by A7, FUNCT_1:72
.=
(F | (the_subsets_of_card n,H)) . h
by A4, A10, A11, FUNCT_1:def 16
.=
F . h
by A4, FUNCT_1:72
;
F1 . ((proj P) . x') =
(F1 * (proj P)) . h
by A12, A9, FUNCT_1:22
.=
F1 . ((proj P) . h)
by A9, FUNCT_1:22
;
then
(proj P) . h = (proj P) . x'
by A2, FUNCT_1:def 8;
hence
x in E
by A8, Th13;
:: thesis: verum
end;
then
the_subsets_of_card n,H c= E
by TARSKI:def 3;
hence
H is_homogeneous_for P
by Def1; :: thesis: verum