defpred S1[ set , set , set ] means $3 = $2 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= $2 ) } ;
A1:
for n being Nat
for B1 being Subset of A ex B2 being Subset of A st S1[n,B1,B2]
proof
let n be
Nat;
for B1 being Subset of A ex B2 being Subset of A st S1[n,B1,B2]let B1 be
Subset of
A;
ex B2 being Subset of A st S1[n,B1,B2]
set B2 =
B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } ;
B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } c= the
carrier of
A
proof
let x be
object ;
TARSKI:def 3 ( x nin B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } or not x nin the carrier of A )
assume that A2:
x in B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) }
and A3:
not
x in the
carrier of
A
;
contradiction
(
x in B1 implies
x in the
carrier of
A )
;
then
x in { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) }
by A2, A3, XBOOLE_0:def 3;
then consider o being
Element of
dom the
charact of
A,
p being
Element of the
carrier of
A * such that A4:
x = (Den (o,A)) . p
and A5:
p in dom (Den (o,A))
and
rng p c= B1
;
x in rng (Den (o,A))
by A4, A5, FUNCT_1:def 3;
hence
contradiction
by A3;
verum
end;
then reconsider B2 =
B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } as
Subset of
A ;
take
B2
;
S1[n,B1,B2]
thus
S1[
n,
B1,
B2]
;
verum
end;
consider F being sequence of (bool the carrier of A) such that
A6:
( F . 0 = B & ( for n being Nat holds S1[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 2(A1);
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
take a = F . n9; ex F being sequence of (bool the carrier of A) st
( a = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) )
take
F
; ( a = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) )
thus
( a = F . n & F . 0 = B )
by A6; for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) }
let n be Nat; F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) }
thus
F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) }
by A6; verum