let X be set ; for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X
for SM being Function of NATPLUS,S
for n being NatPlus
for x being set st x in SM . n holds
ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
let S be cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X; for SM being Function of NATPLUS,S
for n being NatPlus
for x being set st x in SM . n holds
ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
let SM be Function of NATPLUS,S; for n being NatPlus
for x being set st x in SM . n holds
ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
let n be NatPlus; for x being set st x in SM . n holds
ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
let x be set ; ( x in SM . n implies ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) ) )
assume A1:
x in SM . n
; ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
defpred S1[ Nat] means ( $1 is NatPlus & ( for y being set st y in SM . $1 holds
ex n1, n0 being NatPlus ex np being Nat st
( $1 = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) ) );
A2:
for k being Nat st k >= 1 & ( for l being Nat st l >= 1 & l < k holds
S1[l] ) holds
S1[k]
proof
let k be
Nat;
( k >= 1 & ( for l being Nat st l >= 1 & l < k holds
S1[l] ) implies S1[k] )
assume A3:
k >= 1
;
( ex l being Nat st
( l >= 1 & l < k & not S1[l] ) or S1[k] )
assume A4:
for
l being
Nat st
l >= 1 &
l < k holds
S1[
l]
;
S1[k]
A5:
k is
NatPlus
by A3, NAT_LAT:def 6;
for
y being
set st
y in SM . k holds
ex
n1,
n0 being
NatPlus ex
np being
Nat st
(
k = n1 &
n0 <= n1 &
np = n0 - 1 &
y in (SM . n0) \ (Union (SM | (Seg np))) )
proof
let y be
set ;
( y in SM . k implies ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) ) )
assume A6:
y in SM . k
;
ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) )
set k0 =
k - 1;
reconsider k0 =
k - 1 as
Nat by A3, CHORD:1;
set n1 =
k;
A7:
SM . k = ((SM . k) \ (Union (SM | (Seg k0)))) \/ ((SM . k) /\ (Union (SM | (Seg k0))))
by XBOOLE_1:51;
A8:
(
y in (SM . k) \ (Union (SM | (Seg k0))) implies ex
n1,
n0 being
NatPlus ex
np being
Nat st
(
k = n1 &
n0 <= n1 &
np = n0 - 1 &
y in (SM . n0) \ (Union (SM | (Seg np))) ) )
(
y in (SM . k) /\ (Union (SM | (Seg k0))) implies ex
n1,
n0 being
NatPlus ex
np being
Nat st
(
k = n1 &
n0 <= n1 &
np = n0 - 1 &
y in (SM . n0) \ (Union (SM | (Seg np))) ) )
proof
assume
y in (SM . k) /\ (Union (SM | (Seg k0)))
;
ex n1, n0 being NatPlus ex np being Nat st
( k = n1 & n0 <= n1 & np = n0 - 1 & y in (SM . n0) \ (Union (SM | (Seg np))) )
then
y in Union (SM | (Seg k0))
by XBOOLE_0:def 4;
then consider yy being
set such that A10:
(
y in yy &
yy in rng (SM | (Seg k0)) )
by TARSKI:def 4;
consider yyy being
object such that A11:
(
yyy in dom (SM | (Seg k0)) &
yy = (SM | (Seg k0)) . yyy )
by A10, FUNCT_1:def 3;
reconsider yyy =
yyy as
Nat by A11;
A12:
y in SM . yyy
by A10, A11, FUNCT_1:47;
A13:
( 1
<= yyy &
yyy <= k0 )
by A11, FINSEQ_1:1;
set kk =
k - 1;
A14:
k - 1 is
Nat
by A3, CHORD:1;
yyy <= k - 1
by A11, FINSEQ_1:1;
then
(
yyy < (k - 1) + 1 &
k = (k - 1) + 1 )
by A14, NAT_1:13;
then
(
yyy >= 1 &
yyy < k )
by A11, FINSEQ_1:1;
then consider n1,
n0 being
NatPlus,
np being
Nat such that A15:
(
yyy = n1 &
n0 <= n1 &
np = n0 - 1 &
y in (SM . n0) \ (Union (SM | (Seg np))) )
by A4, A12;
A16:
n0 <= k - 1
by A13, A15, XXREAL_0:2;
(k - 1) + 1
= k
;
then A17:
k - 1
<= k
by INT_1:6;
set n2 =
k;
thus
ex
n1,
n0 being
NatPlus ex
np being
Nat st
(
k = n1 &
n0 <= n1 &
np = n0 - 1 &
y in (SM . n0) \ (Union (SM | (Seg np))) )
by A5, A15, A16, A17, XXREAL_0:2;
verum
end;
hence
ex
n1,
n0 being
NatPlus ex
np being
Nat st
(
k = n1 &
n0 <= n1 &
np = n0 - 1 &
y in (SM . n0) \ (Union (SM | (Seg np))) )
by A6, A7, A8, XBOOLE_0:def 3;
verum
end;
hence
S1[
k]
by A3, NAT_LAT:def 6;
verum
end;
A18:
for k being Nat st k >= 1 holds
S1[k]
from NAT_1:sch 9(A2);
for k being NatPlus holds S1[k]
then consider n1, n0 being NatPlus, np being Nat such that
A19:
( n = n1 & n0 <= n1 & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
by A1;
thus
ex n0 being NatPlus ex np being Nat st
( n0 <= n & np = n0 - 1 & x in (SM . n0) \ (Union (SM | (Seg np))) )
by A19; verum