defpred S1[ Element of NAT , FinSequence of bool (bool F1()), set ] means $3 = $2 ^ <*{ (union { F3(c,$1) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= $1 & fq = $2 /. (q + 1) holds
P2[c,V,$1,fq] } ) where V is Subset of F1() : P1[V] } *>;
A1:
for n being Element of NAT
for x being Element of (bool (bool F1())) * ex y being Element of (bool (bool F1())) * st S1[n,x,y]
proof
let n be
Element of
NAT ;
:: thesis: for x being Element of (bool (bool F1())) * ex y being Element of (bool (bool F1())) * st S1[n,x,y]let x be
Element of
(bool (bool F1())) * ;
:: thesis: ex y being Element of (bool (bool F1())) * st S1[n,x,y]
set T =
{ (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } ;
{ (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } in bool (bool F1())
proof
now let X be
set ;
:: thesis: ( X in { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } implies X in bool F1() )assume
X in { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] }
;
:: thesis: X in bool F1()then consider V being
Subset of
F1()
such that A2:
X = union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] }
and
P1[
V]
;
now let a be
set ;
:: thesis: ( a in X implies a in F1() )assume
a in X
;
:: thesis: a in F1()then consider P being
set such that A3:
a in P
and A4:
P in { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] }
by A2, TARSKI:def 4;
consider c being
Element of
F1()
such that A5:
P = F3(
c,
n)
and
for
fq being
Subset-Family of
F1()
for
q being
Element of
NAT st
q <= n &
fq = x /. (q + 1) holds
P2[
c,
V,
n,
fq]
by A4;
thus
a in F1()
by A3, A5;
:: thesis: verum end; then
X c= F1()
by TARSKI:def 3;
hence
X in bool F1()
;
:: thesis: verum end;
then
{ (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } c= bool F1()
by TARSKI:def 3;
hence
{ (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } in bool (bool F1())
;
:: thesis: verum
end;
then reconsider T =
{ (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } as
Subset-Family of
F1() ;
reconsider T1 =
<*T*> as
FinSequence of
bool (bool F1()) ;
consider y being
FinSequence of
bool (bool F1()) such that A6:
y = x ^ T1
;
reconsider y =
y as
Element of
(bool (bool F1())) * by FINSEQ_1:def 11;
take
y
;
:: thesis: S1[n,x,y]
thus
S1[
n,
x,
y]
by A6;
:: thesis: verum
end;
reconsider A = <*F2()*> as Element of (bool (bool F1())) * by FINSEQ_1:def 11;
consider g being Function of NAT ,((bool (bool F1())) * ) such that
A7:
g . 0 = A
and
A8:
for n being Element of NAT holds S1[n,g . n,g . (n + 1)]
from RECDEF_1:sch 2(A1);
deffunc H1( Element of NAT ) -> Element of bool (bool F1()) = (g . $1) /. (len (g . $1));
consider f being Function of NAT ,(bool (bool F1())) such that
A9:
for n being Element of NAT holds f . n = H1(n)
from FUNCT_2:sch 4();
take
f
; :: thesis: ( f . 0 = F2() & ( for n being Element of NAT holds f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } ) )
len <*F2()*> = 1
by FINSEQ_1:56;
hence f . 0 =
<*F2()*> /. 1
by A7, A9
.=
F2()
by FINSEQ_4:25
;
:: thesis: for n being Element of NAT holds f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] }
defpred S2[ Element of NAT ] means len (g . $1) = $1 + 1;
A10:
S2[ 0 ]
by A7, FINSEQ_1:56;
A11:
for k being Element of NAT st S2[k] holds
S2[k + 1]
A13:
for n being Element of NAT holds S2[n]
from NAT_1:sch 1(A10, A11);
defpred S3[ Element of NAT ] means for q being Element of NAT st q <= $1 holds
f . q = (g . $1) /. (q + 1);
A14:
S3[ 0 ]
A16:
for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S3[k] implies S3[k + 1] )
assume A17:
for
q being
Element of
NAT st
q <= k holds
f . q = (g . k) /. (q + 1)
;
:: thesis: S3[k + 1]
let q be
Element of
NAT ;
:: thesis: ( q <= k + 1 implies f . q = (g . (k + 1)) /. (q + 1) )
assume A18:
q <= k + 1
;
:: thesis: f . q = (g . (k + 1)) /. (q + 1)
now per cases
( q = k + 1 or q < k + 1 )
by A18, XXREAL_0:1;
suppose A20:
q < k + 1
;
:: thesis: (g . (k + 1)) /. (q + 1) = f . qthen A21:
q + 1
<= k + 1
by NAT_1:13;
A22:
q <= k
by A20, NAT_1:13;
q + 1
>= 1
by NAT_1:11;
then A23:
q + 1
in Seg (k + 1)
by A21, FINSEQ_1:3;
(k + 1) + 1
>= k + 1
by NAT_1:11;
then
Seg (k + 1) c= Seg ((k + 1) + 1)
by FINSEQ_1:7;
then
q + 1
in Seg ((k + 1) + 1)
by A23;
then
q + 1
in Seg (len (g . (k + 1)))
by A13;
then A24:
q + 1
in dom (g . (k + 1))
by FINSEQ_1:def 3;
q + 1
in Seg (len (g . k))
by A13, A23;
then A25:
q + 1
in dom (g . k)
by FINSEQ_1:def 3;
thus (g . (k + 1)) /. (q + 1) =
(g . (k + 1)) . (q + 1)
by A24, PARTFUN1:def 8
.=
((g . k) ^ <*{ (union { F3(c,k) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= k & fq = (g . k) /. (q + 1) holds
P2[c,V,k,fq] } ) where V is Subset of F1() : P1[V] } *>) . (q + 1)
by A8
.=
(g . k) . (q + 1)
by A25, FINSEQ_1:def 7
.=
(g . k) /. (q + 1)
by A25, PARTFUN1:def 8
.=
f . q
by A17, A22
;
:: thesis: verum end;
hence
f . q = (g . (k + 1)) /. (q + 1)
;
:: thesis: verum
end;
A26:
for n being Element of NAT holds S3[n]
from NAT_1:sch 1(A14, A16);
let n be Element of NAT ; :: thesis: f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] }
deffunc H2( set ) -> set = union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
P2[c,$1,n,fq] } ;
deffunc H3( set ) -> set = union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,$1,n,fq] } ;
set NF = { H2(V) where V is Subset of F1() : P1[V] } ;
A27:
for V being Subset of F1() st P1[V] holds
H2(V) = H3(V)
proof
let V be
Subset of
F1();
:: thesis: ( P1[V] implies H2(V) = H3(V) )
assume
P1[
V]
;
:: thesis: H2(V) = H3(V)
deffunc H4(
set )
-> Subset of
F1() =
F3($1,
n);
defpred S4[
set ]
means for
fq being
Subset-Family of
F1()
for
q being
Element of
NAT st
q <= n &
fq = f . q holds
P2[$1,
V,
n,
fq];
defpred S5[
set ]
means for
fq being
Subset-Family of
F1()
for
q being
Element of
NAT st
q <= n &
fq = (g . n) /. (q + 1) holds
P2[$1,
V,
n,
fq];
A28:
for
c being
Element of
F1() holds
(
S4[
c] iff
S5[
c] )
proof
let c be
Element of
F1();
:: thesis: ( S4[c] iff S5[c] )
thus
( ( for
fq being
Subset-Family of
F1()
for
q being
Element of
NAT st
q <= n &
fq = f . q holds
P2[
c,
V,
n,
fq] ) implies for
fq being
Subset-Family of
F1()
for
q being
Element of
NAT st
q <= n &
fq = (g . n) /. (q + 1) holds
P2[
c,
V,
n,
fq] )
:: thesis: ( S5[c] implies S4[c] )proof
assume A29:
for
fq being
Subset-Family of
F1()
for
q being
Element of
NAT st
q <= n &
fq = f . q holds
P2[
c,
V,
n,
fq]
;
:: thesis: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq]
let fq be
Subset-Family of
F1();
:: thesis: for q being Element of NAT st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq]let q be
Element of
NAT ;
:: thesis: ( q <= n & fq = (g . n) /. (q + 1) implies P2[c,V,n,fq] )
assume A30:
(
q <= n &
fq = (g . n) /. (q + 1) )
;
:: thesis: P2[c,V,n,fq]
then
fq = f . q
by A26;
hence
P2[
c,
V,
n,
fq]
by A29, A30;
:: thesis: verum
end;
assume A31:
for
fq being
Subset-Family of
F1()
for
q being
Element of
NAT st
q <= n &
fq = (g . n) /. (q + 1) holds
P2[
c,
V,
n,
fq]
;
:: thesis: S4[c]
let fq be
Subset-Family of
F1();
:: thesis: for q being Element of NAT st q <= n & fq = f . q holds
P2[c,V,n,fq]let q be
Element of
NAT ;
:: thesis: ( q <= n & fq = f . q implies P2[c,V,n,fq] )
assume A32:
(
q <= n &
fq = f . q )
;
:: thesis: P2[c,V,n,fq]
then
f . q = (g . n) /. (q + 1)
by A26;
hence
P2[
c,
V,
n,
fq]
by A31, A32;
:: thesis: verum
end;
{ H4(c) where c is Element of F1() : S4[c] } = { H4(c) where c is Element of F1() : S5[c] }
from FRAENKEL:sch 3(A28);
hence
H2(
V)
= H3(
V)
;
:: thesis: verum
end;
A33:
{ H2(V) where V is Subset of F1() : P1[V] } = { H3(V) where V is Subset of F1() : P1[V] }
from FRAENKEL:sch 6(A27);
then A34: len (g . (n + 1)) =
len ((g . n) ^ <*{ H2(V) where V is Subset of F1() : P1[V] } *>)
by A8
.=
(len (g . n)) + 1
by FINSEQ_2:19
;
A35:
(len (g . n)) + 1 in dom (g . (n + 1))
thus f . (n + 1) =
(g . (n + 1)) /. ((len (g . n)) + 1)
by A9, A34
.=
(g . (n + 1)) . ((len (g . n)) + 1)
by A35, PARTFUN1:def 8
.=
((g . n) ^ <*{ H2(V) where V is Subset of F1() : P1[V] } *>) . ((len (g . n)) + 1)
by A8, A33
.=
{ H2(V) where V is Subset of F1() : P1[V] }
by FINSEQ_1:59
; :: thesis: verum