let Y be non empty set ; for PA, PB being a_partition of Y
for p0, x, y being set
for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
let PA, PB be a_partition of Y; for p0, x, y being set
for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
let p0, x, y be set ; for f being FinSequence of Y st p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB holds
y in p0
let f be FinSequence of Y; ( p0 c= Y & x in p0 & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 ) ) & p0 is_a_dependent_set_of PA & p0 is_a_dependent_set_of PB implies y in p0 )
assume that
A1:
p0 c= Y
and
A2:
( x in p0 & f . 1 = x )
and
A3:
( f . (len f) = y & 1 <= len f )
and
A4:
for i being Element of NAT st 1 <= i & i < len f holds
ex p2, p3, u being set st
( p2 in PA & p3 in PB & f . i in p2 & u in p2 & u in p3 & f . (i + 1) in p3 )
and
A5:
p0 is_a_dependent_set_of PA
and
A6:
p0 is_a_dependent_set_of PB
; y in p0
consider A1 being set such that
A7:
A1 c= PA
and
A1 <> {}
and
A8:
p0 = union A1
by A5, Def1;
consider B1 being set such that
A9:
B1 c= PB
and
B1 <> {}
and
A10:
p0 = union B1
by A6, Def1;
A11:
union PA = Y
by EQREL_1:def 6;
A12:
for A being set st A in PA holds
( A <> {} & ( for B being set holds
( not B in PA or A = B or A misses B ) ) )
by EQREL_1:def 6;
A13:
for A being set st A in PB holds
( A <> {} & ( for B being set holds
( not B in PB or A = B or A misses B ) ) )
by EQREL_1:def 6;
A14:
for k being Element of NAT st 1 <= k & k <= len f holds
f . k in p0
proof
defpred S1[
Element of
NAT ]
means ( 1
<= $1 & $1
<= len f implies
f . $1
in p0 );
A15:
S1[
0 ]
;
A16:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A17:
S1[
k]
;
S1[k + 1]
assume that A18:
1
<= k + 1
and A19:
k + 1
<= len f
;
f . (k + 1) in p0
A20:
k < len f
by A19, NAT_1:13;
A21:
( 1
<= k or 1
= k + 1 )
by A18, NAT_1:8;
A22:
now per cases
( 1 <= k or 0 = k )
by A21;
suppose A23:
1
<= k
;
f . (k + 1) in p0consider p2,
p3,
u being
set such that A24:
p2 in PA
and A25:
p3 in PB
and A26:
f . k in p2
and A27:
u in p2
and A28:
u in p3
and A29:
f . (k + 1) in p3
by A4, A20, A23;
consider A being
set such that A30:
f . k in A
and A31:
A in PA
by A1, A11, A17, A19, A23, NAT_1:13, TARSKI:def 4;
A32:
(
p2 = A or
p2 misses A )
by A24, A31, EQREL_1:def 6;
consider a being
set such that A33:
f . k in a
and A34:
a in A1
by A8, A17, A19, A23, NAT_1:13, TARSKI:def 4;
A35:
(
a = p2 or
a misses p2 )
by A7, A12, A24, A34;
A36:
A c= p0
by A8, A26, A30, A32, A33, A34, A35, XBOOLE_0:3, ZFMISC_1:92;
consider B being
set such that A37:
u in B
and A38:
B in PB
by A25, A28;
A39:
(
p3 = B or
p3 misses B )
by A25, A38, EQREL_1:def 6;
consider b being
set such that A40:
u in b
and A41:
b in B1
by A10, A26, A27, A30, A32, A36, TARSKI:def 4, XBOOLE_0:3;
A42:
(
p3 = b or
p3 misses b )
by A9, A13, A25, A41;
A43:
B c= p0
by A10, A28, A37, A39, A40, A41, A42, XBOOLE_0:3, ZFMISC_1:92;
thus
f . (k + 1) in p0
by A28, A29, A37, A39, A43, XBOOLE_0:3;
verum end;
thus
f . (k + 1) in p0
by A22;
verum
end;
thus
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A15, A16); verum
end;
thus
y in p0
by A3, A14; verum