reconsider A = <*F2()*> as Element of (bool (bool F1())) * by FINSEQ_1:def 11;
defpred S1[ 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 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 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
Nat;
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())) * ;
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 Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } ;
now for X being object st X in { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } holds
X in bool F1()let X be
object ;
( X in { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being 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() )reconsider XX =
X as
set by TARSKI:1;
assume
X in { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] }
;
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 Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] }
and
P1[
V]
;
then
XX c= F1()
;
hence
X in bool F1()
;
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 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()
by TARSKI:def 3;
reconsider T1 =
<*T*> as
FinSequence of
bool (bool F1()) ;
consider y being
FinSequence of
bool (bool F1()) such that A5:
y = x ^ T1
;
reconsider y =
y as
Element of
(bool (bool F1())) * by FINSEQ_1:def 11;
take
y
;
S1[n,x,y]
thus
S1[
n,
x,
y]
by A5;
verum
end;
consider g being sequence of ((bool (bool F1())) *) such that
A6:
g . 0 = A
and
A7:
for n being Nat holds S1[n,g . n,g . (n + 1)]
from RECDEF_1:sch 2(A1);
defpred S2[ Nat] means len (g . $1) = $1 + 1;
A8:
for k being Nat st S2[k] holds
S2[k + 1]
deffunc H1( Nat) -> Element of bool (bool F1()) = (g . $1) /. (len (g . $1));
consider f being sequence of (bool (bool F1())) such that
A10:
for n being Element of NAT holds f . n = H1(n)
from FUNCT_2:sch 4();
A11:
for n being Nat holds f . n = H1(n)
take
f
; ( f . 0 = F2() & ( for n being 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 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:39;
hence f . 0 =
<*F2()*> /. 1
by A6, A11
.=
F2()
by FINSEQ_4:16
;
for n being 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 Nat st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] }
let n be Nat; f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] }
reconsider n = n as Element of NAT by ORDINAL1:def 12;
defpred S3[ Nat] means for q being Nat st q <= $1 holds
f . q = (g . $1) /. (q + 1);
A12:
S2[ 0 ]
by A6, FINSEQ_1:39;
A13:
for n being Nat holds S2[n]
from NAT_1:sch 2(A12, A8);
then A14:
(len (g . n)) + 1 = (n + 1) + 1
;
A15:
for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be
Nat;
( S3[k] implies S3[k + 1] )
assume A16:
for
q being
Nat st
q <= k holds
f . q = (g . k) /. (q + 1)
;
S3[k + 1]
let q be
Nat;
( q <= k + 1 implies f . q = (g . (k + 1)) /. (q + 1) )
assume A17:
q <= k + 1
;
f . q = (g . (k + 1)) /. (q + 1)
now f . q = (g . (k + 1)) /. (q + 1)per cases
( q = k + 1 or q < k + 1 )
by A17, XXREAL_0:1;
suppose A19:
q < k + 1
;
(g . (k + 1)) /. (q + 1) = f . qA20:
q + 1
>= 1
by NAT_1:11;
q + 1
<= k + 1
by A19, NAT_1:13;
then A21:
q + 1
in Seg (k + 1)
by A20, FINSEQ_1:1;
then
q + 1
in Seg (len (g . k))
by A13;
then A22:
q + 1
in dom (g . k)
by FINSEQ_1:def 3;
A23:
q <= k
by A19, NAT_1:13;
(k + 1) + 1
>= k + 1
by NAT_1:11;
then
Seg (k + 1) c= Seg ((k + 1) + 1)
by FINSEQ_1:5;
then
q + 1
in Seg ((k + 1) + 1)
by A21;
then
q + 1
in Seg (len (g . (k + 1)))
by A13;
then
q + 1
in dom (g . (k + 1))
by FINSEQ_1:def 3;
hence (g . (k + 1)) /. (q + 1) =
(g . (k + 1)) . (q + 1)
by PARTFUN1:def 6
.=
((g . k) ^ <* { (union { F3(c,k) where c is Element of F1() : for fq being Subset-Family of F1()
for q being 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 A7
.=
(g . k) . (q + 1)
by A22, FINSEQ_1:def 7
.=
(g . k) /. (q + 1)
by A22, PARTFUN1:def 6
.=
f . q
by A16, A23
;
verum end; end; end;
hence
f . q = (g . (k + 1)) /. (q + 1)
;
verum
end;
deffunc H2( set ) -> set = union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = (g . n) /. (q + 1) 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 Nat st q <= n & fq = f . q holds
P2[c,$1,n,fq] } ;
set NF = { H3(V) where V is Subset of F1() : P1[V] } ;
len (g . (n + 1)) = (n + 1) + 1
by A13;
then A24:
dom (g . (n + 1)) = Seg ((n + 1) + 1)
by FINSEQ_1:def 3;
A25:
S3[ 0 ]
A27:
for n being Nat holds S3[n]
from NAT_1:sch 2(A25, A15);
A28:
for V being Subset of F1() st P1[V] holds
H3(V) = H2(V)
proof
deffunc H4(
set )
-> Subset of
F1() =
F3($1,
n);
let V be
Subset of
F1();
( P1[V] implies H3(V) = H2(V) )
assume
P1[
V]
;
H3(V) = H2(V)
defpred S4[
set ]
means for
fq being
Subset-Family of
F1()
for
q being
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
Nat st
q <= n &
fq = (g . n) /. (q + 1) holds
P2[$1,
V,
n,
fq];
A29:
for
c being
Element of
F1() holds
(
S4[
c] iff
S5[
c] )
proof
let c be
Element of
F1();
( S4[c] iff S5[c] )
thus
( ( for
fq being
Subset-Family of
F1()
for
q being
Nat st
q <= n &
fq = f . q holds
P2[
c,
V,
n,
fq] ) implies for
fq being
Subset-Family of
F1()
for
q being
Nat st
q <= n &
fq = (g . n) /. (q + 1) holds
P2[
c,
V,
n,
fq] )
( S5[c] implies S4[c] )proof
assume A30:
for
fq being
Subset-Family of
F1()
for
q being
Nat st
q <= n &
fq = f . q holds
P2[
c,
V,
n,
fq]
;
for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq]
let fq be
Subset-Family of
F1();
for q being Nat st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq]let q be
Nat;
( q <= n & fq = (g . n) /. (q + 1) implies P2[c,V,n,fq] )
assume that A31:
q <= n
and A32:
fq = (g . n) /. (q + 1)
;
P2[c,V,n,fq]
fq = f . q
by A27, A31, A32;
hence
P2[
c,
V,
n,
fq]
by A30, A31;
verum
end;
assume A33:
for
fq being
Subset-Family of
F1()
for
q being
Nat st
q <= n &
fq = (g . n) /. (q + 1) holds
P2[
c,
V,
n,
fq]
;
S4[c]
let fq be
Subset-Family of
F1();
for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq]let q be
Nat;
( q <= n & fq = f . q implies P2[c,V,n,fq] )
assume that A34:
q <= n
and A35:
fq = f . q
;
P2[c,V,n,fq]
f . q = (g . n) /. (q + 1)
by A27, A34;
hence
P2[
c,
V,
n,
fq]
by A33, A34, A35;
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(A29);
hence
H3(
V)
= H2(
V)
;
verum
end;
A36:
{ H3(V) where V is Subset of F1() : P1[V] } = { H2(V) where V is Subset of F1() : P1[V] }
from FRAENKEL:sch 6(A28);
then A37: len (g . (n + 1)) =
len ((g . n) ^ <* { H3(V) where V is Subset of F1() : P1[V] } *>)
by A7
.=
(len (g . n)) + 1
by FINSEQ_2:16
;
reconsider n1 = n + 1 as Element of NAT ;
f . n1 =
H1(n1)
by A11
.=
(g . n1) /. (len (g . n1))
.=
(g . n1) /. ((len (g . n)) + 1)
by A37
.=
(g . (n + 1)) . ((len (g . n)) + 1)
by A24, A14, FINSEQ_1:4, PARTFUN1:def 6
.=
((g . n) ^ <* { H3(V) where V is Subset of F1() : P1[V] } *>) . ((len (g . n)) + 1)
by A7, A36
.=
{ H3(V) where V is Subset of F1() : P1[V] }
by FINSEQ_1:42
;
hence
f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] }
; verum