let A be Universal_Algebra; :: thesis: for G being Subset of A holds
( G is GeneratorSet of A iff for I being Element of A ex n being Nat st I in G |^ n )
let B be Subset of A; :: thesis: ( B is GeneratorSet of A iff for I being Element of A ex n being Nat st I in B |^ n )
set X = { (B |^ n) where n is Element of NAT : verum } ;
consider C being Subset of A such that
A1: C = union { (B |^ n) where n is Element of NAT : verum } and
A2: C is opers_closed by Th24;
B |^ 0 = B by Th18;
then A3: B in { (B |^ n) where n is Element of NAT : verum } ;
thus ( B is GeneratorSet of A implies for I being Element of A ex n being Nat st I in B |^ n ) :: thesis: ( ( for I being Element of A ex n being Nat st I in B |^ n ) implies B is GeneratorSet of A )
proof
assume for D being Subset of A st D is opers_closed & B c= D holds
D = the carrier of A ; :: according to FREEALG:def 4 :: thesis: for I being Element of A ex n being Nat st I in B |^ n
then A4: C = the carrier of A by A1, A2, A3, ZFMISC_1:74;
let I be Element of A; :: thesis: ex n being Nat st I in B |^ n
consider Y being set such that
A5: I in Y and
A6: Y in { (B |^ n) where n is Element of NAT : verum } by A1, A4, TARSKI:def 4;
ex n being Element of NAT st Y = B |^ n by A6;
hence ex n being Nat st I in B |^ n by A5; :: thesis: verum
end;
assume A7: for I being Element of A ex n being Nat st I in B |^ n ; :: thesis: B is GeneratorSet of A
let D be Subset of A; :: according to FREEALG:def 4 :: thesis: ( not D is opers_closed or not B c= D or D = the carrier of A )
assume that
A8: D is opers_closed and
A9: B c= D ; :: thesis: D = the carrier of A
A10: union { (B |^ n) where n is Element of NAT : verum } c= D by A8, A9, Th25;
thus D c= the carrier of A ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of A c= D
let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin the carrier of A or not x nin D )
assume x in the carrier of A ; :: thesis: not x nin D
then reconsider I = x as Element of A ;
consider n being Nat such that
A11: I in B |^ n by A7;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
B |^ n in { (B |^ n) where n is Element of NAT : verum } ;
then I in union { (B |^ n) where n is Element of NAT : verum } by A11, TARSKI:def 4;
hence not x nin D by A10; :: thesis: verum