:: FINSUB_1 semantic presentation

begin


definition
let IT be set ;
attrIT is cup-closed  means :Def1: :: FINSUB_1:def 1
 for X, Y being set st X in IT & Y in IT holds
X \/ Y in IT;
attrIT is cap-closed  means :: FINSUB_1:def 2
 for X, Y being set st X in IT & Y in IT holds
X /\ Y in IT;
attrIT is diff-closed  means :Def3: :: FINSUB_1:def 3
 for X, Y being set st X in IT & Y in IT holds
X \ Y in IT;
end;

:: deftheorem Def1 defines cup-closed FINSUB_1:def_1_:_
 for IT being set holds
( IT is cup-closed iff for X, Y being set st X in IT & Y in IT holds
X \/ Y in IT );

:: deftheorem  defines cap-closed FINSUB_1:def_2_:_
 for IT being set holds
( IT is cap-closed iff for X, Y being set st X in IT & Y in IT holds
X /\ Y in IT );

:: deftheorem Def3 defines diff-closed FINSUB_1:def_3_:_
 for IT being set holds
( IT is diff-closed iff for X, Y being set st X in IT & Y in IT holds
X \ Y in IT );

definition
let IT be set ;
attrIT is preBoolean  means :Def4: :: FINSUB_1:def 4
( IT is cup-closed & IT is diff-closed );
end;

:: deftheorem Def4 defines preBoolean FINSUB_1:def_4_:_
 for IT being set holds
( IT is preBoolean iff ( IT is cup-closed & IT is diff-closed ) );

registration
cluster preBoolean  ->  cup-closed diff-closed for set ;
coherence
 for b1 being set st b1 is preBoolean holds
( b1 is cup-closed & b1 is diff-closed ) by Def4;
cluster cup-closed diff-closed  ->  preBoolean for set ;
coherence
 for b1 being set st b1 is cup-closed & b1 is diff-closed holds
b1 is preBoolean by Def4;
end;

registration
cluster non empty cup-closed cap-closed diff-closed for set ;
existence
 ex b1 being set st
( not b1 is empty & b1 is cup-closed & b1 is cap-closed & b1 is diff-closed )
proof
take  {{}} ; ::_thesis: ( not {{}} is empty & {{}} is cup-closed & {{}} is cap-closed & {{}} is diff-closed )
thus  not {{}} is empty ; ::_thesis: ( {{}} is cup-closed & {{}} is cap-closed & {{}} is diff-closed )
thus  {{}} is cup-closed ::_thesis: ( {{}} is cap-closed & {{}} is diff-closed )
proof
let X, Y be set ; :: according to FINSUB_1:def_1 ::_thesis: ( X in {{}} & Y in {{}} implies X \/ Y in {{}} )
assume that
A1: X in {{}} and
A2: Y in {{}} ; ::_thesis: X \/ Y in {{}}
 X = {} by A1, TARSKI:def_1;
hence  X \/ Y in {{}} by A2; ::_thesis: verum
end;
thus  {{}} is cap-closed ::_thesis: {{}} is diff-closed
proof
let X, Y be set ; :: according to FINSUB_1:def_2 ::_thesis: ( X in {{}} & Y in {{}} implies X /\ Y in {{}} )
assume that
A3: X in {{}} and
 Y in {{}} ; ::_thesis: X /\ Y in {{}}
 X = {} by A3, TARSKI:def_1;
hence  X /\ Y in {{}} by TARSKI:def_1; ::_thesis: verum
end;
thus  {{}} is diff-closed ::_thesis: verum
proof
let X, Y be set ; :: according to FINSUB_1:def_3 ::_thesis: ( X in {{}} & Y in {{}} implies X \ Y in {{}} )
assume that
A4: X in {{}} and
 Y in {{}} ; ::_thesis: X \ Y in {{}}
 X = {} by A4, TARSKI:def_1;
hence  X \ Y in {{}} by TARSKI:def_1; ::_thesis: verum
end;
end;
end;

theorem Th1: :: FINSUB_1:1
for A being set holds
( A is preBoolean iff for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) )
proof
let A be set ; ::_thesis: ( A is preBoolean iff for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) )
thus  ( A is preBoolean implies for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) ) by Def1, Def3; ::_thesis: ( ( for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) ) implies A is preBoolean )
assume A1: for X, Y being set st X in A & Y in A holds
( X \/ Y in A & X \ Y in A ) ; ::_thesis: A is preBoolean
A2: A is diff-closed
proof
let X, Y be set ; :: according to FINSUB_1:def_3 ::_thesis: ( X in A & Y in A implies X \ Y in A )
assume  ( X in A & Y in A ) ; ::_thesis: X \ Y in A
hence  X \ Y in A by A1; ::_thesis: verum
end;
 A is cup-closed
