let A be Universal_Algebra; for B being Subset of A ex C being Subset of A st
( C = union { (B |^ n) where n is Element of NAT : verum } & C is opers_closed )
let B be Subset of A; ex C being Subset of A st
( C = union { (B |^ n) where n is Element of NAT : verum } & C is opers_closed )
set X = { (B |^ n) where n is Element of NAT : verum } ;
set C = union { (B |^ n) where n is Element of NAT : verum } ;
A1:
union (bool the carrier of A) = the carrier of A
by ZFMISC_1:81;
{ (B |^ n) where n is Element of NAT : verum } c= bool the carrier of A
then reconsider C = union { (B |^ n) where n is Element of NAT : verum } as Subset of A by A1, ZFMISC_1:77;
take
C
; ( C = union { (B |^ n) where n is Element of NAT : verum } & C is opers_closed )
thus
C = union { (B |^ n) where n is Element of NAT : verum }
; C is opers_closed
let o be Element of Operations A; UNIALG_2:def 4 C is_closed_on o
consider s being object such that
A2:
s in dom the charact of A
and
A3:
o = the charact of A . s
by FUNCT_1:def 3;
reconsider s = s as OperSymbol of A by A2;
A4:
dom o = (arity o) -tuples_on the carrier of A
by MARGREL1:22;
let p be FinSequence of C; UNIALG_2:def 3 ( not len p = arity o or o . p in C )
assume
len p = arity o
; o . p in C
then
p is Element of dom (Den (s,A))
by A3, A4, FINSEQ_2:92;
then A5:
p in dom (Den (s,A))
;
defpred S1[ set , Nat] means $1 in B |^ $2;
A6:
rng p is finite
;
A7:
for x being Element of A st x in rng p holds
ex n being Nat st S1[x,n]
A12:
for x being Element of A
for n, m being Nat st S1[x,n] & n <= m holds
S1[x,m]
proof
let x be
Element of
A;
for n, m being Nat st S1[x,n] & n <= m holds
S1[x,m]let n,
m be
Nat;
( S1[x,n] & n <= m implies S1[x,m] )
assume A13:
S1[
x,
n]
;
( not n <= m or S1[x,m] )
assume
n <= m
;
S1[x,m]
then
B |^ n c= B |^ m
by Th21;
hence
S1[
x,
m]
by A13;
verum
end;
consider n being Nat such that
A14:
for x being Element of A st x in rng p holds
S1[x,n]
from AOFA_000:sch 1(A6, A7, A12);
rng p c= B |^ n
by A14;
then
(Den (s,A)) . p in { ((Den (a,A)) . r) where a is Element of dom the charact of A, r is Element of the carrier of A * : ( r in dom (Den (a,A)) & rng r c= B |^ n ) }
by A5;
then
( o . p in (B |^ n) \/ { ((Den (a,A)) . r) where a is Element of dom the charact of A, r is Element of the carrier of A * : ( r in dom (Den (a,A)) & rng r c= B |^ n ) } & n + 1 in NAT )
by A3, XBOOLE_0:def 3;
then A15:
o . p in B |^ (n + 1)
by Th19;
B |^ (n + 1) in { (B |^ n) where n is Element of NAT : verum }
;
hence
o . p in C
by A15, TARSKI:def 4; verum