let f be non empty Function; :: thesis: for P being a_partition of dom f holds { (f | a) where a is Element of P : verum } is a_partition of f
set X = dom f;
let P be a_partition of dom f; :: thesis: { (f | a) where a is Element of P : verum } is a_partition of f
set Y = f;
set Q = { (f | a) where a is Element of P : verum } ;
{ (f | a) where a is Element of P : verum } c= bool f
then reconsider Q = { (f | a) where a is Element of P : verum } as Subset-Family of f ;
Q is a_partition of f
proof
f c= union Q
proof
let y,
z be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [y,z] in f or [y,z] in union Q )
assume A2:
[y,z] in f
;
:: thesis: [y,z] in union Q
then
(
y in dom f &
dom f = union P )
by EQREL_1:def 6, RELAT_1:def 4;
then consider p being
set such that A3:
(
y in p &
p in P )
by TARSKI:def 4;
(
[y,z] in f | p &
f | p in Q )
by A2, A3, RELAT_1:def 11;
hence
[y,z] in union Q
by TARSKI:def 4;
:: thesis: verum
end;
hence
f = union Q
by XBOOLE_0:def 10;
:: according to EQREL_1:def 6 :: thesis: for b1 being Element of bool f holds
( not b1 in Q or ( not b1 = {} & ( for b2 being Element of bool f holds
( not b2 in Q or b1 = b2 or b1 misses b2 ) ) ) )
let A be
Subset of
f;
:: thesis: ( not A in Q or ( not A = {} & ( for b1 being Element of bool f 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 f holds
( not b1 in Q or A = b1 or A misses b1 ) ) )
then consider p being
Element of
P such that A4:
A = f | p
;
reconsider p =
p as non
empty Subset of
(dom f) ;
consider x being
Element of
p;
thus
A <> {}
by A4;
:: thesis: for b1 being Element of bool f holds
( not b1 in Q or A = b1 or A misses b1 )
let B be
Subset of
f;
:: 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 A5:
B = f | p1
;
assume
A <> B
;
:: thesis: A misses B
then A6:
p misses p1
by A4, A5, EQREL_1:def 6;
assume
A meets B
;
:: thesis: contradiction
then consider x being
set such that A7:
(
x in A &
x in B )
by XBOOLE_0:3;
consider y,
z being
set such that A8:
x = [y,z]
by A7, RELAT_1:def 1;
(
y in p &
y in p1 )
by A4, A5, A7, A8, RELAT_1:def 11;
hence
contradiction
by A6, XBOOLE_0:3;
:: thesis: verum
end;
hence
{ (f | a) where a is Element of P : verum } is a_partition of f
; :: thesis: verum