proof
let X, Y be set ; :: according to FINSUB_1:def_1 ::_thesis: ( X in A & Y in A implies X \/ Y in A )
assume  ( X in A & Y in A ) ; ::_thesis: X \/ Y in A
hence  X \/ Y in A by A1; ::_thesis: verum
end;
hence  A is preBoolean by A2; ::_thesis: verum
end;

definition
let A be non empty preBoolean set ;
let X, Y be Element of A;
:: original: \/
redefine funcX \/ Y ->  Element of A;
correctness
coherence
X \/ Y is Element of A;
by Th1;
:: original: \
redefine funcX \ Y ->  Element of A;
correctness
coherence
X \ Y is Element of A;
by Th1;
end;

theorem Th2: :: FINSUB_1:2
for X, Y being set
for A being non empty preBoolean set st X is Element of A & Y is Element of A holds
X /\ Y is Element of A
proof
let X, Y be set ; ::_thesis: for A being non empty preBoolean set st X is Element of A & Y is Element of A holds
X /\ Y is Element of A
let A be non empty preBoolean set ; ::_thesis: ( X is Element of A & Y is Element of A implies X /\ Y is Element of A )
assume  ( X is Element of A & Y is Element of A ) ; ::_thesis: X /\ Y is Element of A
then reconsider X = X, Y = Y as Element of A ;
 X /\ Y = X \ (X \ Y) by XBOOLE_1:48;
hence  X /\ Y is Element of A ; ::_thesis: verum
end;

theorem Th3: :: FINSUB_1:3
for X, Y being set
for A being non empty preBoolean set st X is Element of A & Y is Element of A holds
X \+\ Y is Element of A
proof
let X, Y be set ; ::_thesis: for A being non empty preBoolean set st X is Element of A & Y is Element of A holds
X \+\ Y is Element of A
let A be non empty preBoolean set ; ::_thesis: ( X is Element of A & Y is Element of A implies X \+\ Y is Element of A )
assume  ( X is Element of A & Y is Element of A ) ; ::_thesis: X \+\ Y is Element of A
then reconsider X = X, Y = Y as Element of A ;
 X \+\ Y = (X \ Y) \/ (Y \ X) ;
hence  X \+\ Y is Element of A ; ::_thesis: verum
end;

theorem :: FINSUB_1:4
for A being non empty set st ( for X, Y being Element of A holds
( X \+\ Y in A & X \ Y in A ) ) holds
A is preBoolean
proof
let A be non empty set ; ::_thesis: ( ( for X, Y being Element of A holds
( X \+\ Y in A & X \ Y in A ) ) implies A is preBoolean )
assume A1: for X, Y being Element of A holds
( X \+\ Y in A & X \ Y in A ) ; ::_thesis: A is preBoolean
now__::_thesis:_for_X,_Y_being_set_st_X_in_A_&_Y_in_A_holds_
(_X_\/_Y_in_A_&_X_\_Y_in_A_)
let X, Y be set ; ::_thesis: ( X in A & Y in A implies ( X \/ Y in A & X \ Y in A ) )
assume that
A2: X in A and
A3: Y in A ; ::_thesis: ( X \/ Y in A & X \ Y in A )
reconsider Z = Y \ X as Element of A by A1, A2, A3;
 X \/ Y = X \+\ Z by XBOOLE_1:98;
hence  X \/ Y in A by A1, A2; ::_thesis: X \ Y in A
thus  X \ Y in A by A1, A2, A3; ::_thesis: verum
end;
hence  A is preBoolean by Th1; ::_thesis: verum
end;

theorem :: FINSUB_1:5
for A being non empty set st ( for X, Y being Element of A holds
( X \+\ Y in A & X /\ Y in A ) ) holds
A is preBoolean
proof
let A be non empty set ; ::_thesis: ( ( for X, Y being Element of A holds
( X \+\ Y in A & X /\ Y in A ) ) implies A is preBoolean )
assume A1: for X, Y being Element of A holds
( X \+\ Y in A & X /\ Y in A ) ; ::_thesis: A is preBoolean
now__::_thesis:_for_X,_Y_being_set_st_X_in_A_&_Y_in_A_holds_
(_X_\/_Y_in_A_&_X_\_Y_in_A_)
let X, Y be set ; ::_thesis: ( X in A & Y in A implies ( X \/ Y in A & X \ Y in A ) )
assume that
A2: X in A and
A3: Y in A ; ::_thesis: ( X \/ Y in A & X \ Y in A )
reconsider Z1 = X \+\ Y, Z2 = X /\ Y as Element of A by A1, A2, A3;
 X \/ Y = Z1 \+\ Z2 by XBOOLE_1:94;
