let X be non empty set ; :: thesis: for Y being set st Y c= X holds
for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
let Y be set ; :: thesis: ( Y c= X implies for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y )
assume A1: Y c= X ; :: thesis: for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
let P be a_partition of X; :: thesis: { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
set Q = { (a /\ Y) where a is Element of P : a meets Y } ;
{ (a /\ Y) where a is Element of P : a meets Y } c= bool Y
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a /\ Y) where a is Element of P : a meets Y } or x in bool Y )
assume x in { (a /\ Y) where a is Element of P : a meets Y } ; :: thesis: x in bool Y
then consider p being Element of P such that
A2: ( x = p /\ Y & p meets Y ) ;
( x c= X /\ Y & X /\ Y = Y ) by A1, A2, XBOOLE_1:26, XBOOLE_1:28;
hence x in bool Y ; :: thesis: verum
end;
then reconsider Q = { (a /\ Y) where a is Element of P : a meets Y } as Subset-Family of Y ;
Q is a_partition of Y
proof
thus union Q c= Y ; :: according to XBOOLE_0:def 10,EQREL_1:def 6 :: thesis: ( Y c= union Q & ( for b1 being Element of bool Y holds
( not b1 in Q or ( not b1 = {} & ( for b2 being Element of bool Y holds
( not b2 in Q or b1 = b2 or b1 misses b2 ) ) ) ) ) )
thus Y c= union Q :: thesis: for b1 being Element of bool Y holds
( not b1 in Q or ( not b1 = {} & ( for b2 being Element of bool Y holds
( not b2 in Q or b1 = b2 or b1 misses b2 ) ) ) )
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in union Q )
assume A3: x in Y ; :: thesis: x in union Q
then ( x in X & X = union P ) by A1, EQREL_1:def 6;
then consider p being set such that
A4: ( x in p & p in P ) by TARSKI:def 4;
p meets Y by A3, A4, XBOOLE_0:3;
then ( x in p /\ Y & p /\ Y in Q ) by A3, A4, XBOOLE_0:def 4;
hence x in union Q by TARSKI:def 4; :: thesis: verum
end;
let A be Subset of Y; :: thesis: ( not A in Q or ( not A = {} & ( for b1 being Element of bool Y holds
( not b1 in Q or A = b1 or A misses b1 ) ) ) )
assume A in Q ; :: thesis: ( not A = {} & ( for b1 being Element of bool Y holds
( not b1 in Q or A = b1 or A misses b1 ) ) )
then consider p being Element of P such that
A5: ( A = p /\ Y & p meets Y ) ;
thus A <> {} by A5, XBOOLE_0:def 7; :: thesis: for b1 being Element of bool Y holds
( not b1 in Q or A = b1 or A misses b1 )
let B be Subset of Y; :: thesis: ( not B in Q or A = B or A misses B )
assume B in Q ; :: thesis: ( A = B or A misses B )
then consider p1 being Element of P such that
A6: ( B = p1 /\ Y & p1 meets Y ) ;
assume A <> B ; :: thesis: A misses B
then p misses p1 by A5, A6, EQREL_1:def 6;
then A misses p1 by A5, XBOOLE_1:74;
hence A misses B by A6, XBOOLE_1:74; :: thesis: verum
end;
hence { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y ; :: thesis: verum