let n, k be natural number ; 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 ; 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; ( card P = k implies ex H being Subset of X st
( not H is finite & H is_homogeneous_for P ) )
assume A1:
card P = k
; 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
and
A3:
dom F1 = P
and
A4:
rng F1 = k
by WELLORD2:def 4;
reconsider F1 = F1 as Function of P,k by A3, A4, FUNCT_2:3;
set F = F1 * (proj P);
reconsider F = F1 * (proj P) as Function of (the_subsets_of_card n,X),k ;
consider H being Subset of X such that
A5:
not H is finite
and
A6:
F | (the_subsets_of_card n,H) is constant
by A1, Th14;
take
H
; ( not H is finite & H is_homogeneous_for P )
thus
not H is finite
by A5; H is_homogeneous_for P
consider h being Element of the_subsets_of_card n,H;
not the_subsets_of_card n,H is empty
by A5;
then A7:
h in the_subsets_of_card n,H
;
A8:
the_subsets_of_card n,H c= the_subsets_of_card n,X
by Lm1;
then reconsider h = h as Element of the_subsets_of_card n,X by A7;
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 ;
( x in the_subsets_of_card n,H implies x in E )
assume A9:
x in the_subsets_of_card n,
H
;
x in E
then reconsider x9 =
x as
Element of
the_subsets_of_card n,
X by A8;
A10:
dom F = the_subsets_of_card n,
X
by A1, FUNCT_2:def 1;
then
h in (dom F) /\ (the_subsets_of_card n,H)
by A5, XBOOLE_0:def 4;
then A11:
h in dom (F | (the_subsets_of_card n,H))
by RELAT_1:90;
x9 in (dom F) /\ (the_subsets_of_card n,H)
by A9, A10, XBOOLE_0:def 4;
then A12:
x9 in dom (F | (the_subsets_of_card n,H))
by RELAT_1:90;
F . x9 =
(F | (the_subsets_of_card n,H)) . x9
by A9, FUNCT_1:72
.=
(F | (the_subsets_of_card n,H)) . h
by A6, A12, A11, FUNCT_1:def 16
.=
F . h
by A5, FUNCT_1:72
;
then F1 . ((proj P) . x9) =
(F1 * (proj P)) . h
by A10, FUNCT_1:22
.=
F1 . ((proj P) . h)
by A10, FUNCT_1:22
;
then
(
h in E &
(proj P) . h = (proj P) . x9 )
by A2, A3, EQREL_1:def 8, FUNCT_1:def 8;
hence
x in E
by Th13;
verum
end;
then
the_subsets_of_card n,H c= E
by TARSKI:def 3;
hence
H is_homogeneous_for P
by Def1; verum