hence  X \/ Y in A by A1; ::_thesis: X \ Y in A
 X \ Y = X \+\ Z2 by XBOOLE_1:100;
hence  X \ Y in A by A1, A2; ::_thesis: verum
end;
hence  A is preBoolean by Th1; ::_thesis: verum
end;

theorem :: FINSUB_1:6
for A being non empty set st ( for X, Y being Element of A holds
( X \+\ Y in A & X \/ Y in A ) ) holds
A is preBoolean
proof
let A be non empty set ; ::_thesis: ( ( for X, Y being Element of A holds
( X \+\ Y in A & X \/ Y in A ) ) implies A is preBoolean )
assume A1: for X, Y being Element of A holds
( X \+\ Y in A & X \/ Y in A ) ; ::_thesis: A is preBoolean
now__::_thesis:_for_X,_Y_being_set_st_X_in_A_&_Y_in_A_holds_
(_X_\/_Y_in_A_&_X_\_Y_in_A_)
let X, Y be set ; ::_thesis: ( X in A & Y in A implies ( X \/ Y in A & X \ Y in A ) )
assume that
A2: X in A and
A3: Y in A ; ::_thesis: ( X \/ Y in A & X \ Y in A )
thus  X \/ Y in A by A1, A2, A3; ::_thesis: X \ Y in A
reconsider Z1 = X \+\ Y, Z2 = X \/ Y as Element of A by A1, A2, A3;
 X /\ Y = Z1 \+\ Z2 by XBOOLE_1:95;
then reconsider Z = X /\ Y as Element of A by A1;
 X \ Y = X \+\ Z by XBOOLE_1:100;
hence  X \ Y in A by A1, A2; ::_thesis: verum
end;
hence  A is preBoolean by Th1; ::_thesis: verum
end;

definition
let A be non empty preBoolean set ;
let X, Y be Element of A;
:: original: /\
redefine funcX /\ Y ->  Element of A;
coherence
 X /\ Y is Element of A by Th2;
:: original: \+\
redefine funcX \+\ Y ->  Element of A;
coherence
 X \+\ Y is Element of A by Th3;
end;

theorem Th7: :: FINSUB_1:7
for A being non empty preBoolean set holds {} in A
proof
let A be non empty preBoolean set ; ::_thesis: {} in A
set x = the Element of A;
 the Element of A \ the Element of A = {} by XBOOLE_1:37;
hence  {} in A ; ::_thesis: verum
end;

theorem Th8: :: FINSUB_1:8
for A being set holds bool A is preBoolean
proof
let A be set ; ::_thesis: bool A is preBoolean
now__::_thesis:_for_X,_Y_being_set_st_X_in_bool_A_&_Y_in_bool_A_holds_
(_X_\/_Y_in_bool_A_&_X_\_Y_in_bool_A_)
let X, Y be set ; ::_thesis: ( X in bool A & Y in bool A implies ( X \/ Y in bool A & X \ Y in bool A ) )
assume  ( X in bool A & Y in bool A ) ; ::_thesis: ( X \/ Y in bool A & X \ Y in bool A )
then reconsider X9 = X, Y9 = Y as Subset of A ;
 ( X9 \/ Y9 in bool A & X9 \ Y9 in bool A ) ;
hence  ( X \/ Y in bool A & X \ Y in bool A ) ; ::_thesis: verum
end;
hence  bool A is preBoolean by Th1; ::_thesis: verum
end;

registration
let A be set ;
cluster bool A ->  preBoolean ;
coherence
 bool A is preBoolean by Th8;
end;

theorem :: FINSUB_1:9
for A, B being non empty preBoolean set holds
( not A /\ B is empty & A /\ B is preBoolean )
proof
let A, B be non empty preBoolean set ; ::_thesis: ( not A /\ B is empty & A /\ B is preBoolean )
 ( {} in A & {} in B ) by Th7;
