defpred S1[ set , set , set , set ] means ( P2[$1,$2,$3] & not $1 in union $4 );
consider f being Function of NAT,(bool (bool F1())) such that
A1: f . 0 = F2() and
A2: 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
S1[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } from PCOMPS_2:sch 2();
 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() : ( P2[c,V,n] & not c in union { (union (f . q)) where q is Element of NAT : q <= n } ) } ) where V is Subset of F1() : P1[V] } ) )
thus f . 0 = F2() by A1; :: thesis: for n being Element of NAT holds f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union { (union (f . q)) where q is Element of NAT : q <= n } ) } ) where V is Subset of F1() : P1[V] }
let n be Element of NAT ; :: thesis: f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union { (union (f . q)) where q is Element of NAT : q <= n } ) } ) where V is Subset of F1() : P1[V] }
deffunc H1( 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] & not c in union fq ) } ;
deffunc H2( set ) -> set = union { F3(c,n) where c is Element of F1() : ( P2[c,$1,n] & not c in union { (union (f . q)) where q is Element of NAT : q <= n } ) } ;
set fxxx1 = { H1(V) where V is Subset of F1() : P1[V] } ;
set fxxx = { H2(V) where V is Subset of F1() : P1[V] } ;
A3: now
deffunc H3( set ) -> Subset of F1() = F3($1,n);
let V be Subset of F1(); :: thesis: ( P1[V] implies H1(V) = H2(V) )
assume P1[V] ; :: thesis: H1(V) = H2(V)
defpred S2[ 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] & not $1 in union fq );
defpred S3[ set ] means ( P2[$1,V,n] & not $1 in union { (union (f . q1)) where q1 is Element of NAT : q1 <= n } );
A4: now
let c be Element of F1(); :: thesis: ( S2[c] iff S3[c] )
A5: ( ( for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq ) iff not c in union { (union (f . q)) where q is Element of NAT : q <= n } )
proof
thus ( ( for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq ) implies not c in union { (union (f . q)) where q is Element of NAT : q <= n } ) :: thesis: ( not c in union { (union (f . q)) where q is Element of NAT : q <= n } implies for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq )
proof
assume A6: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq ; :: thesis: not c in union { (union (f . q)) where q is Element of NAT : q <= n }
assume c in union { (union (f . q)) where q is Element of NAT : q <= n } ; :: thesis: contradiction
then consider C being set such that
A7: c in C and
A8: C in { (union (f . q)) where q is Element of NAT : q <= n } by TARSKI:def 4;
ex q being Element of NAT st
( C = union (f . q) & q <= n ) by A8;
hence contradiction by A6, A7; :: thesis: verum
end;
assume A9: not c in union { (union (f . q)) where q is Element of NAT : q <= n } ; :: thesis: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq
let fq be Subset-Family of F1(); :: thesis: for q being Element of NAT st q <= n & fq = f . q holds
not c in union fq
let q be Element of NAT ; :: thesis: ( q <= n & fq = f . q implies not c in union fq )
assume ( q <= n & fq = f . q ) ; :: thesis: not c in union fq
then A10: union fq in { (union (f . p)) where p is Element of NAT : p <= n } ;
assume c in union fq ; :: thesis: contradiction
hence contradiction by A9, A10, TARSKI:def 4; :: thesis: verum
end;
thus ( S2[c] iff S3[c] ) :: thesis: verum
proof
hereby :: thesis: ( S3[c] implies S2[c] )
consider q being Element of NAT such that
A11: q <= n ;
assume A12: for fq being Subset-Family of F1()
for q being Element of NAT st q <= n & fq = f . q holds
( P2[c,V,n] & not c in union fq ) ; :: thesis: ( P2[c,V,n] & not c in union { (union (f . p)) where p is Element of NAT : p <= n } )
ex fq being Subset-Family of F1() st fq = f . q ;
hence P2[c,V,n] by A12, A11; :: thesis: not c in union { (union (f . p)) where p is Element of NAT : p <= n }
thus not c in union { (union (f . p)) where p is Element of NAT : p <= n } by A5, A12; :: thesis: verum
end;
assume ( P2[c,V,n] & not c in union { (union (f . q)) where q is Element of NAT : q <= n } ) ; :: thesis: S2[c]
hence S2[c] by A5; :: thesis: verum
end;
end;
{ H3(c) where c is Element of F1() : S2[c] } = { H3(c) where c is Element of F1() : S3[c] } from FRAENKEL:sch 3(A4);
hence H1(V) = H2(V) ; :: thesis: verum
end;
{ H1(V) where V is Subset of F1() : P1[V] } = { H2(V) where V is Subset of F1() : P1[V] } from FRAENKEL:sch 6(A3);
 hence f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union { (union (f . q)) where q is Element of NAT : q <= n } ) } ) where V is Subset of F1() : P1[V] } by A2; :: thesis: verum