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 Element of NAT
for B1 being Subset of A ex B2 being Subset of A st S1[n,B1,B2]
proof
let n be
Element of
NAT ;
:: thesis: for B1 being Subset of A ex B2 being Subset of A st S1[n,B1,B2]let B1 be
Subset of
A;
:: thesis: 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 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 ) } & not
x in the
carrier of
A )
;
:: thesis: 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, 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 A3:
(
x = (Den o,A) . p &
p in dom (Den o,A) &
rng p c= B1 )
;
x in rng (Den o,A)
by A3, FUNCT_1:def 5;
hence
contradiction
by A2;
:: thesis: 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
;
:: thesis: S1[n,B1,B2]
thus
S1[
n,
B1,
B2]
;
:: thesis: verum
end;
consider F being Function of NAT ,(bool the carrier of A) such that
A4:
( F . 0 = B & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 2(A1);
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
take a = F . n'; :: thesis: ex F being Function of NAT ,(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
; :: thesis: ( 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 A4; :: thesis: 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; :: thesis: 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 ) }
n in NAT
by ORDINAL1:def 13;
hence
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 A4; :: thesis: verum