:: FINSUB_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let IT be set ;
attr IT 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;
attr IT 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;
attr IT 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 ;
attr IT 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 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 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 preBoolean set ;
existence
ex b1 being set st
( not b1 is empty & b1 is cup-closed & b1 is cap-closed & b1 is diff-closed )
proof end;
end;

theorem :: FINSUB_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th10: :: FINSUB_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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

theorem :: FINSUB_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th13: :: FINSUB_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th14: :: FINSUB_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: FINSUB_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: FINSUB_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: FINSUB_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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

theorem Th18: :: FINSUB_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty preBoolean set holds {} in A
proof end;

theorem :: FINSUB_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th20: :: FINSUB_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds bool A is preBoolean
proof end;

registration
let A be set ;
cluster bool A -> cup-closed diff-closed preBoolean ;
coherence
bool A is preBoolean by Th20;
end;

theorem :: FINSUB_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty preBoolean set holds
( not A /\ B is empty & A /\ B is preBoolean )
proof 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 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 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 cup-closed diff-closed preBoolean ;
coherence
not Fin A is empty
proof end;
end;

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

theorem :: FINSUB_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th23: :: FINSUB_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being set st A c= B holds
Fin A c= Fin B
proof end;

theorem :: FINSUB_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being set holds Fin (A /\ B) = (Fin A) /\ (Fin B)
proof end;

theorem :: FINSUB_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being set holds (Fin A) \/ (Fin B) c= Fin (A \/ B)
proof end;

theorem Th26: :: FINSUB_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds Fin A c= bool A
proof end;

theorem Th27: :: FINSUB_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set st A is finite holds
Fin A = bool A
proof end;

theorem :: FINSUB_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Fin {} = {{} } by Th27, ZFMISC_1:1;

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

theorem :: FINSUB_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for X being Finite_Subset of A holds X is finite ;

theorem :: FINSUB_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for X being Finite_Subset of A holds X is Subset of A by Def5;

theorem :: FINSUB_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FINSUB_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for X being Subset of A st A is finite holds
X is Finite_Subset of A
proof end;