then reconsider C = A /\ B as non empty set by XBOOLE_0:def_4;
now__::_thesis:_for_X,_Y_being_set_st_X_in_C_&_Y_in_C_holds_
(_X_\/_Y_in_C_&_X_\_Y_in_C_)
let X, Y be set ; ::_thesis: ( X in C & Y in C implies ( X \/ Y in C & X \ Y in C ) )
assume A1: ( X in C & Y in C ) ; ::_thesis: ( X \/ Y in C & X \ Y in C )
then A2: ( X in B & Y in B ) by XBOOLE_0:def_4;
then A3: X \/ Y in B by Th1;
A4: X \ Y in B by A2, Th1;
A5: ( X in A & Y in A ) by A1, XBOOLE_0:def_4;
then  X \/ Y in A by Th1;
hence  X \/ Y in C by A3, XBOOLE_0:def_4; ::_thesis: X \ Y in C
 X \ Y in A by A5, Th1;
hence  X \ Y in C by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  ( not A /\ B is empty & A /\ B is preBoolean ) by Th1; ::_thesis: verum
end;

definition
let A be set ;
func Fin A ->  preBoolean set  means :Def5: :: FINSUB_1:def 5
 for X being set holds
( X in it iff ( X c= A & X is finite ) );
existence
 ex b1 being preBoolean set st
for X being set holds
( X in b1 iff ( X c= A & X is finite ) )
proof
defpred S1[ set ] means  ex y being set st
( y = $1 & y c= A & y is finite );
consider P being set  such that
A1: for x being set holds
( x in P iff ( x in bool A & S1[x] ) ) from XBOOLE_0:sch_1();
 {} c= A by XBOOLE_1:2;
then reconsider Q = P as non empty set by A1;
 for X, Y being set st X in Q & Y in Q holds
( X \/ Y in Q & X \ Y in Q )
proof
let X, Y be set ; ::_thesis: ( X in Q & Y in Q implies ( X \/ Y in Q & X \ Y in Q ) )
assume that
A2: X in Q and
A3: Y in Q ; ::_thesis: ( X \/ Y in Q & X \ Y in Q )
consider Z1 being set  such that
A4: Z1 = X and
A5: Z1 c= A and
A6: Z1 is finite by A1, A2;
consider Z2 being set  such that
A7: Z2 = Y and
A8: Z2 c= A and
A9: Z2 is finite by A1, A3;
A10: Z1 \ Z2 c= A by A5, XBOOLE_1:1;
 Z1 \/ Z2 c= A by A5, A8, XBOOLE_1:8;
hence  ( X \/ Y in Q & X \ Y in Q ) by A1, A4, A6, A7, A9, A10; ::_thesis: verum
end;
then reconsider R = Q as non empty preBoolean set by Th1;
 for X being set holds
