:: FLANG_3 semantic presentation
begin
theorem :: FLANG_3:1
for E being set
for B, A being Subset of (E ^omega) st B c= A * holds
( (A *) ^^ B c= A * & B ^^ (A *) c= A * )
proof
let E be set ; ::_thesis: for B, A being Subset of (E ^omega) st B c= A * holds
( (A *) ^^ B c= A * & B ^^ (A *) c= A * )
let B, A be Subset of (E ^omega); ::_thesis: ( B c= A * implies ( (A *) ^^ B c= A * & B ^^ (A *) c= A * ) )
assume A1: B c= A * ; ::_thesis: ( (A *) ^^ B c= A * & B ^^ (A *) c= A * )
then A2: B ^^ (A *) c= (A *) ^^ (A *) by FLANG_1:17;
(A *) ^^ B c= (A *) ^^ (A *) by A1, FLANG_1:17;
hence ( (A *) ^^ B c= A * & B ^^ (A *) c= A * ) by A2, FLANG_1:63; ::_thesis: verum
end;
begin
definition
let E be set ;
let A be Subset of (E ^omega);
let n be Nat;
funcA |^.. n -> Subset of (E ^omega) equals :: FLANG_3:def 1
union { B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m & B = A |^ m ) } ;
coherence
union { B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m & B = A |^ m ) } is Subset of (E ^omega)
proof
defpred S1[ set ] means ex m being Nat st
( n <= m & $1 = A |^ m );
reconsider M = { B where B is Subset of (E ^omega) : S1[B] } as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
union M is Subset of (E ^omega) ;
hence union { B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m & B = A |^ m ) } is Subset of (E ^omega) ; ::_thesis: verum
end;
end;
:: deftheorem defines |^.. FLANG_3:def_1_:_
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^.. n = union { B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m & B = A |^ m ) } ;
theorem Th2: :: FLANG_3:2
for E, x being set
for A being Subset of (E ^omega)
for n being Nat holds
( x in A |^.. n iff ex m being Nat st
( n <= m & x in A |^ m ) )
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds
( x in A |^.. n iff ex m being Nat st
( n <= m & x in A |^ m ) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds
( x in A |^.. n iff ex m being Nat st
( n <= m & x in A |^ m ) )
let n be Nat; ::_thesis: ( x in A |^.. n iff ex m being Nat st
( n <= m & x in A |^ m ) )
thus ( x in A |^.. n implies ex m being Nat st
( n <= m & x in A |^ m ) ) ::_thesis: ( ex m being Nat st
( n <= m & x in A |^ m ) implies x in A |^.. n )
proof
defpred S1[ set ] means ex m being Nat st
( n <= m & $1 = A |^ m );
assume x in A |^.. n ; ::_thesis: ex m being Nat st
( n <= m & x in A |^ m )
then consider X being set such that
A1: x in X and
A2: X in { B where B is Subset of (E ^omega) : ex m being Nat st
( n <= m & B = A |^ m ) } by TARSKI:def_4;
A3: X in { B where B is Subset of (E ^omega) : S1[B] } by A2;
S1[X] from CARD_FIL:sch_1(A3);
hence ex m being Nat st
( n <= m & x in A |^ m ) by A1; ::_thesis: verum
end;
given m being Nat such that A4: n <= m and
A5: x in A |^ m ; ::_thesis: x in A |^.. n
defpred S1[ set ] means ex m being Nat st
( n <= m & $1 = A |^ m );
consider B being Subset of (E ^omega) such that
A6: x in B and
A7: S1[B] by A4, A5;
reconsider A = { C where C is Subset of (E ^omega) : S1[C] } as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
B in A by A7;
hence x in A |^.. n by A6, TARSKI:def_4; ::_thesis: verum
end;
theorem Th3: :: FLANG_3:3
for E being set
for A being Subset of (E ^omega)
for n, m being Nat st n <= m holds
A |^ m c= A |^.. n
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n, m being Nat st n <= m holds
A |^ m c= A |^.. n
let A be Subset of (E ^omega); ::_thesis: for n, m being Nat st n <= m holds
A |^ m c= A |^.. n
let n, m be Nat; ::_thesis: ( n <= m implies A |^ m c= A |^.. n )
assume n <= m ; ::_thesis: A |^ m c= A |^.. n
then for x being set st x in A |^ m holds
x in A |^.. n by Th2;
hence A |^ m c= A |^.. n by TARSKI:def_3; ::_thesis: verum
end;
theorem Th4: :: FLANG_3:4
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = {} iff ( n > 0 & A = {} ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = {} iff ( n > 0 & A = {} ) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds
( A |^.. n = {} iff ( n > 0 & A = {} ) )
let n be Nat; ::_thesis: ( A |^.. n = {} iff ( n > 0 & A = {} ) )
thus ( A |^.. n = {} implies ( n > 0 & A = {} ) ) ::_thesis: ( n > 0 & A = {} implies A |^.. n = {} )
proof
A1: ( A <> {} implies A |^.. n <> {} )
proof
assume A2: A <> {} ; ::_thesis: A |^.. n <> {}
now__::_thesis:_for_m_being_Nat_holds_A_|^.._n_<>_{}
let m be Nat; ::_thesis: A |^.. n <> {}
consider m being Nat such that
A3: n <= m ;
A |^ m <> {} by A2, FLANG_1:27;
then ex x being set st x in A |^ m by XBOOLE_0:def_1;
hence A |^.. n <> {} by A3, Th2; ::_thesis: verum
end;
hence A |^.. n <> {} ; ::_thesis: verum
end;
assume that
A4: A |^.. n = {} and
A5: ( n <= 0 or A <> {} ) ; ::_thesis: contradiction
( n <= 0 implies <%> E in A |^.. n )
proof
assume n <= 0 ; ::_thesis: <%> E in A |^.. n
then A6: n = 0 ;
A |^ 0 c= A |^.. 0 by Th3;
then {(<%> E)} c= A |^.. 0 by FLANG_1:24;
hence <%> E in A |^.. n by A6, ZFMISC_1:31; ::_thesis: verum
end;
hence contradiction by A4, A5, A1; ::_thesis: verum
end;
assume that
A7: n > 0 and
A8: A = {} ; ::_thesis: A |^.. n = {}
now__::_thesis:_for_x_being_set_holds_not_x_in_A_|^.._n
let x be set ; ::_thesis: not x in A |^.. n
assume x in A |^.. n ; ::_thesis: contradiction
then ex m being Nat st
( n <= m & x in A |^ m ) by Th2;
hence contradiction by A7, A8, FLANG_1:27; ::_thesis: verum
end;
hence A |^.. n = {} by XBOOLE_0:def_1; ::_thesis: verum
end;
theorem Th5: :: FLANG_3:5
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
A |^.. n c= A |^.. m
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <= n holds
A |^.. n c= A |^.. m
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n holds
A |^.. n c= A |^.. m
let m, n be Nat; ::_thesis: ( m <= n implies A |^.. n c= A |^.. m )
assume A1: m <= n ; ::_thesis: A |^.. n c= A |^.. m
now__::_thesis:_for_x_being_set_st_x_in_A_|^.._n_holds_
x_in_A_|^.._m
let x be set ; ::_thesis: ( x in A |^.. n implies x in A |^.. m )
assume x in A |^.. n ; ::_thesis: x in A |^.. m
then consider k being Nat such that
A2: n <= k and
A3: x in A |^ k by Th2;
m <= k by A1, A2, XXREAL_0:2;
hence x in A |^.. m by A3, Th2; ::_thesis: verum
end;
hence A |^.. n c= A |^.. m by TARSKI:def_3; ::_thesis: verum
end;
theorem Th6: :: FLANG_3:6
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat st k <= m holds
A |^ (m,n) c= A |^.. k
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, m, n being Nat st k <= m holds
A |^ (m,n) c= A |^.. k
let A be Subset of (E ^omega); ::_thesis: for k, m, n being Nat st k <= m holds
A |^ (m,n) c= A |^.. k
let k, m, n be Nat; ::_thesis: ( k <= m implies A |^ (m,n) c= A |^.. k )
assume A1: k <= m ; ::_thesis: A |^ (m,n) c= A |^.. k
now__::_thesis:_for_x_being_set_st_x_in_A_|^_(m,n)_holds_
x_in_A_|^.._k
let x be set ; ::_thesis: ( x in A |^ (m,n) implies x in A |^.. k )
assume x in A |^ (m,n) ; ::_thesis: x in A |^.. k
then consider l being Nat such that
A2: m <= l and
l <= n and
A3: x in A |^ l by FLANG_2:19;
k <= l by A1, A2, XXREAL_0:2;
hence x in A |^.. k by A3, Th2; ::_thesis: verum
end;
hence A |^ (m,n) c= A |^.. k by TARSKI:def_3; ::_thesis: verum
end;
theorem Th7: :: FLANG_3:7
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n + 1 holds
(A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m <= n + 1 holds
(A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m <= n + 1 holds
(A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m
let m, n be Nat; ::_thesis: ( m <= n + 1 implies (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m )
assume m <= n + 1 ; ::_thesis: (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m
then A1: A |^.. (n + 1) c= A |^.. m by Th5;
now__::_thesis:_for_x_being_set_st_x_in_A_|^.._m_holds_
x_in_(A_|^_(m,n))_\/_(A_|^.._(n_+_1))
let x be set ; ::_thesis: ( x in A |^.. m implies x in (A |^ (m,n)) \/ (A |^.. (n + 1)) )
assume x in A |^.. m ; ::_thesis: x in (A |^ (m,n)) \/ (A |^.. (n + 1))
then consider k being Nat such that
A2: m <= k and
A3: x in A |^ k by Th2;
A4: now__::_thesis:_(_k_>_n_implies_x_in_A_|^.._(n_+_1)_)
assume k > n ; ::_thesis: x in A |^.. (n + 1)
then k >= n + 1 by NAT_1:13;
hence x in A |^.. (n + 1) by A3, Th2; ::_thesis: verum
end;
( k <= n implies x in A |^ (m,n) ) by A2, A3, FLANG_2:19;
hence x in (A |^ (m,n)) \/ (A |^.. (n + 1)) by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
then A5: A |^.. m c= (A |^ (m,n)) \/ (A |^.. (n + 1)) by TARSKI:def_3;
A |^ (m,n) c= A |^.. m by Th6;
then (A |^ (m,n)) \/ (A |^.. (n + 1)) c= A |^.. m by A1, XBOOLE_1:8;
hence (A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: FLANG_3:8
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n
let n be Nat; ::_thesis: (A |^ n) \/ (A |^.. (n + 1)) = A |^.. n
A1: n <= n + 1 by NAT_1:13;
thus (A |^ n) \/ (A |^.. (n + 1)) = (A |^ (n,n)) \/ (A |^.. (n + 1)) by FLANG_2:22
.= A |^.. n by A1, Th7 ; ::_thesis: verum
end;
theorem Th9: :: FLANG_3:9
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^.. n c= A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds A |^.. n c= A *
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A |^.. n c= A *
let n be Nat; ::_thesis: A |^.. n c= A *
now__::_thesis:_for_x_being_set_st_x_in_A_|^.._n_holds_
x_in_A_*
let x be set ; ::_thesis: ( x in A |^.. n implies x in A * )
assume x in A |^.. n ; ::_thesis: x in A *
then ex k being Nat st
( n <= k & x in A |^ k ) by Th2;
hence x in A * by FLANG_1:41; ::_thesis: verum
end;
hence A |^.. n c= A * by TARSKI:def_3; ::_thesis: verum
end;
theorem Th10: :: FLANG_3:10
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( <%> E in A |^.. n iff ( n = 0 or <%> E in A ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds
( <%> E in A |^.. n iff ( n = 0 or <%> E in A ) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds
( <%> E in A |^.. n iff ( n = 0 or <%> E in A ) )
let n be Nat; ::_thesis: ( <%> E in A |^.. n iff ( n = 0 or <%> E in A ) )
thus ( not <%> E in A |^.. n or n = 0 or <%> E in A ) ::_thesis: ( ( n = 0 or <%> E in A ) implies <%> E in A |^.. n )
proof
assume <%> E in A |^.. n ; ::_thesis: ( n = 0 or <%> E in A )
then A1: ex k being Nat st
( n <= k & <%> E in A |^ k ) by Th2;
( n = 0 or n > 0 ) ;
hence ( n = 0 or <%> E in A ) by A1, FLANG_1:31; ::_thesis: verum
end;
assume A2: ( n = 0 or <%> E in A ) ; ::_thesis: <%> E in A |^.. n
percases ( n = 0 or <%> E in A ) by A2;
supposeA3: n = 0 ; ::_thesis: <%> E in A |^.. n
{(<%> E)} = A |^ 0 by FLANG_1:24;
then <%> E in A |^ n by A3, TARSKI:def_1;
hence <%> E in A |^.. n by Th2; ::_thesis: verum
end;
suppose <%> E in A ; ::_thesis: <%> E in A |^.. n
then <%> E in A |^ n by FLANG_1:30;
hence <%> E in A |^.. n by Th2; ::_thesis: verum
end;
end;
end;
theorem Th11: :: FLANG_3:11
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = A * iff ( <%> E in A or n = 0 ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = A * iff ( <%> E in A or n = 0 ) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds
( A |^.. n = A * iff ( <%> E in A or n = 0 ) )
let n be Nat; ::_thesis: ( A |^.. n = A * iff ( <%> E in A or n = 0 ) )
thus ( not A |^.. n = A * or <%> E in A or n = 0 ) ::_thesis: ( ( <%> E in A or n = 0 ) implies A |^.. n = A * )
proof
assume that
A1: A |^.. n = A * and
A2: not <%> E in A and
A3: n <> 0 ; ::_thesis: contradiction
<%> E in A * by FLANG_1:48;
hence contradiction by A1, A2, A3, Th10; ::_thesis: verum
end;
assume A4: ( <%> E in A or n = 0 ) ; ::_thesis: A |^.. n = A *
now__::_thesis:_for_x_being_set_st_x_in_A_*_holds_
x_in_A_|^.._n
let x be set ; ::_thesis: ( x in A * implies b1 in A |^.. n )
assume x in A * ; ::_thesis: b1 in A |^.. n
then consider k being Nat such that
A5: x in A |^ k by FLANG_1:41;
percases ( n <= k or k < n ) ;
suppose n <= k ; ::_thesis: b1 in A |^.. n
hence x in A |^.. n by A5, Th2; ::_thesis: verum
end;
suppose k < n ; ::_thesis: b1 in A |^.. n
then A |^ k c= A |^ n by A4, FLANG_1:36;
hence x in A |^.. n by A5, Th2; ::_thesis: verum
end;
end;
end;
then A6: A * c= A |^.. n by TARSKI:def_3;
A |^.. n c= A * by Th9;
hence A |^.. n = A * by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: FLANG_3:12
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1))
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1))
let n be Nat; ::_thesis: A * = (A |^ (0,n)) \/ (A |^.. (n + 1))
thus A * = A |^.. 0 by Th11
.= (A |^ (0,n)) \/ (A |^.. (n + 1)) by Th7 ; ::_thesis: verum
end;
theorem Th13: :: FLANG_3:13
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B holds
A |^.. n c= B |^.. n
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for n being Nat st A c= B holds
A |^.. n c= B |^.. n
let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B holds
A |^.. n c= B |^.. n
let n be Nat; ::_thesis: ( A c= B implies A |^.. n c= B |^.. n )
assume A1: A c= B ; ::_thesis: A |^.. n c= B |^.. n
now__::_thesis:_for_x_being_set_st_x_in_A_|^.._n_holds_
x_in_B_|^.._n
let x be set ; ::_thesis: ( x in A |^.. n implies x in B |^.. n )
assume x in A |^.. n ; ::_thesis: x in B |^.. n
then consider k being Nat such that
A2: n <= k and
A3: x in A |^ k by Th2;
A |^ k c= B |^ k by A1, FLANG_1:37;
hence x in B |^.. n by A2, A3, Th2; ::_thesis: verum
end;
hence A |^.. n c= B |^.. n by TARSKI:def_3; ::_thesis: verum
end;
theorem Th14: :: FLANG_3:14
for x, E being set
for A being Subset of (E ^omega)
for n being Nat st x in A & x <> <%> E holds
A |^.. n <> {(<%> E)}
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st x in A & x <> <%> E holds
A |^.. n <> {(<%> E)}
let A be Subset of (E ^omega); ::_thesis: for n being Nat st x in A & x <> <%> E holds
A |^.. n <> {(<%> E)}
let n be Nat; ::_thesis: ( x in A & x <> <%> E implies A |^.. n <> {(<%> E)} )
assume that
A1: x in A and
A2: x <> <%> E ; ::_thesis: A |^.. n <> {(<%> E)}
percases ( n = 0 or n > 0 ) ;
supposeA3: n = 0 ; ::_thesis: A |^.. n <> {(<%> E)}
x in A |^ 1 by A1, FLANG_1:25;
then x in A |^.. n by A3, Th2;
hence A |^.. n <> {(<%> E)} by A2, TARSKI:def_1; ::_thesis: verum
end;
supposeA4: n > 0 ; ::_thesis: A |^.. n <> {(<%> E)}
A5: A |^ n <> {} by A1, FLANG_1:27;
A |^ n <> {(<%> E)} by A1, A2, A4, FLANG_2:7;
then consider y being set such that
A6: y in A |^ n and
A7: y <> <%> E by A5, ZFMISC_1:35;
y in A |^.. n by A6, Th2;
hence A |^.. n <> {(<%> E)} by A7, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
theorem Th15: :: FLANG_3:15
for E being set
for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) )
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds
( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) )
let n be Nat; ::_thesis: ( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) )
thus ( not A |^.. n = {(<%> E)} or A = {(<%> E)} or ( n = 0 & A = {} ) ) ::_thesis: ( ( A = {(<%> E)} or ( n = 0 & A = {} ) ) implies A |^.. n = {(<%> E)} )
proof
assume that
A1: A |^.. n = {(<%> E)} and
A2: A <> {(<%> E)} and
A3: ( n <> 0 or A <> {} ) ; ::_thesis: contradiction
percases ( n <> 0 or A <> {} ) by A3;
supposeA4: n <> 0 ; ::_thesis: contradiction
<%> E in A |^.. n by A1, ZFMISC_1:31;
then consider k being Nat such that
A5: n <= k and
A6: <%> E in A |^ k by Th2;
k > 0 by A4, A5;
then A7: <%> E in A by A6, FLANG_1:31;
for x being set holds
( not x in A or not x <> <%> E ) by A1, Th14;
hence contradiction by A2, A7, ZFMISC_1:35; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: contradiction
then ex x being set st
( x in A & x <> <%> E ) by A2, ZFMISC_1:35;
hence contradiction by A1, Th14; ::_thesis: verum
end;
end;
end;
assume A8: ( A = {(<%> E)} or ( n = 0 & A = {} ) ) ; ::_thesis: A |^.. n = {(<%> E)}
percases ( A = {(<%> E)} or ( n = 0 & A = {} ) ) by A8;
supposeA9: A = {(<%> E)} ; ::_thesis: A |^.. n = {(<%> E)}
A10: now__::_thesis:_for_x_being_set_st_x_in_{(<%>_E)}_holds_
x_in_A_|^.._n
let x be set ; ::_thesis: ( x in {(<%> E)} implies x in A |^.. n )
assume x in {(<%> E)} ; ::_thesis: x in A |^.. n
then x in A |^ n by A9, FLANG_1:28;
hence x in A |^.. n by Th2; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_A_|^.._n_holds_
x_in_{(<%>_E)}
let x be set ; ::_thesis: ( x in A |^.. n implies x in {(<%> E)} )
assume x in A |^.. n ; ::_thesis: x in {(<%> E)}
then ex k being Nat st
( n <= k & x in A |^ k ) by Th2;
hence x in {(<%> E)} by A9, FLANG_1:28; ::_thesis: verum
end;
hence A |^.. n = {(<%> E)} by A10, TARSKI:1; ::_thesis: verum
end;
supposeA11: ( n = 0 & A = {} ) ; ::_thesis: A |^.. n = {(<%> E)}
hence A |^.. n = A * by Th11
.= {(<%> E)} by A11, FLANG_1:47 ;
::_thesis: verum
end;
end;
end;
theorem Th16: :: FLANG_3:16
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A |^.. (n + 1) = (A |^.. n) ^^ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds A |^.. (n + 1) = (A |^.. n) ^^ A
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A |^.. (n + 1) = (A |^.. n) ^^ A
let n be Nat; ::_thesis: A |^.. (n + 1) = (A |^.. n) ^^ A
now__::_thesis:_for_x_being_set_st_x_in_A_|^.._(n_+_1)_holds_
x_in_(A_|^.._n)_^^_A
let x be set ; ::_thesis: ( x in A |^.. (n + 1) implies x in (A |^.. n) ^^ A )
assume x in A |^.. (n + 1) ; ::_thesis: x in (A |^.. n) ^^ A
then consider k being Nat such that
A1: n + 1 <= k and
A2: x in A |^ k by Th2;
consider l being Nat such that
A3: l + 1 = k by A1, NAT_1:6;
x in (A |^ l) ^^ (A |^ 1) by A2, A3, FLANG_1:33;
then consider a, b being Element of E ^omega such that
A4: a in A |^ l and
A5: b in A |^ 1 and
A6: x = a ^ b by FLANG_1:def_1;
n <= l by A1, A3, XREAL_1:6;
then a in A |^.. n by A4, Th2;
then x in (A |^.. n) ^^ (A |^ 1) by A5, A6, FLANG_1:def_1;
hence x in (A |^.. n) ^^ A by FLANG_1:25; ::_thesis: verum
end;
then A7: A |^.. (n + 1) c= (A |^.. n) ^^ A by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_(A_|^.._n)_^^_A_holds_
x_in_A_|^.._(n_+_1)
let x be set ; ::_thesis: ( x in (A |^.. n) ^^ A implies x in A |^.. (n + 1) )
assume x in (A |^.. n) ^^ A ; ::_thesis: x in A |^.. (n + 1)
then consider a, b being Element of E ^omega such that
A8: a in A |^.. n and
A9: b in A and
A10: x = a ^ b by FLANG_1:def_1;
consider k being Nat such that
A11: n <= k and
A12: a in A |^ k by A8, Th2;
A13: n + 1 <= k + 1 by A11, XREAL_1:6;
b in A |^ 1 by A9, FLANG_1:25;
then x in A |^ (k + 1) by A10, A12, FLANG_1:40;
hence x in A |^.. (n + 1) by A13, Th2; ::_thesis: verum
end;
then (A |^.. n) ^^ A c= A |^.. (n + 1) by TARSKI:def_3;
hence A |^.. (n + 1) = (A |^.. n) ^^ A by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th17: :: FLANG_3:17
for E being set
for A being Subset of (E ^omega)
for m being Nat holds (A |^.. m) ^^ (A *) = A |^.. m
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m being Nat holds (A |^.. m) ^^ (A *) = A |^.. m
let A be Subset of (E ^omega); ::_thesis: for m being Nat holds (A |^.. m) ^^ (A *) = A |^.. m
let m be Nat; ::_thesis: (A |^.. m) ^^ (A *) = A |^.. m
now__::_thesis:_for_x_being_set_st_x_in_(A_|^.._m)_^^_(A_*)_holds_
x_in_A_|^.._m
let x be set ; ::_thesis: ( x in (A |^.. m) ^^ (A *) implies x in A |^.. m )
assume x in (A |^.. m) ^^ (A *) ; ::_thesis: x in A |^.. m
then consider a, b being Element of E ^omega such that
A1: a in A |^.. m and
A2: b in A * and
A3: x = a ^ b by FLANG_1:def_1;
consider k being Nat such that
A4: b in A |^ k by A2, FLANG_1:41;
consider l being Nat such that
A5: m <= l and
A6: a in A |^ l by A1, Th2;
A7: l + k >= m by A5, NAT_1:12;
a ^ b in A |^ (l + k) by A4, A6, FLANG_1:40;
hence x in A |^.. m by A3, A7, Th2; ::_thesis: verum
end;
then A8: (A |^.. m) ^^ (A *) c= A |^.. m by TARSKI:def_3;
<%> E in A * by FLANG_1:48;
then A |^.. m c= (A |^.. m) ^^ (A *) by FLANG_1:16;
hence (A |^.. m) ^^ (A *) = A |^.. m by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th18: :: FLANG_3:18
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n)
let m, n be Nat; ::_thesis: (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n)
defpred S1[ Nat] means (A |^.. m) ^^ (A |^.. $1) = A |^.. (m + $1);
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
(A |^.. m) ^^ (A |^.. (n + 1)) = (A |^.. m) ^^ ((A |^.. n) ^^ A) by Th16
.= (A |^.. (m + n)) ^^ A by A2, FLANG_1:18
.= A |^.. ((m + n) + 1) by Th16 ;
hence S1[n + 1] ; ::_thesis: verum
end;
(A |^.. m) ^^ (A |^.. 0) = (A |^.. m) ^^ (A *) by Th11
.= A |^.. (m + 0) by Th17 ;
then A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n) ; ::_thesis: verum
end;
theorem Th19: :: FLANG_3:19
for E being set
for A being Subset of (E ^omega)
for n, m being Nat st n > 0 holds
(A |^.. m) |^ n = A |^.. (m * n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n, m being Nat st n > 0 holds
(A |^.. m) |^ n = A |^.. (m * n)
let A be Subset of (E ^omega); ::_thesis: for n, m being Nat st n > 0 holds
(A |^.. m) |^ n = A |^.. (m * n)
let n, m be Nat; ::_thesis: ( n > 0 implies (A |^.. m) |^ n = A |^.. (m * n) )
defpred S1[ Nat] means ( $1 > 0 implies (A |^.. m) |^ $1 = A |^.. (m * $1) );
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_(_n_+_1_>_0_implies_(A_|^.._m)_|^_(n_+_1)_=_A_|^.._(m_*_(n_+_1))_)
assume n + 1 > 0 ; ::_thesis: (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1))
percases ( n = 0 or n > 0 ) ;
suppose n = 0 ; ::_thesis: (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1))
hence (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1)) by FLANG_1:25; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1))
hence (A |^.. m) |^ (n + 1) = (A |^.. (m * n)) ^^ (A |^.. m) by A2, FLANG_1:23
.= A |^.. ((m * n) + m) by Th18
.= A |^.. (m * (n + 1)) ;
::_thesis: verum
end;
end;
end;
hence S1[n + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence ( n > 0 implies (A |^.. m) |^ n = A |^.. (m * n) ) ; ::_thesis: verum
end;
theorem :: FLANG_3:20
for E being set
for A being Subset of (E ^omega)
for n being Nat holds (A |^.. n) * = (A |^.. n) ?
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds (A |^.. n) * = (A |^.. n) ?
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds (A |^.. n) * = (A |^.. n) ?
let n be Nat; ::_thesis: (A |^.. n) * = (A |^.. n) ?
now__::_thesis:_for_x_being_set_st_x_in_(A_|^.._n)_*_holds_
x_in_(A_|^.._n)_?
let x be set ; ::_thesis: ( x in (A |^.. n) * implies b1 in (A |^.. n) ? )
assume x in (A |^.. n) * ; ::_thesis: b1 in (A |^.. n) ?
then consider k being Nat such that
A1: x in (A |^.. n) |^ k by FLANG_1:41;
percases ( k = 0 or k > 0 ) ;
suppose k = 0 ; ::_thesis: b1 in (A |^.. n) ?
then x in ((A |^.. n) |^ 0) \/ ((A |^.. n) |^ 1) by A1, XBOOLE_0:def_3;
hence x in (A |^.. n) ? by FLANG_2:75; ::_thesis: verum
end;
supposeA2: k > 0 ; ::_thesis: b1 in (A |^.. n) ?
then (A |^.. n) |^ k c= A |^.. (n * k) by Th19;
then consider l being Nat such that
A3: n * k <= l and
A4: x in A |^ l by A1, Th2;
k >= 0 + 1 by A2, NAT_1:13;
then n * k >= n by XREAL_1:151;
then l >= n by A3, XXREAL_0:2;
then x in A |^.. n by A4, Th2;
then x in (A |^.. n) |^ 1 by FLANG_1:25;
then x in ((A |^.. n) |^ 0) \/ ((A |^.. n) |^ 1) by XBOOLE_0:def_3;
hence x in (A |^.. n) ? by FLANG_2:75; ::_thesis: verum
end;
end;
end;
then A5: (A |^.. n) * c= (A |^.. n) ? by TARSKI:def_3;
(A |^.. n) ? c= (A |^.. n) * by FLANG_2:86;
hence (A |^.. n) * = (A |^.. n) ? by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th21: :: FLANG_3:21
for E being set
for A, C, B being Subset of (E ^omega)
for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds
A ^^ B c= C |^.. (m + n)
proof
let E be set ; ::_thesis: for A, C, B being Subset of (E ^omega)
for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds
A ^^ B c= C |^.. (m + n)
let A, C, B be Subset of (E ^omega); ::_thesis: for m, n being Nat st A c= C |^.. m & B c= C |^.. n holds
A ^^ B c= C |^.. (m + n)
let m, n be Nat; ::_thesis: ( A c= C |^.. m & B c= C |^.. n implies A ^^ B c= C |^.. (m + n) )
assume that
A1: A c= C |^.. m and
A2: B c= C |^.. n ; ::_thesis: A ^^ B c= C |^.. (m + n)
thus for x being set st x in A ^^ B holds
x in C |^.. (m + n) :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in A ^^ B implies x in C |^.. (m + n) )
assume x in A ^^ B ; ::_thesis: x in C |^.. (m + n)
then consider a, b being Element of E ^omega such that
A3: a in A and
A4: b in B and
A5: x = a ^ b by FLANG_1:def_1;
a ^ b in (C |^.. m) ^^ (C |^.. n) by A1, A2, A3, A4, FLANG_1:def_1;
hence x in C |^.. (m + n) by A5, Th18; ::_thesis: verum
end;
end;
theorem Th22: :: FLANG_3:22
for E being set
for A being Subset of (E ^omega)
for n, k being Nat holds A |^.. (n + k) = (A |^.. n) ^^ (A |^ k)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n, k being Nat holds A |^.. (n + k) = (A |^.. n) ^^ (A |^ k)
let A be Subset of (E ^omega); ::_thesis: for n, k being Nat holds A |^.. (n + k) = (A |^.. n) ^^ (A |^ k)
let n, k be Nat; ::_thesis: A |^.. (n + k) = (A |^.. n) ^^ (A |^ k)
defpred S1[ Nat] means A |^.. (n + $1) = (A |^.. n) ^^ (A |^ $1);
A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
A |^.. (n + (k + 1)) = A |^.. ((n + k) + 1)
.= ((A |^.. n) ^^ (A |^ k)) ^^ A by A2, Th16
.= (A |^.. n) ^^ ((A |^ k) ^^ A) by FLANG_1:18
.= (A |^.. n) ^^ (A |^ (k + 1)) by FLANG_1:23 ;
hence S1[k + 1] ; ::_thesis: verum
end;
A |^.. (n + 0) = (A |^.. n) ^^ {(<%> E)} by FLANG_1:13
.= (A |^.. n) ^^ (A |^ 0) by FLANG_1:24 ;
then A3: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
hence A |^.. (n + k) = (A |^.. n) ^^ (A |^ k) ; ::_thesis: verum
end;
theorem Th23: :: FLANG_3:23
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A ^^ (A |^.. n) = (A |^.. n) ^^ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds A ^^ (A |^.. n) = (A |^.. n) ^^ A
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A ^^ (A |^.. n) = (A |^.. n) ^^ A
let n be Nat; ::_thesis: A ^^ (A |^.. n) = (A |^.. n) ^^ A
defpred S1[ Nat] means A ^^ (A |^.. $1) = (A |^.. $1) ^^ A;
A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
A ^^ (A |^.. (k + 1)) = A ^^ ((A |^.. k) ^^ A) by Th16
.= ((A |^.. k) ^^ A) ^^ A by A2, FLANG_1:18
.= (A |^.. (k + 1)) ^^ A by Th16 ;
hence S1[k + 1] ; ::_thesis: verum
end;
A ^^ (A |^.. 0) = A ^^ (A *) by Th11
.= (A *) ^^ A by FLANG_1:57
.= (A |^.. 0) ^^ A by Th11 ;
then A3: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
hence A ^^ (A |^.. n) = (A |^.. n) ^^ A ; ::_thesis: verum
end;
theorem Th24: :: FLANG_3:24
for E being set
for A being Subset of (E ^omega)
for k, n being Nat holds (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, n being Nat holds (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k)
let A be Subset of (E ^omega); ::_thesis: for k, n being Nat holds (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k)
let k, n be Nat; ::_thesis: (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k)
defpred S1[ Nat] means (A |^ $1) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ $1);
A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
(A |^ (k + 1)) ^^ (A |^.. n) = ((A |^ k) ^^ A) ^^ (A |^.. n) by FLANG_1:23
.= (A ^^ (A |^ k)) ^^ (A |^.. n) by FLANG_1:32
.= A ^^ ((A |^.. n) ^^ (A |^ k)) by A2, FLANG_1:18
.= (A ^^ (A |^.. n)) ^^ (A |^ k) by FLANG_1:18
.= ((A |^.. n) ^^ A) ^^ (A |^ k) by Th23
.= (A |^.. n) ^^ (A ^^ (A |^ k)) by FLANG_1:18
.= (A |^.. n) ^^ ((A |^ k) ^^ A) by FLANG_1:32
.= (A |^.. n) ^^ (A |^ (k + 1)) by FLANG_1:23 ;
hence S1[k + 1] ; ::_thesis: verum
end;
(A |^ 0) ^^ (A |^.. n) = {(<%> E)} ^^ (A |^.. n) by FLANG_1:24
.= A |^.. n by FLANG_1:13
.= (A |^.. n) ^^ {(<%> E)} by FLANG_1:13
.= (A |^.. n) ^^ (A |^ 0) by FLANG_1:24 ;
then A3: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
hence (A |^ k) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ k) ; ::_thesis: verum
end;
theorem Th25: :: FLANG_3:25
for E being set
for A being Subset of (E ^omega)
for k, l, n being Nat holds (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, l, n being Nat holds (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l))
let A be Subset of (E ^omega); ::_thesis: for k, l, n being Nat holds (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l))
let k, l, n be Nat; ::_thesis: (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l))
defpred S1[ Nat] means (A |^ (k,l)) ^^ (A |^.. $1) = (A |^.. $1) ^^ (A |^ (k,l));
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
(A |^ (k,l)) ^^ (A |^.. (n + 1)) = (A |^ (k,l)) ^^ ((A |^.. n) ^^ A) by Th16
.= ((A |^.. n) ^^ (A |^ (k,l))) ^^ A by A2, FLANG_1:18
.= (A |^.. n) ^^ ((A |^ (k,l)) ^^ A) by FLANG_1:18
.= (A |^.. n) ^^ (A ^^ (A |^ (k,l))) by FLANG_2:36
.= ((A |^.. n) ^^ A) ^^ (A |^ (k,l)) by FLANG_1:18
.= (A |^.. (n + 1)) ^^ (A |^ (k,l)) by Th16 ;
hence S1[n + 1] ; ::_thesis: verum
end;
(A |^ (k,l)) ^^ (A |^.. 0) = (A |^ (k,l)) ^^ (A *) by Th11
.= (A *) ^^ (A |^ (k,l)) by FLANG_2:66
.= (A |^.. 0) ^^ (A |^ (k,l)) by Th11 ;
then A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l)) ; ::_thesis: verum
end;
theorem :: FLANG_3:26
for E being set
for B, A being Subset of (E ^omega)
for n being Nat st <%> E in B holds
( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A )
proof
let E be set ; ::_thesis: for B, A being Subset of (E ^omega)
for n being Nat st <%> E in B holds
( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A )
let B, A be Subset of (E ^omega); ::_thesis: for n being Nat st <%> E in B holds
( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A )
let n be Nat; ::_thesis: ( <%> E in B implies ( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A ) )
assume <%> E in B ; ::_thesis: ( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A )
then <%> E in B |^.. n by Th10;
hence ( A c= A ^^ (B |^.. n) & A c= (B |^.. n) ^^ A ) by FLANG_1:16; ::_thesis: verum
end;
theorem Th27: :: FLANG_3:27
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^.. m)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^.. m)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^.. m) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^.. m)
let m, n be Nat; ::_thesis: (A |^.. m) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^.. m)
thus (A |^.. m) ^^ (A |^.. n) = A |^.. (m + n) by Th18
.= (A |^.. n) ^^ (A |^.. m) by Th18 ; ::_thesis: verum
end;
theorem Th28: :: FLANG_3:28
for E being set
for A, B being Subset of (E ^omega)
for k, n being Nat st A c= B |^.. k & n > 0 holds
A |^ n c= B |^.. k
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for k, n being Nat st A c= B |^.. k & n > 0 holds
A |^ n c= B |^.. k
let A, B be Subset of (E ^omega); ::_thesis: for k, n being Nat st A c= B |^.. k & n > 0 holds
A |^ n c= B |^.. k
let k, n be Nat; ::_thesis: ( A c= B |^.. k & n > 0 implies A |^ n c= B |^.. k )
assume that
A1: A c= B |^.. k and
A2: n > 0 ; ::_thesis: A |^ n c= B |^.. k
defpred S1[ Nat] means ( $1 > 0 implies A |^ $1 c= B |^.. k );
A3: now__::_thesis:_for_m_being_Nat_st_S1[m]_holds_
S1[m_+_1]
let m be Nat; ::_thesis: ( S1[m] implies S1[b1 + 1] )
assume A4: S1[m] ; ::_thesis: S1[b1 + 1]
percases ( m <= 0 or m > 0 ) ;
suppose m <= 0 ; ::_thesis: S1[b1 + 1]
then m = 0 ;
hence S1[m + 1] by A1, FLANG_1:25; ::_thesis: verum
end;
suppose m > 0 ; ::_thesis: S1[b1 + 1]
then (A |^ m) ^^ A c= (B |^.. k) ^^ (B |^.. k) by A1, A4, FLANG_1:17;
then A |^ (m + 1) c= (B |^.. k) ^^ (B |^.. k) by FLANG_1:23;
then A5: A |^ (m + 1) c= B |^.. (k + k) by Th18;
B |^.. (k + k) c= B |^.. k by Th5, NAT_1:11;
hence S1[m + 1] by A5, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
A6: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch_2(A6, A3);
hence A |^ n c= B |^.. k by A2; ::_thesis: verum
end;
theorem Th29: :: FLANG_3:29
for E being set
for A, B being Subset of (E ^omega)
for k, n being Nat st A c= B |^.. k & n > 0 holds
A |^.. n c= B |^.. k
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for k, n being Nat st A c= B |^.. k & n > 0 holds
A |^.. n c= B |^.. k
let A, B be Subset of (E ^omega); ::_thesis: for k, n being Nat st A c= B |^.. k & n > 0 holds
A |^.. n c= B |^.. k
let k, n be Nat; ::_thesis: ( A c= B |^.. k & n > 0 implies A |^.. n c= B |^.. k )
assume that
A1: A c= B |^.. k and
A2: n > 0 ; ::_thesis: A |^.. n c= B |^.. k
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^.. n or x in B |^.. k )
assume x in A |^.. n ; ::_thesis: x in B |^.. k
then consider m being Nat such that
A3: m >= n and
A4: x in A |^ m by Th2;
A |^ m c= B |^.. k by A1, A2, A3, Th28;
hence x in B |^.. k by A4; ::_thesis: verum
end;
theorem Th30: :: FLANG_3:30
for E being set
for A being Subset of (E ^omega) holds (A *) ^^ A = A |^.. 1
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A *) ^^ A = A |^.. 1
let A be Subset of (E ^omega); ::_thesis: (A *) ^^ A = A |^.. 1
A1: now__::_thesis:_for_x_being_set_st_x_in_(A_*)_^^_A_holds_
x_in_A_|^.._1
let x be set ; ::_thesis: ( x in (A *) ^^ A implies x in A |^.. 1 )
assume x in (A *) ^^ A ; ::_thesis: x in A |^.. 1
then consider a1, a2 being Element of E ^omega such that
A2: a1 in A * and
A3: a2 in A and
A4: x = a1 ^ a2 by FLANG_1:def_1;
consider n being Nat such that
A5: a1 in A |^ n by A2, FLANG_1:41;
A6: n + 1 >= 1 by NAT_1:11;
a2 in A |^ 1 by A3, FLANG_1:25;
then a1 ^ a2 in A |^ (n + 1) by A5, FLANG_1:40;
hence x in A |^.. 1 by A4, A6, Th2; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_A_|^.._1_holds_
x_in_(A_*)_^^_A
let x be set ; ::_thesis: ( x in A |^.. 1 implies x in (A *) ^^ A )
assume x in A |^.. 1 ; ::_thesis: x in (A *) ^^ A
then consider n being Nat such that
A7: n >= 1 and
A8: x in A |^ n by Th2;
consider m being Nat such that
A9: m + 1 = n by A7, NAT_1:6;
A |^ (m + 1) c= (A *) ^^ A by FLANG_1:51;
hence x in (A *) ^^ A by A8, A9; ::_thesis: verum
end;
hence (A *) ^^ A = A |^.. 1 by A1, TARSKI:1; ::_thesis: verum
end;
theorem :: FLANG_3:31
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A *) ^^ (A |^ k) = A |^.. k
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A *) ^^ (A |^ k) = A |^.. k
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A *) ^^ (A |^ k) = A |^.. k
let k be Nat; ::_thesis: (A *) ^^ (A |^ k) = A |^.. k
defpred S1[ Nat] means (A *) ^^ (A |^ $1) = A |^.. $1;
A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
(A *) ^^ (A |^ (k + 1)) = (A *) ^^ ((A |^ k) ^^ A) by FLANG_1:23
.= (A |^.. k) ^^ A by A2, FLANG_1:18
.= A |^.. (k + 1) by Th16 ;
hence S1[k + 1] ; ::_thesis: verum
end;
(A *) ^^ (A |^ 0) = (A *) ^^ {(<%> E)} by FLANG_1:24
.= A * by FLANG_1:13
.= A |^.. 0 by Th11 ;
then A3: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A3, A1);
hence (A *) ^^ (A |^ k) = A |^.. k ; ::_thesis: verum
end;
theorem Th32: :: FLANG_3:32
for E being set
for A being Subset of (E ^omega)
for m being Nat holds (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m being Nat holds (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m)
let A be Subset of (E ^omega); ::_thesis: for m being Nat holds (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m)
let m be Nat; ::_thesis: (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m)
thus (A |^.. m) ^^ (A *) = (A |^.. m) ^^ (A |^.. 0) by Th11
.= (A |^.. 0) ^^ (A |^.. m) by Th27
.= (A *) ^^ (A |^.. m) by Th11 ; ::_thesis: verum
end;
theorem Th33: :: FLANG_3:33
for E being set
for A being Subset of (E ^omega)
for k, l, n being Nat st k <= l holds
(A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, l, n being Nat st k <= l holds
(A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
let A be Subset of (E ^omega); ::_thesis: for k, l, n being Nat st k <= l holds
(A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
let k, l, n be Nat; ::_thesis: ( k <= l implies (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k) )
assume A1: k <= l ; ::_thesis: (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k)
A2: A |^.. (n + k) c= (A |^.. n) ^^ (A |^ (k,l))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^.. (n + k) or x in (A |^.. n) ^^ (A |^ (k,l)) )
assume x in A |^.. (n + k) ; ::_thesis: x in (A |^.. n) ^^ (A |^ (k,l))
then consider i being Nat such that
A3: i >= n + k and
A4: x in A |^ i by Th2;
consider m being Nat such that
A5: (n + k) + m = i by A3, NAT_1:10;
i = (n + m) + k by A5;
then x in (A |^ (n + m)) ^^ (A |^ k) by A4, FLANG_1:33;
then A6: ex a, b being Element of E ^omega st
( a in A |^ (n + m) & b in A |^ k & x = a ^ b ) by FLANG_1:def_1;
A7: A |^ (n + m) c= A |^.. n by Th3, NAT_1:11;
A |^ k c= A |^ (k,l) by A1, FLANG_2:20;
hence x in (A |^.. n) ^^ (A |^ (k,l)) by A6, A7, FLANG_1:def_1; ::_thesis: verum
end;
(A |^.. n) ^^ (A |^ (k,l)) c= A |^.. (n + k)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^.. n) ^^ (A |^ (k,l)) or x in A |^.. (n + k) )
assume x in (A |^.. n) ^^ (A |^ (k,l)) ; ::_thesis: x in A |^.. (n + k)
then consider a, b being Element of E ^omega such that
A8: a in A |^.. n and
A9: b in A |^ (k,l) and
A10: x = a ^ b by FLANG_1:def_1;
A |^ (k,l) c= A |^.. k by Th6;
then a ^ b in (A |^.. n) ^^ (A |^.. k) by A8, A9, FLANG_1:def_1;
hence x in A |^.. (n + k) by A10, Th18; ::_thesis: verum
end;
hence (A |^.. n) ^^ (A |^ (k,l)) = A |^.. (n + k) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: FLANG_3:34
for E being set
for A being Subset of (E ^omega)
for k, l being Nat st k <= l holds
(A *) ^^ (A |^ (k,l)) = A |^.. k
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, l being Nat st k <= l holds
(A *) ^^ (A |^ (k,l)) = A |^.. k
let A be Subset of (E ^omega); ::_thesis: for k, l being Nat st k <= l holds
(A *) ^^ (A |^ (k,l)) = A |^.. k
let k, l be Nat; ::_thesis: ( k <= l implies (A *) ^^ (A |^ (k,l)) = A |^.. k )
assume k <= l ; ::_thesis: (A *) ^^ (A |^ (k,l)) = A |^.. k
then (A |^.. 0) ^^ (A |^ (k,l)) = A |^.. (0 + k) by Th33;
hence (A *) ^^ (A |^ (k,l)) = A |^.. k by Th11; ::_thesis: verum
end;
theorem Th35: :: FLANG_3:35
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n)
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n)
let m, n be Nat; ::_thesis: (A |^ m) |^.. n c= A |^.. (m * n)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A |^ m) |^.. n or x in A |^.. (m * n) )
assume x in (A |^ m) |^.. n ; ::_thesis: x in A |^.. (m * n)
then consider k being Nat such that
A1: k >= n and
A2: x in (A |^ m) |^ k by Th2;
A3: m * k >= m * n by A1, XREAL_1:64;
x in A |^ (m * k) by A2, FLANG_1:34;
hence x in A |^.. (m * n) by A3, Th2; ::_thesis: verum
end;
theorem :: FLANG_3:36
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^.. n c= (A |^.. n) |^ m
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ m) |^.. n c= (A |^.. n) |^ m
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ m) |^.. n c= (A |^.. n) |^ m
let m, n be Nat; ::_thesis: (A |^ m) |^.. n c= (A |^.. n) |^ m
percases ( m > 0 or m <= 0 ) ;
supposeA1: m > 0 ; ::_thesis: (A |^ m) |^.. n c= (A |^.. n) |^ m
(A |^ m) |^.. n c= A |^.. (m * n) by Th35;
hence (A |^ m) |^.. n c= (A |^.. n) |^ m by A1, Th19; ::_thesis: verum
end;
suppose m <= 0 ; ::_thesis: (A |^ m) |^.. n c= (A |^.. n) |^ m
then A2: m = 0 ;
then (A |^ m) |^.. n = {(<%> E)} |^.. n by FLANG_1:24
.= {(<%> E)} by Th15
.= (A |^.. n) |^ m by A2, FLANG_1:24 ;
hence (A |^ m) |^.. n c= (A |^.. n) |^ m ; ::_thesis: verum
end;
end;
end;
theorem Th37: :: FLANG_3:37
for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega
for m, n being Nat st a in C |^.. m & b in C |^.. n holds
a ^ b in C |^.. (m + n)
proof
let E be set ; ::_thesis: for C being Subset of (E ^omega)
for a, b being Element of E ^omega
for m, n being Nat st a in C |^.. m & b in C |^.. n holds
a ^ b in C |^.. (m + n)
let C be Subset of (E ^omega); ::_thesis: for a, b being Element of E ^omega
for m, n being Nat st a in C |^.. m & b in C |^.. n holds
a ^ b in C |^.. (m + n)
let a, b be Element of E ^omega ; ::_thesis: for m, n being Nat st a in C |^.. m & b in C |^.. n holds
a ^ b in C |^.. (m + n)
let m, n be Nat; ::_thesis: ( a in C |^.. m & b in C |^.. n implies a ^ b in C |^.. (m + n) )
assume that
A1: a in C |^.. m and
A2: b in C |^.. n ; ::_thesis: a ^ b in C |^.. (m + n)
A3: (C |^.. m) ^^ (C |^.. n) c= C |^.. (m + n) by Th21;
a ^ b in (C |^.. m) ^^ (C |^.. n) by A1, A2, FLANG_1:def_1;
hence a ^ b in C |^.. (m + n) by A3; ::_thesis: verum
end;
theorem Th38: :: FLANG_3:38
for x, E being set
for A being Subset of (E ^omega)
for k being Nat st A |^.. k = {x} holds
x = <%> E
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat st A |^.. k = {x} holds
x = <%> E
let A be Subset of (E ^omega); ::_thesis: for k being Nat st A |^.. k = {x} holds
x = <%> E
let k be Nat; ::_thesis: ( A |^.. k = {x} implies x = <%> E )
assume that
A1: A |^.. k = {x} and
A2: x <> <%> E ; ::_thesis: contradiction
reconsider a = x as Element of E ^omega by A1, ZFMISC_1:31;
x in A |^.. k by A1, ZFMISC_1:31;
then A3: a ^ a in A |^.. (k + k) by Th37;
A4: A |^.. (k + k) c= A |^.. k by Th5, NAT_1:11;
a ^ a <> x by A2, FLANG_1:11;
hence contradiction by A1, A4, A3, TARSKI:def_1; ::_thesis: verum
end;
theorem :: FLANG_3:39
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B * holds
A |^.. n c= B *
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for n being Nat st A c= B * holds
A |^.. n c= B *
let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B * holds
A |^.. n c= B *
let n be Nat; ::_thesis: ( A c= B * implies A |^.. n c= B * )
assume A1: A c= B * ; ::_thesis: A |^.. n c= B *
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^.. n or x in B * )
assume x in A |^.. n ; ::_thesis: x in B *
then consider k being Nat such that
k >= n and
A2: x in A |^ k by Th2;
A |^ k c= B * by A1, FLANG_1:59;
hence x in B * by A2; ::_thesis: verum
end;
theorem Th40: :: FLANG_3:40
for E being set
for A being Subset of (E ^omega)
for k being Nat holds
( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds
( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds
( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )
let k be Nat; ::_thesis: ( A ? c= A |^.. k iff ( k = 0 or <%> E in A ) )
thus ( not A ? c= A |^.. k or k = 0 or <%> E in A ) ::_thesis: ( ( k = 0 or <%> E in A ) implies A ? c= A |^.. k )
proof
A1: <%> E in A ? by FLANG_2:78;
assume A ? c= A |^.. k ; ::_thesis: ( k = 0 or <%> E in A )
hence ( k = 0 or <%> E in A ) by A1, Th10; ::_thesis: verum
end;
assume ( k = 0 or <%> E in A ) ; ::_thesis: A ? c= A |^.. k
then A |^.. k = A * by Th11;
hence A ? c= A |^.. k by FLANG_2:86; ::_thesis: verum
end;
theorem Th41: :: FLANG_3:41
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^.. k) ^^ (A ?) = A |^.. k
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A |^.. k) ^^ (A ?) = A |^.. k
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A |^.. k) ^^ (A ?) = A |^.. k
let k be Nat; ::_thesis: (A |^.. k) ^^ (A ?) = A |^.. k
thus (A |^.. k) ^^ (A ?) = (A |^.. k) ^^ (A |^ (0,1)) by FLANG_2:79
.= A |^.. (k + 0) by Th33
.= A |^.. k ; ::_thesis: verum
end;
theorem :: FLANG_3:42
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^.. k) ^^ (A ?) = (A ?) ^^ (A |^.. k)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A |^.. k) ^^ (A ?) = (A ?) ^^ (A |^.. k)
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A |^.. k) ^^ (A ?) = (A ?) ^^ (A |^.. k)
let k be Nat; ::_thesis: (A |^.. k) ^^ (A ?) = (A ?) ^^ (A |^.. k)
thus (A |^.. k) ^^ (A ?) = (A |^.. k) ^^ (A |^ (0,1)) by FLANG_2:79
.= (A |^ (0,1)) ^^ (A |^.. k) by Th25
.= (A ?) ^^ (A |^.. k) by FLANG_2:79 ; ::_thesis: verum
end;
theorem :: FLANG_3:43
for E being set
for B, A being Subset of (E ^omega)
for k being Nat st B c= A * holds
( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )
proof
let E be set ; ::_thesis: for B, A being Subset of (E ^omega)
for k being Nat st B c= A * holds
( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )
let B, A be Subset of (E ^omega); ::_thesis: for k being Nat st B c= A * holds
( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )
let k be Nat; ::_thesis: ( B c= A * implies ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k ) )
assume A1: B c= A * ; ::_thesis: ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )
then B ^^ (A |^.. k) c= (A *) ^^ (A |^.. k) by FLANG_1:17;
then A2: B ^^ (A |^.. k) c= (A |^.. k) ^^ (A *) by Th32;
(A |^.. k) ^^ B c= (A |^.. k) ^^ (A *) by A1, FLANG_1:17;
hence ( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k ) by A2, Th17; ::_thesis: verum
end;
theorem Th44: :: FLANG_3:44
for E being set
for A, B being Subset of (E ^omega)
for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)
let A, B be Subset of (E ^omega); ::_thesis: for k being Nat holds (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)
let k be Nat; ::_thesis: (A /\ B) |^.. k c= (A |^.. k) /\ (B |^.. k)
thus for x being set st x in (A /\ B) |^.. k holds
x in (A |^.. k) /\ (B |^.. k) :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in (A /\ B) |^.. k implies x in (A |^.. k) /\ (B |^.. k) )
assume x in (A /\ B) |^.. k ; ::_thesis: x in (A |^.. k) /\ (B |^.. k)
then consider m being Nat such that
A1: k <= m and
A2: x in (A /\ B) |^ m by Th2;
A3: B |^ m c= B |^.. k by A1, Th3;
(A /\ B) |^ m c= (A |^ m) /\ (B |^ m) by FLANG_1:39;
then A4: x in (A |^ m) /\ (B |^ m) by A2;
A |^ m c= A |^.. k by A1, Th3;
then (A |^ m) /\ (B |^ m) c= (A |^.. k) /\ (B |^.. k) by A3, XBOOLE_1:27;
hence x in (A |^.. k) /\ (B |^.. k) by A4; ::_thesis: verum
end;
end;
theorem Th45: :: FLANG_3:45
for E being set
for A, B being Subset of (E ^omega)
for k being Nat holds (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for k being Nat holds (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k
let A, B be Subset of (E ^omega); ::_thesis: for k being Nat holds (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k
let k be Nat; ::_thesis: (A |^.. k) \/ (B |^.. k) c= (A \/ B) |^.. k
thus for x being set st x in (A |^.. k) \/ (B |^.. k) holds
x in (A \/ B) |^.. k :: according to TARSKI:def_3 ::_thesis: verum
proof
let x be set ; ::_thesis: ( x in (A |^.. k) \/ (B |^.. k) implies x in (A \/ B) |^.. k )
assume A1: x in (A |^.. k) \/ (B |^.. k) ; ::_thesis: x in (A \/ B) |^.. k
percases ( x in A |^.. k or x in B |^.. k ) by A1, XBOOLE_0:def_3;
suppose x in A |^.. k ; ::_thesis: x in (A \/ B) |^.. k
then consider m being Nat such that
A2: k <= m and
A3: x in A |^ m by Th2;
A4: (A |^ m) \/ (B |^ m) c= (A \/ B) |^ m by FLANG_1:38;
A |^ m c= (A |^ m) \/ (B |^ m) by XBOOLE_1:7;
then A |^ m c= (A \/ B) |^ m by A4, XBOOLE_1:1;
then A5: x in (A \/ B) |^ m by A3;
(A \/ B) |^ m c= (A \/ B) |^.. k by A2, Th3;
hence x in (A \/ B) |^.. k by A5; ::_thesis: verum
end;
suppose x in B |^.. k ; ::_thesis: x in (A \/ B) |^.. k
then consider m being Nat such that
A6: k <= m and
A7: x in B |^ m by Th2;
A8: (A |^ m) \/ (B |^ m) c= (A \/ B) |^ m by FLANG_1:38;
B |^ m c= (A |^ m) \/ (B |^ m) by XBOOLE_1:7;
then B |^ m c= (A \/ B) |^ m by A8, XBOOLE_1:1;
then A9: x in (A \/ B) |^ m by A7;
(A \/ B) |^ m c= (A \/ B) |^.. k by A6, Th3;
hence x in (A \/ B) |^.. k by A9; ::_thesis: verum
end;
end;
end;
end;
theorem Th46: :: FLANG_3:46
for x, E being set
for A being Subset of (E ^omega)
for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds
( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )
let k be Nat; ::_thesis: ( <%x%> in A |^.. k iff ( <%x%> in A & ( <%> E in A or k <= 1 ) ) )
thus ( <%x%> in A |^.. k implies ( <%x%> in A & ( <%> E in A or k <= 1 ) ) ) ::_thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) implies <%x%> in A |^.. k )
proof
assume <%x%> in A |^.. k ; ::_thesis: ( <%x%> in A & ( <%> E in A or k <= 1 ) )
then ex m being Nat st
( k <= m & <%x%> in A |^ m ) by Th2;
hence ( <%x%> in A & ( <%> E in A or k <= 1 ) ) by FLANG_2:9; ::_thesis: verum
end;
assume that
A1: <%x%> in A and
A2: ( <%> E in A or k <= 1 ) ; ::_thesis: <%x%> in A |^.. k
percases ( ( <%> E in A & k > 1 ) or k = 0 or k = 1 ) by A2, NAT_1:25;
suppose ( <%> E in A & k > 1 ) ; ::_thesis: <%x%> in A |^.. k
then <%x%> in A |^ k by A1, FLANG_2:9;
hence <%x%> in A |^.. k by Th2; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: <%x%> in A |^.. k
then A |^.. k = A * by Th11;
hence <%x%> in A |^.. k by A1, FLANG_1:72; ::_thesis: verum
end;
suppose k = 1 ; ::_thesis: <%x%> in A |^.. k
then <%x%> in A |^ k by A1, FLANG_1:25;
hence <%x%> in A |^.. k by Th2; ::_thesis: verum
end;
end;
end;
theorem Th47: :: FLANG_3:47
for E being set
for A, B being Subset of (E ^omega)
for k being Nat st A c= B |^.. k holds
B |^.. k = (B \/ A) |^.. k
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for k being Nat st A c= B |^.. k holds
B |^.. k = (B \/ A) |^.. k
let A, B be Subset of (E ^omega); ::_thesis: for k being Nat st A c= B |^.. k holds
B |^.. k = (B \/ A) |^.. k
let k be Nat; ::_thesis: ( A c= B |^.. k implies B |^.. k = (B \/ A) |^.. k )
defpred S1[ Nat] means ( $1 >= k implies (B \/ A) |^ $1 c= B |^.. k );
B |^ 1 c= B |^.. 1 by Th3;
then A1: B c= B |^.. 1 by FLANG_1:25;
assume A2: A c= B |^.. k ; ::_thesis: B |^.. k = (B \/ A) |^.. k
A3: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A4: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_(_n_+_1_>=_k_implies_(B_\/_A)_|^_(n_+_1)_c=_B_|^.._k_)
assume A5: n + 1 >= k ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k
percases ( n + 1 = k or n >= k ) by A5, NAT_1:8;
supposeA6: n + 1 = k ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k
percases ( k = 0 or k > 0 ) ;
suppose k = 0 ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k
hence (B \/ A) |^ (n + 1) c= B |^.. k by A6; ::_thesis: verum
end;
supposeA7: k > 0 ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k
then k >= 0 + 1 by NAT_1:13;
then B |^.. k c= B |^.. 1 by Th5;
then A c= B |^.. 1 by A2, XBOOLE_1:1;
then B \/ A c= B |^.. 1 by A1, XBOOLE_1:8;
then A8: (B \/ A) |^ k c= (B |^.. 1) |^ k by FLANG_1:37;
(B |^.. 1) |^ k c= B |^.. (1 * k) by A7, Th19;
hence (B \/ A) |^ (n + 1) c= B |^.. k by A6, A8, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
supposeA9: n >= k ; ::_thesis: (B \/ A) |^ (n + 1) c= B |^.. k
A10: B |^.. (k + k) c= B |^.. k by Th5, NAT_1:11;
((B \/ A) |^ n) ^^ A c= B |^.. (k + k) by A2, A4, A9, Th21;
then A11: ((B \/ A) |^ n) ^^ A c= B |^.. k by A10, XBOOLE_1:1;
A12: B |^.. (k + 1) c= B |^.. k by Th5, NAT_1:11;
((B \/ A) |^ n) ^^ B c= B |^.. (k + 1) by A1, A4, A9, Th21;
then A13: ((B \/ A) |^ n) ^^ B c= B |^.. k by A12, XBOOLE_1:1;
(B \/ A) |^ (n + 1) = ((B \/ A) |^ n) ^^ (B \/ A) by FLANG_1:23
.= (((B \/ A) |^ n) ^^ B) \/ (((B \/ A) |^ n) ^^ A) by FLANG_1:20 ;
hence (B \/ A) |^ (n + 1) c= B |^.. k by A13, A11, XBOOLE_1:8; ::_thesis: verum
end;
end;
end;
hence S1[n + 1] ; ::_thesis: verum
end;
A14: S1[ 0 ]
proof
assume 0 >= k ; ::_thesis: (B \/ A) |^ 0 c= B |^.. k
then k = 0 ;
then A15: B |^.. k = B * by Th11;
A16: <%> E in B * by FLANG_1:48;
(B \/ A) |^ 0 = {(<%> E)} by FLANG_1:24;
hence (B \/ A) |^ 0 c= B |^.. k by A15, A16, ZFMISC_1:31; ::_thesis: verum
end;
A17: for n being Nat holds S1[n] from NAT_1:sch_2(A14, A3);
A18: (B \/ A) |^.. k c= B |^.. k
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (B \/ A) |^.. k or x in B |^.. k )
assume x in (B \/ A) |^.. k ; ::_thesis: x in B |^.. k
then consider n being Nat such that
A19: n >= k and
A20: x in (B \/ A) |^ n by Th2;
(B \/ A) |^ n c= B |^.. k by A17, A19;
hence x in B |^.. k by A20; ::_thesis: verum
end;
B |^.. k c= (B \/ A) |^.. k by Th13, XBOOLE_1:7;
hence B |^.. k = (B \/ A) |^.. k by A18, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
definition
let E be set ;
let A be Subset of (E ^omega);
funcA + -> Subset of (E ^omega) equals :: FLANG_3:def 2
union { B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 & B = A |^ n ) } ;
coherence
union { B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 & B = A |^ n ) } is Subset of (E ^omega)
proof
defpred S1[ set ] means ex n being Nat st
( n > 0 & $1 = A |^ n );
reconsider M = { B where B is Subset of (E ^omega) : S1[B] } as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
union M is Subset of (E ^omega) ;
hence union { B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 & B = A |^ n ) } is Subset of (E ^omega) ; ::_thesis: verum
end;
end;
:: deftheorem defines + FLANG_3:def_2_:_
for E being set
for A being Subset of (E ^omega) holds A + = union { B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 & B = A |^ n ) } ;
theorem Th48: :: FLANG_3:48
for E, x being set
for A being Subset of (E ^omega) holds
( x in A + iff ex n being Nat st
( n > 0 & x in A |^ n ) )
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega) holds
( x in A + iff ex n being Nat st
( n > 0 & x in A |^ n ) )
let A be Subset of (E ^omega); ::_thesis: ( x in A + iff ex n being Nat st
( n > 0 & x in A |^ n ) )
thus ( x in A + implies ex n being Nat st
( n > 0 & x in A |^ n ) ) ::_thesis: ( ex n being Nat st
( n > 0 & x in A |^ n ) implies x in A + )
proof
defpred S1[ set ] means ex n being Nat st
( n > 0 & $1 = A |^ n );
assume x in A + ; ::_thesis: ex n being Nat st
( n > 0 & x in A |^ n )
then consider X being set such that
A1: x in X and
A2: X in { B where B is Subset of (E ^omega) : ex n being Nat st
( n > 0 & B = A |^ n ) } by TARSKI:def_4;
A3: X in { B where B is Subset of (E ^omega) : S1[B] } by A2;
S1[X] from CARD_FIL:sch_1(A3);
hence ex n being Nat st
( n > 0 & x in A |^ n ) by A1; ::_thesis: verum
end;
given n being Nat such that A4: n > 0 and
A5: x in A |^ n ; ::_thesis: x in A +
defpred S1[ set ] means ex n being Nat st
( n > 0 & $1 = A |^ n );
consider B being Subset of (E ^omega) such that
A6: x in B and
A7: S1[B] by A4, A5;
reconsider A = { C where C is Subset of (E ^omega) : S1[C] } as Subset-Family of (E ^omega) from DOMAIN_1:sch_7();
B in A by A7;
hence x in A + by A6, TARSKI:def_4; ::_thesis: verum
end;
theorem Th49: :: FLANG_3:49
for E being set
for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
A |^ n c= A +
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
A |^ n c= A +
let A be Subset of (E ^omega); ::_thesis: for n being Nat st n > 0 holds
A |^ n c= A +
let n be Nat; ::_thesis: ( n > 0 implies A |^ n c= A + )
assume n > 0 ; ::_thesis: A |^ n c= A +
then for x being set st x in A |^ n holds
x in A + by Th48;
hence A |^ n c= A + by TARSKI:def_3; ::_thesis: verum
end;
theorem Th50: :: FLANG_3:50
for E being set
for A being Subset of (E ^omega) holds A + = A |^.. 1
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A + = A |^.. 1
let A be Subset of (E ^omega); ::_thesis: A + = A |^.. 1
A1: now__::_thesis:_for_x_being_set_st_x_in_A_+_holds_
x_in_A_|^.._1
let x be set ; ::_thesis: ( x in A + implies x in A |^.. 1 )
assume x in A + ; ::_thesis: x in A |^.. 1
then consider k being Nat such that
A2: 0 < k and
A3: x in A |^ k by Th48;
0 + 1 <= k by A2, NAT_1:13;
hence x in A |^.. 1 by A3, Th2; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_A_|^.._1_holds_
x_in_A_+
let x be set ; ::_thesis: ( x in A |^.. 1 implies x in A + )
assume x in A |^.. 1 ; ::_thesis: x in A +
then ex k being Nat st
( 1 <= k & x in A |^ k ) by Th2;
hence x in A + by Th48; ::_thesis: verum
end;
hence A + = A |^.. 1 by A1, TARSKI:1; ::_thesis: verum
end;
theorem :: FLANG_3:51
for E being set
for A being Subset of (E ^omega) holds
( A + = {} iff A = {} )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( A + = {} iff A = {} )
let A be Subset of (E ^omega); ::_thesis: ( A + = {} iff A = {} )
A + = A |^.. 1 by Th50;
hence ( A + = {} iff A = {} ) by Th4; ::_thesis: verum
end;
theorem Th52: :: FLANG_3:52
for E being set
for A being Subset of (E ^omega) holds A + = (A *) ^^ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A + = (A *) ^^ A
let A be Subset of (E ^omega); ::_thesis: A + = (A *) ^^ A
(A *) ^^ A = A |^.. 1 by Th30;
hence A + = (A *) ^^ A by Th50; ::_thesis: verum
end;
theorem Th53: :: FLANG_3:53
for E being set
for A being Subset of (E ^omega) holds A * = {(<%> E)} \/ (A +)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A * = {(<%> E)} \/ (A +)
let A be Subset of (E ^omega); ::_thesis: A * = {(<%> E)} \/ (A +)
thus A * = {(<%> E)} \/ ((A *) ^^ A) by FLANG_1:56
.= {(<%> E)} \/ (A +) by Th52 ; ::_thesis: verum
end;
theorem :: FLANG_3:54
for E being set
for A being Subset of (E ^omega)
for n being Nat holds A + = (A |^ (1,n)) \/ (A |^.. (n + 1))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat holds A + = (A |^ (1,n)) \/ (A |^.. (n + 1))
let A be Subset of (E ^omega); ::_thesis: for n being Nat holds A + = (A |^ (1,n)) \/ (A |^.. (n + 1))
let n be Nat; ::_thesis: A + = (A |^ (1,n)) \/ (A |^.. (n + 1))
A1: 0 + 1 <= n + 1 by XREAL_1:7;
thus A + = A |^.. 1 by Th50
.= (A |^ (1,n)) \/ (A |^.. (n + 1)) by A1, Th7 ; ::_thesis: verum
end;
theorem Th55: :: FLANG_3:55
for E being set
for A being Subset of (E ^omega) holds A + c= A *
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A + c= A *
let A be Subset of (E ^omega); ::_thesis: A + c= A *
A |^.. 1 c= A * by Th9;
hence A + c= A * by Th50; ::_thesis: verum
end;
theorem Th56: :: FLANG_3:56
for E being set
for A being Subset of (E ^omega) holds
( <%> E in A + iff <%> E in A )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( <%> E in A + iff <%> E in A )
let A be Subset of (E ^omega); ::_thesis: ( <%> E in A + iff <%> E in A )
A + = A |^.. 1 by Th50;
hence ( <%> E in A + iff <%> E in A ) by Th10; ::_thesis: verum
end;
theorem Th57: :: FLANG_3:57
for E being set
for A being Subset of (E ^omega) holds
( A + = A * iff <%> E in A )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( A + = A * iff <%> E in A )
let A be Subset of (E ^omega); ::_thesis: ( A + = A * iff <%> E in A )
thus ( A + = A * implies <%> E in A ) ::_thesis: ( <%> E in A implies A + = A * )
proof
assume A + = A * ; ::_thesis: <%> E in A
then <%> E in A + by FLANG_1:48;
hence <%> E in A by Th56; ::_thesis: verum
end;
assume <%> E in A ; ::_thesis: A + = A *
then A * = (A *) ^^ A by FLANG_1:54;
hence A + = A * by Th52; ::_thesis: verum
end;
theorem Th58: :: FLANG_3:58
for E being set
for A, B being Subset of (E ^omega) st A c= B holds
A + c= B +
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B holds
A + c= B +
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B implies A + c= B + )
assume A c= B ; ::_thesis: A + c= B +
then A |^.. 1 c= B |^.. 1 by Th13;
then A + c= B |^.. 1 by Th50;
hence A + c= B + by Th50; ::_thesis: verum
end;
theorem Th59: :: FLANG_3:59
for E being set
for A being Subset of (E ^omega) holds A c= A +
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A c= A +
let A be Subset of (E ^omega); ::_thesis: A c= A +
A |^ 1 c= A + by Th49;
hence A c= A + by FLANG_1:25; ::_thesis: verum
end;
theorem Th60: :: FLANG_3:60
for E being set
for A being Subset of (E ^omega) holds
( (A *) + = A * & (A +) * = A * )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( (A *) + = A * & (A +) * = A * )
let A be Subset of (E ^omega); ::_thesis: ( (A *) + = A * & (A +) * = A * )
A1: A * c= (A +) * by Th59, FLANG_1:61;
now__::_thesis:_for_x_being_set_st_x_in_(A_*)_+_holds_
x_in_A_*
let x be set ; ::_thesis: ( x in (A *) + implies x in A * )
assume x in (A *) + ; ::_thesis: x in A *
then consider k being Nat such that
0 < k and
A2: x in (A *) |^ k by Th48;
(A *) |^ k c= A * by FLANG_1:65;
hence x in A * by A2; ::_thesis: verum
end;
then A3: (A *) + c= A * by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_(A_+)_*_holds_
x_in_A_*
let x be set ; ::_thesis: ( x in (A +) * implies x in A * )
assume x in (A +) * ; ::_thesis: x in A *
then consider k being Nat such that
A4: x in (A +) |^ k by FLANG_1:41;
(A +) |^ k c= A * by Th55, FLANG_1:59;
hence x in A * by A4; ::_thesis: verum
end;
then A5: (A +) * c= A * by TARSKI:def_3;
A * c= (A *) + by Th59;
hence ( (A *) + = A * & (A +) * = A * ) by A1, A3, A5, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th61: :: FLANG_3:61
for E being set
for A, B being Subset of (E ^omega) st A c= B * holds
A + c= B *
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B * holds
A + c= B *
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B * implies A + c= B * )
assume A c= B * ; ::_thesis: A + c= B *
then A + c= (B *) + by Th58;
hence A + c= B * by Th60; ::_thesis: verum
end;
theorem :: FLANG_3:62
for E being set
for A being Subset of (E ^omega) holds (A +) + = A +
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A +) + = A +
let A be Subset of (E ^omega); ::_thesis: (A +) + = A +
now__::_thesis:_for_x_being_set_st_x_in_(A_+)_+_holds_
x_in_A_+
let x be set ; ::_thesis: ( x in (A +) + implies b1 in A + )
assume A1: x in (A +) + ; ::_thesis: b1 in A +
percases ( x = <%> E or x <> <%> E ) ;
suppose x = <%> E ; ::_thesis: b1 in A +
hence x in A + by A1, Th56; ::_thesis: verum
end;
supposeA2: x <> <%> E ; ::_thesis: b1 in A +
(A +) + c= A * by Th55, Th61;
then x in A * by A1;
then A3: x in (A +) \/ {(<%> E)} by Th53;
not x in {(<%> E)} by A2, TARSKI:def_1;
hence x in A + by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
then A4: (A +) + c= A + by TARSKI:def_3;
A + c= (A +) + by Th59;
hence (A +) + = A + by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: FLANG_3:63
for x, E being set
for A being Subset of (E ^omega) st x in A & x <> <%> E holds
A + <> {(<%> E)}
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega) st x in A & x <> <%> E holds
A + <> {(<%> E)}
let A be Subset of (E ^omega); ::_thesis: ( x in A & x <> <%> E implies A + <> {(<%> E)} )
assume that
A1: x in A and
A2: x <> <%> E ; ::_thesis: A + <> {(<%> E)}
A + = A |^.. 1 by Th50;
hence A + <> {(<%> E)} by A1, A2, Th14; ::_thesis: verum
end;
theorem :: FLANG_3:64
for E being set
for A being Subset of (E ^omega) holds
( A + = {(<%> E)} iff A = {(<%> E)} )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( A + = {(<%> E)} iff A = {(<%> E)} )
let A be Subset of (E ^omega); ::_thesis: ( A + = {(<%> E)} iff A = {(<%> E)} )
A + = A |^.. 1 by Th50;
hence ( A + = {(<%> E)} iff A = {(<%> E)} ) by Th15; ::_thesis: verum
end;
theorem :: FLANG_3:65
for E being set
for A being Subset of (E ^omega) holds
( (A +) ? = A * & (A ?) + = A * )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( (A +) ? = A * & (A ?) + = A * )
let A be Subset of (E ^omega); ::_thesis: ( (A +) ? = A * & (A ?) + = A * )
thus (A +) ? = {(<%> E)} \/ (A +) by FLANG_2:76
.= A * by Th53 ; ::_thesis: (A ?) + = A *
<%> E in A ? by FLANG_2:78;
then (A ?) + = (A ?) * by Th57;
hence (A ?) + = A * by FLANG_2:85; ::_thesis: verum
end;
theorem Th66: :: FLANG_3:66
for E being set
for C being Subset of (E ^omega)
for a, b being Element of E ^omega st a in C + & b in C + holds
a ^ b in C +
proof
let E be set ; ::_thesis: for C being Subset of (E ^omega)
for a, b being Element of E ^omega st a in C + & b in C + holds
a ^ b in C +
let C be Subset of (E ^omega); ::_thesis: for a, b being Element of E ^omega st a in C + & b in C + holds
a ^ b in C +
let a, b be Element of E ^omega ; ::_thesis: ( a in C + & b in C + implies a ^ b in C + )
assume that
A1: a in C + and
A2: b in C + ; ::_thesis: a ^ b in C +
consider l being Nat such that
l > 0 and
A3: b in C |^ l by A2, Th48;
consider k being Nat such that
A4: k > 0 and
A5: a in C |^ k by A1, Th48;
a ^ b in C |^ (k + l) by A5, A3, FLANG_1:40;
hence a ^ b in C + by A4, Th48; ::_thesis: verum
end;
theorem :: FLANG_3:67
for E being set
for A, C, B being Subset of (E ^omega) st A c= C + & B c= C + holds
A ^^ B c= C +
proof
let E be set ; ::_thesis: for A, C, B being Subset of (E ^omega) st A c= C + & B c= C + holds
A ^^ B c= C +
let A, C, B be Subset of (E ^omega); ::_thesis: ( A c= C + & B c= C + implies A ^^ B c= C + )
assume that
A1: A c= C + and
A2: B c= C + ; ::_thesis: A ^^ B c= C +
now__::_thesis:_for_x_being_set_st_x_in_A_^^_B_holds_
x_in_C_+
let x be set ; ::_thesis: ( x in A ^^ B implies x in C + )
assume x in A ^^ B ; ::_thesis: x in C +
then ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by FLANG_1:def_1;
hence x in C + by A1, A2, Th66; ::_thesis: verum
end;
hence A ^^ B c= C + by TARSKI:def_3; ::_thesis: verum
end;
theorem :: FLANG_3:68
for E being set
for A being Subset of (E ^omega) holds A ^^ A c= A +
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ^^ A c= A +
let A be Subset of (E ^omega); ::_thesis: A ^^ A c= A +
A ^^ A = A |^ 2 by FLANG_1:26;
hence A ^^ A c= A + by Th49; ::_thesis: verum
end;
theorem :: FLANG_3:69
for x, E being set
for A being Subset of (E ^omega) st A + = {x} holds
x = <%> E
proof
let x, E be set ; ::_thesis: for A being Subset of (E ^omega) st A + = {x} holds
x = <%> E
let A be Subset of (E ^omega); ::_thesis: ( A + = {x} implies x = <%> E )
assume that
A1: A + = {x} and
A2: x <> <%> E ; ::_thesis: contradiction
A |^.. 1 = {x} by A1, Th50;
hence contradiction by A2, Th38; ::_thesis: verum
end;
theorem :: FLANG_3:70
for E being set
for A being Subset of (E ^omega) holds A ^^ (A +) = (A +) ^^ A
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds A ^^ (A +) = (A +) ^^ A
let A be Subset of (E ^omega); ::_thesis: A ^^ (A +) = (A +) ^^ A
thus A ^^ (A +) = A ^^ (A |^.. 1) by Th50
.= (A |^.. 1) ^^ A by Th23
.= (A +) ^^ A by Th50 ; ::_thesis: verum
end;
theorem :: FLANG_3:71
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^ k) ^^ (A +) = (A +) ^^ (A |^ k)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A |^ k) ^^ (A +) = (A +) ^^ (A |^ k)
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A |^ k) ^^ (A +) = (A +) ^^ (A |^ k)
let k be Nat; ::_thesis: (A |^ k) ^^ (A +) = (A +) ^^ (A |^ k)
thus (A |^ k) ^^ (A +) = (A |^ k) ^^ (A |^.. 1) by Th50
.= (A |^.. 1) ^^ (A |^ k) by Th24
.= (A +) ^^ (A |^ k) by Th50 ; ::_thesis: verum
end;
theorem Th72: :: FLANG_3:72
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ^^ (A +) = (A +) ^^ (A |^ (m,n))
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ^^ (A +) = (A +) ^^ (A |^ (m,n))
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A |^ (m,n)) ^^ (A +) = (A +) ^^ (A |^ (m,n))
let m, n be Nat; ::_thesis: (A |^ (m,n)) ^^ (A +) = (A +) ^^ (A |^ (m,n))
thus (A |^ (m,n)) ^^ (A +) = (A |^ (m,n)) ^^ (A |^.. 1) by Th50
.= (A |^.. 1) ^^ (A |^ (m,n)) by Th25
.= (A +) ^^ (A |^ (m,n)) by Th50 ; ::_thesis: verum
end;
theorem :: FLANG_3:73
for E being set
for B, A being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ (B +) & A c= (B +) ^^ A )
proof
let E be set ; ::_thesis: for B, A being Subset of (E ^omega) st <%> E in B holds
( A c= A ^^ (B +) & A c= (B +) ^^ A )
let B, A be Subset of (E ^omega); ::_thesis: ( <%> E in B implies ( A c= A ^^ (B +) & A c= (B +) ^^ A ) )
assume <%> E in B ; ::_thesis: ( A c= A ^^ (B +) & A c= (B +) ^^ A )
then B + = B * by Th57;
hence ( A c= A ^^ (B +) & A c= (B +) ^^ A ) by FLANG_2:18; ::_thesis: verum
end;
theorem :: FLANG_3:74
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A +) = A |^.. 2
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A +) ^^ (A +) = A |^.. 2
let A be Subset of (E ^omega); ::_thesis: (A +) ^^ (A +) = A |^.. 2
thus (A +) ^^ (A +) = (A |^.. 1) ^^ (A +) by Th50
.= (A |^.. 1) ^^ (A |^.. 1) by Th50
.= A |^.. (1 + 1) by Th18
.= A |^.. 2 ; ::_thesis: verum
end;
theorem Th75: :: FLANG_3:75
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A +) ^^ (A |^ k) = A |^.. (k + 1)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A +) ^^ (A |^ k) = A |^.. (k + 1)
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A +) ^^ (A |^ k) = A |^.. (k + 1)
let k be Nat; ::_thesis: (A +) ^^ (A |^ k) = A |^.. (k + 1)
thus (A +) ^^ (A |^ k) = (A |^.. 1) ^^ (A |^ k) by Th50
.= A |^.. (k + 1) by Th22 ; ::_thesis: verum
end;
theorem :: FLANG_3:76
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ A = A |^.. 2
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A +) ^^ A = A |^.. 2
let A be Subset of (E ^omega); ::_thesis: (A +) ^^ A = A |^.. 2
(A +) ^^ A = (A +) ^^ (A |^ 1) by FLANG_1:25
.= A |^.. (1 + 1) by Th75 ;
hence (A +) ^^ A = A |^.. 2 ; ::_thesis: verum
end;
theorem :: FLANG_3:77
for E being set
for A being Subset of (E ^omega)
for k, l being Nat st k <= l holds
(A +) ^^ (A |^ (k,l)) = A |^.. (k + 1)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k, l being Nat st k <= l holds
(A +) ^^ (A |^ (k,l)) = A |^.. (k + 1)
let A be Subset of (E ^omega); ::_thesis: for k, l being Nat st k <= l holds
(A +) ^^ (A |^ (k,l)) = A |^.. (k + 1)
let k, l be Nat; ::_thesis: ( k <= l implies (A +) ^^ (A |^ (k,l)) = A |^.. (k + 1) )
assume k <= l ; ::_thesis: (A +) ^^ (A |^ (k,l)) = A |^.. (k + 1)
then (A |^.. 1) ^^ (A |^ (k,l)) = A |^.. (1 + k) by Th33;
hence (A +) ^^ (A |^ (k,l)) = A |^.. (k + 1) by Th50; ::_thesis: verum
end;
theorem :: FLANG_3:78
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B + & n > 0 holds
A |^ n c= B +
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for n being Nat st A c= B + & n > 0 holds
A |^ n c= B +
let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B + & n > 0 holds
A |^ n c= B +
let n be Nat; ::_thesis: ( A c= B + & n > 0 implies A |^ n c= B + )
assume that
A1: A c= B + and
A2: n > 0 ; ::_thesis: A |^ n c= B +
A c= B |^.. 1 by A1, Th50;
then A |^ n c= B |^.. 1 by A2, Th28;
hence A |^ n c= B + by Th50; ::_thesis: verum
end;
theorem :: FLANG_3:79
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A ?) = (A ?) ^^ (A +)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A +) ^^ (A ?) = (A ?) ^^ (A +)
let A be Subset of (E ^omega); ::_thesis: (A +) ^^ (A ?) = (A ?) ^^ (A +)
thus (A +) ^^ (A ?) = (A +) ^^ (A |^ (0,1)) by FLANG_2:79
.= (A |^ (0,1)) ^^ (A +) by Th72
.= (A ?) ^^ (A +) by FLANG_2:79 ; ::_thesis: verum
end;
theorem :: FLANG_3:80
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A ?) = A +
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A +) ^^ (A ?) = A +
let A be Subset of (E ^omega); ::_thesis: (A +) ^^ (A ?) = A +
thus (A +) ^^ (A ?) = (A |^.. 1) ^^ (A ?) by Th50
.= A |^.. 1 by Th41
.= A + by Th50 ; ::_thesis: verum
end;
theorem :: FLANG_3:81
for E being set
for A being Subset of (E ^omega) holds
( A ? c= A + iff <%> E in A )
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds
( A ? c= A + iff <%> E in A )
let A be Subset of (E ^omega); ::_thesis: ( A ? c= A + iff <%> E in A )
A + = A |^.. 1 by Th50;
hence ( A ? c= A + iff <%> E in A ) by Th40; ::_thesis: verum
end;
theorem :: FLANG_3:82
for E being set
for A, B being Subset of (E ^omega) st A c= B + holds
A + c= B +
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B + holds
A + c= B +
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B + implies A + c= B + )
assume A c= B + ; ::_thesis: A + c= B +
then A c= B |^.. 1 by Th50;
then A |^.. 1 c= B |^.. 1 by Th29;
then A + c= B |^.. 1 by Th50;
hence A + c= B + by Th50; ::_thesis: verum
end;
theorem :: FLANG_3:83
for E being set
for A, B being Subset of (E ^omega) st A c= B + holds
B + = (B \/ A) +
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) st A c= B + holds
B + = (B \/ A) +
let A, B be Subset of (E ^omega); ::_thesis: ( A c= B + implies B + = (B \/ A) + )
assume A c= B + ; ::_thesis: B + = (B \/ A) +
then A c= B |^.. 1 by Th50;
then B |^.. 1 = (B \/ A) |^.. 1 by Th47;
then B |^.. 1 = (B \/ A) + by Th50;
hence B + = (B \/ A) + by Th50; ::_thesis: verum
end;
theorem :: FLANG_3:84
for E being set
for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
A |^.. n c= A +
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for n being Nat st n > 0 holds
A |^.. n c= A +
let A be Subset of (E ^omega); ::_thesis: for n being Nat st n > 0 holds
A |^.. n c= A +
let n be Nat; ::_thesis: ( n > 0 implies A |^.. n c= A + )
assume A1: n > 0 ; ::_thesis: A |^.. n c= A +
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^.. n or x in A + )
assume x in A |^.. n ; ::_thesis: x in A +
then ex k being Nat st
( k >= n & x in A |^ k ) by Th2;
hence x in A + by A1, Th48; ::_thesis: verum
end;
theorem :: FLANG_3:85
for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m > 0 holds
A |^ (m,n) c= A +
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat st m > 0 holds
A |^ (m,n) c= A +
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat st m > 0 holds
A |^ (m,n) c= A +
let m, n be Nat; ::_thesis: ( m > 0 implies A |^ (m,n) c= A + )
assume A1: m > 0 ; ::_thesis: A |^ (m,n) c= A +
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A |^ (m,n) or x in A + )
assume x in A |^ (m,n) ; ::_thesis: x in A +
then ex k being Nat st
( m <= k & k <= n & x in A |^ k ) by FLANG_2:19;
hence x in A + by A1, Th48; ::_thesis: verum
end;
theorem Th86: :: FLANG_3:86
for E being set
for A being Subset of (E ^omega) holds (A *) ^^ (A +) = (A +) ^^ (A *)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A *) ^^ (A +) = (A +) ^^ (A *)
let A be Subset of (E ^omega); ::_thesis: (A *) ^^ (A +) = (A +) ^^ (A *)
thus (A *) ^^ (A +) = (A *) ^^ (A |^.. 1) by Th50
.= (A |^.. 1) ^^ (A *) by Th32
.= (A +) ^^ (A *) by Th50 ; ::_thesis: verum
end;
theorem Th87: :: FLANG_3:87
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A +) |^ k c= A |^.. k
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A +) |^ k c= A |^.. k
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A +) |^ k c= A |^.. k
let k be Nat; ::_thesis: (A +) |^ k c= A |^.. k
percases ( k > 0 or k = 0 ) ;
suppose k > 0 ; ::_thesis: (A +) |^ k c= A |^.. k
then (A |^.. 1) |^ k c= A |^.. (1 * k) by Th19;
hence (A +) |^ k c= A |^.. k by Th50; ::_thesis: verum
end;
supposeA1: k = 0 ; ::_thesis: (A +) |^ k c= A |^.. k
A |^.. 0 = A * by Th11;
then A2: <%> E in A |^.. 0 by FLANG_1:48;
(A +) |^ k = {(<%> E)} by A1, FLANG_1:24;
hence (A +) |^ k c= A |^.. k by A1, A2, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
theorem :: FLANG_3:88
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m
let A be Subset of (E ^omega); ::_thesis: for m, n being Nat holds (A +) |^ (m,n) c= A |^.. m
let m, n be Nat; ::_thesis: (A +) |^ (m,n) c= A |^.. m
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A +) |^ (m,n) or x in A |^.. m )
assume x in (A +) |^ (m,n) ; ::_thesis: x in A |^.. m
then consider k being Nat such that
A1: m <= k and
k <= n and
A2: x in (A +) |^ k by FLANG_2:19;
(A +) |^ k c= A |^.. k by Th87;
then A3: x in A |^.. k by A2;
A |^.. k c= A |^.. m by A1, Th5;
hence x in A |^.. m by A3; ::_thesis: verum
end;
theorem :: FLANG_3:89
for E being set
for A, B being Subset of (E ^omega)
for n being Nat st A c= B + & n > 0 holds
A |^.. n c= B +
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega)
for n being Nat st A c= B + & n > 0 holds
A |^.. n c= B +
let A, B be Subset of (E ^omega); ::_thesis: for n being Nat st A c= B + & n > 0 holds
A |^.. n c= B +
let n be Nat; ::_thesis: ( A c= B + & n > 0 implies A |^.. n c= B + )
assume that
A1: A c= B + and
A2: n > 0 ; ::_thesis: A |^.. n c= B +
A c= B |^.. 1 by A1, Th50;
then A |^.. n c= B |^.. 1 by A2, Th29;
hence A |^.. n c= B + by Th50; ::_thesis: verum
end;
theorem Th90: :: FLANG_3:90
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A +) ^^ (A |^.. k) = A |^.. (k + 1)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A +) ^^ (A |^.. k) = A |^.. (k + 1)
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A +) ^^ (A |^.. k) = A |^.. (k + 1)
let k be Nat; ::_thesis: (A +) ^^ (A |^.. k) = A |^.. (k + 1)
thus (A +) ^^ (A |^.. k) = (A |^.. 1) ^^ (A |^.. k) by Th50
.= A |^.. (k + 1) by Th18 ; ::_thesis: verum
end;
theorem :: FLANG_3:91
for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A +) ^^ (A |^.. k) = (A |^.. k) ^^ (A +)
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega)
for k being Nat holds (A +) ^^ (A |^.. k) = (A |^.. k) ^^ (A +)
let A be Subset of (E ^omega); ::_thesis: for k being Nat holds (A +) ^^ (A |^.. k) = (A |^.. k) ^^ (A +)
let k be Nat; ::_thesis: (A +) ^^ (A |^.. k) = (A |^.. k) ^^ (A +)
thus (A +) ^^ (A |^.. k) = A |^.. (k + 1) by Th90
.= (A |^.. k) ^^ (A |^.. 1) by Th18
.= (A |^.. k) ^^ (A +) by Th50 ; ::_thesis: verum
end;
theorem Th92: :: FLANG_3:92
for E being set
for A being Subset of (E ^omega) holds (A +) ^^ (A *) = A +
proof
let E be set ; ::_thesis: for A being Subset of (E ^omega) holds (A +) ^^ (A *) = A +
let A be Subset of (E ^omega); ::_thesis: (A +) ^^ (A *) = A +
thus (A +) ^^ (A *) = (A |^.. 1) ^^ (A *) by Th50
.= A |^.. 1 by Th17
.= A + by Th50 ; ::_thesis: verum
end;
theorem :: FLANG_3:93
for E being set
for B, A being Subset of (E ^omega) st B c= A * holds
( (A +) ^^ B c= A + & B ^^ (A +) c= A + )
proof
let E be set ; ::_thesis: for B, A being Subset of (E ^omega) st B c= A * holds
( (A +) ^^ B c= A + & B ^^ (A +) c= A + )
let B, A be Subset of (E ^omega); ::_thesis: ( B c= A * implies ( (A +) ^^ B c= A + & B ^^ (A +) c= A + ) )
assume A1: B c= A * ; ::_thesis: ( (A +) ^^ B c= A + & B ^^ (A +) c= A + )
then B ^^ (A +) c= (A *) ^^ (A +) by FLANG_1:17;
then A2: B ^^ (A +) c= (A +) ^^ (A *) by Th86;
(A +) ^^ B c= (A +) ^^ (A *) by A1, FLANG_1:17;
hence ( (A +) ^^ B c= A + & B ^^ (A +) c= A + ) by A2, Th92; ::_thesis: verum
end;
theorem :: FLANG_3:94
for E being set
for A, B being Subset of (E ^omega) holds (A /\ B) + c= (A +) /\ (B +)
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds (A /\ B) + c= (A +) /\ (B +)
let A, B be Subset of (E ^omega); ::_thesis: (A /\ B) + c= (A +) /\ (B +)
A1: A + = A |^.. 1 by Th50;
A2: B + = B |^.. 1 by Th50;
(A /\ B) + = (A /\ B) |^.. 1 by Th50;
hence (A /\ B) + c= (A +) /\ (B +) by A1, A2, Th44; ::_thesis: verum
end;
theorem :: FLANG_3:95
for E being set
for A, B being Subset of (E ^omega) holds (A +) \/ (B +) c= (A \/ B) +
proof
let E be set ; ::_thesis: for A, B being Subset of (E ^omega) holds (A +) \/ (B +) c= (A \/ B) +
let A, B be Subset of (E ^omega); ::_thesis: (A +) \/ (B +) c= (A \/ B) +
A1: A + = A |^.. 1 by Th50;
A2: B + = B |^.. 1 by Th50;
(A \/ B) + = (A \/ B) |^.. 1 by Th50;
hence (A +) \/ (B +) c= (A \/ B) + by A1, A2, Th45; ::_thesis: verum
end;
theorem :: FLANG_3:96
for E, x being set
for A being Subset of (E ^omega) holds
( <%x%> in A + iff <%x%> in A )
proof
let E, x be set ; ::_thesis: for A being Subset of (E ^omega) holds
( <%x%> in A + iff <%x%> in A )
let A be Subset of (E ^omega); ::_thesis: ( <%x%> in A + iff <%x%> in A )
A + = A |^.. 1 by Th50;
hence ( <%x%> in A + iff <%x%> in A ) by Th46; ::_thesis: verum
end;