let n, k be Nat; :: 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

( H is infinite & 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

( H is infinite & 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

( H is infinite & H is_homogeneous_for P ) )

assume A1: card P = k ; :: thesis: ex H being Subset of X st

( H is infinite & H is_homogeneous_for P )

then P,k are_equipotent by CARD_1:def 2;

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:1;

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: H is infinite and

A6: F | (the_subsets_of_card (n,H)) is constant by A1, Th14;

take H ; :: thesis: ( H is infinite & H is_homogeneous_for P )

thus H is infinite by A5; :: thesis: H is_homogeneous_for P

set h = the Element of the_subsets_of_card (n,H);

not the_subsets_of_card (n,H) is empty by A5;

then A7: the Element of the_subsets_of_card (n,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 = the Element of the_subsets_of_card (n,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 6;

for x being object st x in the_subsets_of_card (n,H) holds

x in E

hence H is_homogeneous_for P ; :: thesis: verum

for P being a_partition of the_subsets_of_card (n,X) st card P = k holds

ex H being Subset of X st

( H is infinite & 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

( H is infinite & 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

( H is infinite & H is_homogeneous_for P ) )

assume A1: card P = k ; :: thesis: ex H being Subset of X st

( H is infinite & H is_homogeneous_for P )

then P,k are_equipotent by CARD_1:def 2;

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:1;

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: H is infinite and

A6: F | (the_subsets_of_card (n,H)) is constant by A1, Th14;

take H ; :: thesis: ( H is infinite & H is_homogeneous_for P )

thus H is infinite by A5; :: thesis: H is_homogeneous_for P

set h = the Element of the_subsets_of_card (n,H);

not the_subsets_of_card (n,H) is empty by A5;

then A7: the Element of the_subsets_of_card (n,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 = the Element of the_subsets_of_card (n,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 6;

for x being object st x in the_subsets_of_card (n,H) holds

x in E

proof

then
the_subsets_of_card (n,H) c= E
;
let x be object ; :: thesis: ( x in the_subsets_of_card (n,H) implies x in E )

assume A9: x in the_subsets_of_card (n,H) ; :: thesis: 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:61;

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:61;

F . x9 = (F | (the_subsets_of_card (n,H))) . x9 by A9, FUNCT_1:49

.= (F | (the_subsets_of_card (n,H))) . h by A6, A12, A11, FUNCT_1:def 10

.= F . h by A5, FUNCT_1:49 ;

then F1 . ((proj P) . x9) = (F1 * (proj P)) . h by A10, FUNCT_1:12

.= F1 . ((proj P) . h) by A10, FUNCT_1:12 ;

then ( h in E & (proj P) . h = (proj P) . x9 ) by A2, A3, EQREL_1:def 6, FUNCT_1:def 4;

hence x in E by Th13; :: thesis: verum

end;assume A9: x in the_subsets_of_card (n,H) ; :: thesis: 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:61;

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:61;

F . x9 = (F | (the_subsets_of_card (n,H))) . x9 by A9, FUNCT_1:49

.= (F | (the_subsets_of_card (n,H))) . h by A6, A12, A11, FUNCT_1:def 10

.= F . h by A5, FUNCT_1:49 ;

then F1 . ((proj P) . x9) = (F1 * (proj P)) . h by A10, FUNCT_1:12

.= F1 . ((proj P) . h) by A10, FUNCT_1:12 ;

then ( h in E & (proj P) . h = (proj P) . x9 ) by A2, A3, EQREL_1:def 6, FUNCT_1:def 4;

hence x in E by Th13; :: thesis: verum

hence H is_homogeneous_for P ; :: thesis: verum