defpred S1[ object , object ] means ex D2 being set st
( D2 = $2 & $1 in D2 );
let X be set ; :: thesis: for F being Subset-Family of X st F is finite holds
for A being Subset of X st A is infinite & A c= union F holds
ex Y being Subset of X st
( Y in F & Y /\ A is infinite )
let F be Subset-Family of X; :: thesis: ( F is finite implies for A being Subset of X st A is infinite & A c= union F holds
ex Y being Subset of X st
( Y in F & Y /\ A is infinite ) )
assume A1: F is finite ; :: thesis: for A being Subset of X st A is infinite & A c= union F holds
ex Y being Subset of X st
( Y in F & Y /\ A is infinite )
let A be Subset of X; :: thesis: ( A is infinite & A c= union F implies ex Y being Subset of X st
( Y in F & Y /\ A is infinite ) )
assume that
A2: A is infinite and
A3: A c= union F ; :: thesis: ex Y being Subset of X st
( Y in F & Y /\ A is infinite )
set I = INTERSECTION (F,{A});
card [:F,{A}:] = card F by CARD_1:69;
then card (INTERSECTION (F,{A})) c= card F by TOPGEN_4:25;
then A4: INTERSECTION (F,{A}) is finite by A1;
A5: for x being object st x in A holds
ex y being object st
( y in INTERSECTION (F,{A}) & S1[x,y] )
proof
let x be object ; :: thesis: ( x in A implies ex y being object st
( y in INTERSECTION (F,{A}) & S1[x,y] ) )
assume A6: x in A ; :: thesis: ex y being object st
( y in INTERSECTION (F,{A}) & S1[x,y] )
consider y being set such that
A7: x in y and
A8: y in F by A3, A6, TARSKI:def 4;
take y /\ A ; :: thesis: ( y /\ A in INTERSECTION (F,{A}) & S1[x,y /\ A] )
A in {A} by TARSKI:def 1;
hence y /\ A in INTERSECTION (F,{A}) by A8, SETFAM_1:def 5; :: thesis: S1[x,y /\ A]
take y /\ A ; :: thesis: ( y /\ A = y /\ A & x in y /\ A )
thus ( y /\ A = y /\ A & x in y /\ A ) by A6, A7, XBOOLE_0:def 4; :: thesis: verum
end;
consider p being Function of A,(INTERSECTION (F,{A})) such that
A9: for x being object st x in A holds
S1[x,p . x] from FUNCT_2:sch 1(A5);
 consider x being object such that
A10: x in A by A2, XBOOLE_0:def 1;
ex y being object st
( y in INTERSECTION (F,{A}) & S1[x,y] ) by A5, A10;
then dom p = A by FUNCT_2:def 1;
then consider t being object such that
A11: t in rng p and
A12: p " {t} is infinite by A2, A4, CARD_2:101;
consider Y, Z being set such that
A13: Y in F and
A14: Z in {A} and
A15: t = Y /\ Z by A11, SETFAM_1:def 5;
reconsider Y = Y as Subset of X by A13;
take Y ; :: thesis: ( Y in F & Y /\ A is infinite )
A16: Z = A by A14, TARSKI:def 1;
p " {t} c= Y /\ A
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in p " {t} or z in Y /\ A )
assume A17: z in p " {t} ; :: thesis: z in Y /\ A
p . z in {t} by A17, FUNCT_1:def 7;
then A18: p . z = t by TARSKI:def 1;
S1[z,p . z] by A9, A17;
hence z in Y /\ A by A15, A16, A18; :: thesis: verum
end;
hence ( Y in F & Y /\ A is infinite ) by A12, A13; :: thesis: verum