let X be set ; :: thesis: for P being finite a_partition of X
for S being Subset of X holds
( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
let P be finite a_partition of X; :: thesis: for S being Subset of X holds
( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
let S be Subset of X; :: thesis: ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
per cases ( X = {} or X <> {} ) ;
suppose X = {} ; :: thesis: ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
hence ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P ) ; :: thesis: verum
end;
suppose A2: X <> {} ; :: thesis: ( ( for p being set st p in P holds
p meets S ) iff card (P | S) = card P )
set PS = P | S;
reconsider Pp1 = P as non empty finite set by A2;
hereby :: thesis: ( card (P | S) = card P implies for p being set st p in P holds
p meets S )
assume A3: for p being set st p in P holds
p meets S ; :: thesis: card (P | S) = card P
set p = the Element of P;
the Element of P in Pp1 ;
then the Element of P meets S by A3;
then the Element of P /\ S in P | S ;
then reconsider PSp1 = P | S as non empty finite set ;
defpred S2[ object , object ] means ex D1 being set st
( D1 = $1 & $1 in P & $2 = D1 /\ S );
A4: for x being object st x in P holds
ex y being object st
( y in PSp1 & S2[x,y] )
proof
let x be object ; :: thesis: ( x in P implies ex y being object st
( y in PSp1 & S2[x,y] ) )
assume A5: x in P ; :: thesis: ex y being object st
( y in PSp1 & S2[x,y] )
reconsider xx = x as set by TARSKI:1;
take xx /\ S ; :: thesis: ( xx /\ S in PSp1 & S2[x,xx /\ S] )
xx meets S by A5, A3;
hence ( xx /\ S in PSp1 & S2[x,xx /\ S] ) by A5; :: thesis: verum
end;
consider f being Function of P,PSp1 such that
A6: for x being object st x in P holds
S2[x,f . x] from FUNCT_2:sch 1(A4);
now :: thesis: for x1, x2 being object st x1 in P & x2 in P & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in P & x2 in P & f . x1 = f . x2 implies x1 = x2 )
assume that
A7: x1 in P and
A8: x2 in P and
A9: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider xx1 = x1, xx2 = x2 as set by TARSKI:1;
S2[x1,f . x1] by A7, A6;
then A10: f . x1 = xx1 /\ S ;
S2[x2,f . x2] by A8, A6;
then A11: f . x2 = xx2 /\ S ;
xx1 meets S by A7, A3;
then f . x1 in P | S by A10, A7;
then f . x1 <> {} ;
then consider x being object such that
A12: x in f . x1 by XBOOLE_0:def 1;
( x in xx1 & x in xx2 ) by A12, A9, A10, A11, XBOOLE_0:def 4;
then xx1 meets xx2 by XBOOLE_0:3;
hence x1 = x2 by A7, A8, EQREL_1:def 4; :: thesis: verum
end;
then A13: f is one-to-one by FUNCT_2:19;
rng f = PSp1
proof
thus rng f c= PSp1 :: according to XBOOLE_0:def 10 :: thesis: PSp1 c= rng f
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in PSp1 )
assume y in rng f ; :: thesis: y in PSp1
then consider x being object such that
A14: x in P and
A15: f . x = y by FUNCT_2:11;
reconsider x = x as set by TARSKI:1;
A16: x meets S by A3, A14;
S2[x,f . x] by A14, A6;
then consider D1 being set such that
A17: ( D1 = x & x in P & f . x = D1 /\ S ) ;
thus y in PSp1 by A15, A17, A16; :: thesis: verum
end;
thus PSp1 c= rng f :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in PSp1 or y in rng f )
assume y in PSp1 ; :: thesis: y in rng f
then consider p being Element of P such that
A18: y = p /\ S and
p meets S ;
A19: p in Pp1 ;
S2[p,f . p] by A6, A19;
then f . p = p /\ S ;
hence y in rng f by A18, A19, FUNCT_2:4; :: thesis: verum
end;
end;
then f is onto by FUNCT_2:def 3;
hence card (P | S) = card P by A13, EULER_1:11; :: thesis: verum
end;
assume A20: card (P | S) = card P ; :: thesis: for p being set st p in P holds
p meets S
defpred S2[ object , object ] means ex D2 being set st
( D2 = $2 & $1 in P | S & $2 in Pp1 & $1 = D2 /\ S );
A21: for x being object st x in P | S holds
ex y being object st
( y in Pp1 & S2[x,y] )
proof
let x be object ; :: thesis: ( x in P | S implies ex y being object st
( y in Pp1 & S2[x,y] ) )
assume A22: x in P | S ; :: thesis: ex y being object st
( y in Pp1 & S2[x,y] )
then consider p being Element of P such that
A23: x = p /\ S and
p meets S ;
take p ; :: thesis: ( p in Pp1 & S2[x,p] )
thus ( p in Pp1 & S2[x,p] ) by A22, A23; :: thesis: verum
end;
consider f being Function of (P | S),Pp1 such that
A24: for x being object st x in P | S holds
S2[x,f . x] from FUNCT_2:sch 1(A21);
A25: f is one-to-one
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A26: x1 in dom f and
A27: x2 in dom f and
A28: f . x1 = f . x2 ; :: thesis: x1 = x2
A29: S2[x2,f . x2] by A27, A24;
S2[x1,f . x1] by A26, A24;
then x1 = (f . x1) /\ S ;
hence x1 = x2 by A28, A29; :: thesis: verum
end;
f is onto by A20, A25, FINSEQ_4:63;
then A30: rng f = P by FUNCT_2:def 3;
let p be set ; :: thesis: ( p in P implies p meets S )
assume p in P ; :: thesis: p meets S
then consider ps being object such that
A31: ps in dom f and
A32: p = f . ps by A30, FUNCT_1:def 3;
S2[ps,f . ps] by A31, A24;
then A33: ps = p /\ S by A32;
reconsider ps = ps as set by TARSKI:1;
not ps is empty by A31;
then ex x being object st x in ps ;
hence p meets S by A33; :: thesis: verum
end;
end;