defpred S1[ object , object ] means ex D2 being set st
( D2 = $2 & $1 in D2 );
let X be set ; 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; ( 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
; 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; ( 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
; 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 ;
( x in A implies ex y being object st
( y in INTERSECTION (F,{A}) & S1[x,y] ) )
assume A6:
x in A
;
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
;
( 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;
S1[x,y /\ A]
take
y /\ A
;
( y /\ A = y /\ A & x in y /\ A )
thus
(
y /\ A = y /\ A &
x in y /\ A )
by A6, A7, XBOOLE_0:def 4;
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
; ( Y in F & Y /\ A is infinite )
A16:
Z = A
by A14, TARSKI:def 1;
p " {t} c= Y /\ A
hence
( Y in F & Y /\ A is infinite )
by A12, A13; verum