( X in R iff ( X c= A & X is finite ) )
proof
let X be set ; ::_thesis: ( X in R iff ( X c= A & X is finite ) )
thus  ( X in R implies ( X c= A & X is finite ) ) ::_thesis: ( X c= A & X is finite implies X in R )
proof
assume  X in R ; ::_thesis: ( X c= A & X is finite )
then  ex Y being set st
( Y = X & Y c= A & Y is finite ) by A1;
hence  ( X c= A & X is finite ) ; ::_thesis: verum
end;
thus  ( X c= A & X is finite implies X in R ) by A1; ::_thesis: verum
end;
hence  ex b1 being preBoolean set st
for X being set holds
( X in b1 iff ( X c= A & X is finite ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being preBoolean set st ( for X being set holds
( X in b1 iff ( X c= A & X is finite ) ) ) & ( for X being set holds
( X in b2 iff ( X c= A & X is finite ) ) ) holds
b1 = b2
proof
let P, Q be preBoolean set ; ::_thesis: ( ( for X being set holds
( X in P iff ( X c= A & X is finite ) ) ) & ( for X being set holds
( X in Q iff ( X c= A & X is finite ) ) ) implies P = Q )
assume that
A11: for X being set holds
( X in P iff ( X c= A & X is finite ) ) and
A12: for X being set holds
( X in Q iff ( X c= A & X is finite ) ) ; ::_thesis: P = Q
 for x being set holds
( x in P iff x in Q )
proof
let x be set ; ::_thesis: ( x in P iff x in Q )
thus  ( x in P implies x in Q ) ::_thesis: ( x in Q implies x in P )
proof
assume  x in P ; ::_thesis: x in Q
then  ( x c= A & x is finite ) by A11;
hence  x in Q by A12; ::_thesis: verum
end;
thus  ( x in Q implies x in P ) ::_thesis: verum
proof
assume  x in Q ; ::_thesis: x in P
then  ( x c= A & x is finite ) by A12;
hence  x in P by A11; ::_thesis: verum
end;
end;
hence  P = Q by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Fin FINSUB_1:def_5_:_
 for A being set
for b2 being preBoolean set holds
( b2 = Fin A iff for X being set holds
( X in b2 iff ( X c= A & X is finite ) ) );

registration
let A be set ;
cluster Fin A ->  non empty preBoolean ;
coherence
 not Fin A is empty
proof
 {} c= A by XBOOLE_1:2;
hence  not Fin A is empty by Def5; ::_thesis: verum
end;
end;

registration
let A be set ;
cluster  ->  finite for Element of Fin A;
coherence
 for b1 being Element of Fin A holds b1 is finite by Def5;
end;

theorem Th10: :: FINSUB_1:10
for A, B being set st A c= B holds
Fin A c= Fin B
proof
let A, B be set ; ::_thesis: ( A c= B implies Fin A c= Fin B )
assume A1: A c= B ; ::_thesis: Fin A c= Fin B
now__::_thesis:_for_X_being_set_st_X_in_Fin_A_holds_
X_in_Fin_B
let X be set ; ::_thesis: ( X in Fin A implies X in Fin B )
assume A2: X in Fin A ; ::_thesis: X in Fin B
then  X c= A by Def5;
then  X c= B by A1, XBOOLE_1:1;
hence  X in Fin B by A2, Def5; ::_thesis: verum
end;
hence  Fin A c= Fin B by TARSKI:def_3; ::_thesis: verum
end;

theorem :: FINSUB_1:11
for A, B being set holds Fin (A /\ B) = (Fin A) /\ (Fin B)
proof
let A, B be set ; ::_thesis: Fin (A /\ B) = (Fin A) /\ (Fin B)
 ( Fin (A /\ B) c= Fin A & Fin (A /\ B) c= Fin B ) by Th10, XBOOLE_1:17;
hence  Fin (A /\ B) c= (Fin A) /\ (Fin B) by XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: (Fin A) /\ (Fin B) c= Fin (A /\ B)
now__::_thesis:_for_X_being_set_st_X_in_(Fin_A)_/\_(Fin_B)_holds_
X_in_Fin_(A_/\_B)
let X be set ; ::_thesis: ( X in (Fin A) /\ (Fin B) implies X in Fin (A /\ B) )
assume A1: X in (Fin A) /\ (Fin B) ; ::_thesis: X in Fin (A /\ B)
then  X in Fin B by XBOOLE_0:def_4;
then A2: X c= B by Def5;
A3: X in Fin A by A1, XBOOLE_0:def_4;
then  X c= A by Def5;
then  X c= A /\ B by A2, XBOOLE_1:19;
hence  X in Fin (A /\ B) by A3, Def5; ::_thesis: verum
end;
hence  (Fin A) /\ (Fin B) c= Fin (A /\ B) by TARSKI:def_3; ::_thesis: verum
end;

theorem :: FINSUB_1:12
for A, B being set holds (Fin A) \/ (Fin B) c= Fin (A \/ B)
proof
let A, B be set ; ::_thesis: (Fin A) \/ (Fin B) c= Fin (A \/ B)
 ( Fin A c= Fin (A \/ B) & Fin B c= Fin (A \/ B) ) by Th10, XBOOLE_1:7;
hence  (Fin A) \/ (Fin B) c= Fin (A \/ B) by XBOOLE_1:8; ::_thesis: verum
end;

theorem Th13: :: FINSUB_1:13
for A being set holds Fin A c= bool A
proof
let A be set ; ::_thesis: Fin A c= bool A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fin A or x in bool A )
assume  x in Fin A ; ::_thesis: x in bool A
then  x c= A by Def5;
hence  x in bool A ; ::_thesis: verum
end;

theorem Th14: :: FINSUB_1:14
for A being set st A is finite holds
Fin A = bool A
proof
let A be set ; ::_thesis: ( A is finite implies Fin A = bool A )
assume A1: A is finite ; ::_thesis: Fin A = bool A
A2: bool A c= Fin A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool A or x in Fin A )
assume  x in bool A ; ::_thesis: x in Fin A
hence  x in Fin A by A1, Def5; ::_thesis: verum
end;
 Fin A c= bool A by Th13;
hence  Fin A = bool A by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: FINSUB_1:15
Fin {} = {{}} by Th14, ZFMISC_1:1;

definition
let A be set ;
mode Finite_Subset of A is Element of Fin A;
end;

theorem :: FINSUB_1:16
for A being set
for X being Finite_Subset of A holds X is finite ;

theorem :: FINSUB_1:17
for A being set
for X being Finite_Subset of A holds X is Subset of A by Def5;

theorem :: FINSUB_1:18
for A being set
for X being Subset of A st A is finite holds
X is Finite_Subset of A by Def5;