subset_1.miz
begin
reserve E,X,Y,x for
set;
registration
let X be
set;
cluster (
bool X) -> non
empty;
coherence by
ZFMISC_1:def 1;
end
registration
let x1,x2,x3 be
object;
cluster
{x1, x2, x3} -> non
empty;
coherence by
ENUMSET1:def 1;
let x4 be
object;
cluster
{x1, x2, x3, x4} -> non
empty;
coherence by
ENUMSET1:def 2;
let x5 be
object;
cluster
{x1, x2, x3, x4, x5} -> non
empty;
coherence by
ENUMSET1:def 3;
let x6 be
object;
cluster
{x1, x2, x3, x4, x5, x6} -> non
empty;
coherence by
ENUMSET1:def 4;
let x7 be
object;
cluster
{x1, x2, x3, x4, x5, x6, x7} -> non
empty;
coherence by
ENUMSET1:def 5;
let x8 be
object;
cluster
{x1, x2, x3, x4, x5, x6, x7, x8} -> non
empty;
coherence by
ENUMSET1:def 6;
let x9 be
object;
cluster
{x1, x2, x3, x4, x5, x6, x7, x8, x9} -> non
empty;
coherence by
ENUMSET1:def 7;
let x10 be
object;
cluster
{x1, x2, x3, x4, x5, x6, x7, x8, x9, x10} -> non
empty;
coherence by
ENUMSET1:def 8;
end
definition
let X;
::
SUBSET_1:def1
mode
Element of X ->
set means
:
Def1: it
in X if X is non
empty
otherwise it is
empty;
existence
proof
thus X is non
empty implies ex Y be
set st Y
in X
proof
assume X is non
empty;
then
consider Y be
object such that
A1: Y
in X;
reconsider Y as
set by
TARSKI: 1;
take Y;
thus thesis by
A1;
end;
thus thesis;
end;
consistency ;
sethood
proof
per cases ;
case X is non
empty;
take X;
thus thesis;
end;
case X is
empty;
take
{
{} };
let y be
set;
thus thesis by
TARSKI:def 1;
end;
end;
end
definition
let X;
mode
Subset of X is
Element of (
bool X);
end
registration
let X be non
empty
set;
cluster non
empty for
Subset of X;
existence
proof
X
in (
bool X) by
ZFMISC_1:def 1;
then X is
Subset of X by
Def1;
hence thesis;
end;
end
registration
let X1,X2 be non
empty
set;
cluster
[:X1, X2:] -> non
empty;
coherence
proof
consider x2 be
object such that
A1: x2
in X2 by
XBOOLE_0:def 1;
consider x1 be
object such that
A2: x1
in X1 by
XBOOLE_0:def 1;
[x1, x2]
in
[:X1, X2:] by
A2,
A1,
ZFMISC_1:def 2;
hence thesis;
end;
end
registration
let X1,X2,X3 be non
empty
set;
cluster
[:X1, X2, X3:] -> non
empty;
coherence ;
end
registration
let X1,X2,X3,X4 be non
empty
set;
cluster
[:X1, X2, X3, X4:] -> non
empty;
coherence ;
end
definition
let D be non
empty
set, X be non
empty
Subset of D;
:: original:
Element
redefine
mode
Element of X ->
Element of D ;
coherence
proof
let x be
Element of X;
X
in (
bool D) by
Def1;
then
A1: X
c= D by
ZFMISC_1:def 1;
x
in X by
Def1;
then x
in D by
A1;
hence thesis by
Def1;
end;
end
Lm1: for X be
Subset of E, x be
object st x
in X holds x
in E
proof
let X be
Subset of E, x be
object such that
A1: x
in X;
X
in (
bool E) by
Def1;
then X
c= E by
ZFMISC_1:def 1;
hence thesis by
A1;
end;
registration
let E;
cluster
empty for
Subset of E;
existence
proof
{}
c= E;
then
{}
in (
bool E) by
ZFMISC_1:def 1;
then
{} is
Subset of E by
Def1;
hence thesis;
end;
end
definition
let E;
::
SUBSET_1:def2
func
{} E ->
Subset of E equals
{} ;
coherence
proof
{}
c= E;
then
{}
in (
bool E) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
correctness ;
::
SUBSET_1:def3
func
[#] E ->
Subset of E equals E;
coherence
proof
E
in (
bool E) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
correctness ;
end
registration
let E;
cluster (
{} E) ->
empty;
coherence ;
end
theorem ::
SUBSET_1:1
{} is
Subset of X
proof
(
{} X)
=
{} ;
hence thesis;
end;
reserve A,B,C for
Subset of E;
theorem ::
SUBSET_1:2
Th2: (for x be
Element of E holds x
in A implies x
in B) implies A
c= B
proof
assume
A1: for x be
Element of E holds x
in A implies x
in B;
let x be
object;
assume
A2: x
in A;
reconsider x as
set by
TARSKI: 1;
x
in E by
Lm1,
A2;
then x is
Element of E by
Def1;
hence thesis by
A1,
A2;
end;
theorem ::
SUBSET_1:3
(for x be
Element of E holds x
in A iff x
in B) implies A
= B by
Th2;
theorem ::
SUBSET_1:4
Th4: A
<>
{} implies ex x be
Element of E st x
in A
proof
assume A
<>
{} ;
then
consider x be
object such that
A1: x
in A by
XBOOLE_0:def 1;
reconsider x as
set by
TARSKI: 1;
x
in E by
A1,
Lm1;
then x is
Element of E by
Def1;
hence thesis by
A1;
end;
definition
let E, A;
::
SUBSET_1:def4
func A
` ->
Subset of E equals (E
\ A);
coherence
proof
(E
\ A)
c= E by
XBOOLE_1: 36;
then (E
\ A)
in (
bool E) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
correctness ;
involutiveness
proof
let S,T be
Subset of E;
assume
A1: S
= (E
\ T);
T
in (
bool E) by
Def1;
then T
c= E by
ZFMISC_1:def 1;
hence T
= (
{}
\/ (E
/\ T)) by
XBOOLE_1: 28
.= ((E
\ E)
\/ (E
/\ T)) by
XBOOLE_1: 37
.= (E
\ S) by
A1,
XBOOLE_1: 52;
end;
let B;
:: original:
\/
redefine
func A
\/ B ->
Subset of E ;
coherence
proof
B
in (
bool E) by
Def1;
then
A2: B
c= E by
ZFMISC_1:def 1;
A
in (
bool E) by
Def1;
then A
c= E by
ZFMISC_1:def 1;
then (A
\/ B)
c= E by
A2,
XBOOLE_1: 8;
then (A
\/ B)
in (
bool E) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
:: original:
\+\
redefine
func A
\+\ B ->
Subset of E ;
coherence
proof
B
in (
bool E) by
Def1;
then (B
\ A)
c= B & B
c= E by
XBOOLE_1: 36,
ZFMISC_1:def 1;
then
A3: (B
\ A)
c= E;
A
in (
bool E) by
Def1;
then (A
\ B)
c= A & A
c= E by
XBOOLE_1: 36,
ZFMISC_1:def 1;
then (A
\ B)
c= E;
then ((A
\ B)
\/ (B
\ A))
c= E by
A3,
XBOOLE_1: 8;
then (A
\+\ B)
in (
bool E) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
end
definition
let X,Y be
set;
:: original:
\
redefine
func X
\ Y ->
Subset of X ;
coherence
proof
(X
\ Y)
c= X by
XBOOLE_1: 36;
then (X
\ Y)
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
end
definition
let E, A, X;
:: original:
\
redefine
func A
\ X ->
Subset of E ;
coherence
proof
A
in (
bool E) by
Def1;
then (A
\ X)
c= A & A
c= E by
XBOOLE_1: 36,
ZFMISC_1:def 1;
then (A
\ X)
c= E;
then (A
\ X)
in (
bool E) by
ZFMISC_1:def 1;
hence (A
\ X) is
Subset of E by
Def1;
end;
end
definition
let E, A, X;
:: original:
/\
redefine
func A
/\ X ->
Subset of E ;
coherence
proof
A
in (
bool E) by
Def1;
then (A
/\ X)
c= A & A
c= E by
XBOOLE_1: 17,
ZFMISC_1:def 1;
then (A
/\ X)
c= E;
then (A
/\ X)
in (
bool E) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
end
definition
let E, X, A;
:: original:
/\
redefine
func X
/\ A ->
Subset of E ;
coherence
proof
(A
/\ X) is
Subset of E;
hence thesis;
end;
end
theorem ::
SUBSET_1:5
(for x be
Element of E holds x
in A iff x
in B or x
in C) implies A
= (B
\/ C)
proof
assume
A1: for x be
Element of E holds x
in A iff x
in B or x
in C;
now
let x be
Element of E;
assume x
in A;
then x
in B or x
in C by
A1;
hence x
in (B
\/ C) by
XBOOLE_0:def 3;
end;
hence A
c= (B
\/ C) by
Th2;
now
let x be
Element of E;
assume x
in (B
\/ C);
then x
in B or x
in C by
XBOOLE_0:def 3;
hence x
in A by
A1;
end;
hence thesis by
Th2;
end;
theorem ::
SUBSET_1:6
(for x be
Element of E holds x
in A iff x
in B & x
in C) implies A
= (B
/\ C)
proof
assume
A1: for x be
Element of E holds x
in A iff x
in B & x
in C;
now
let x be
Element of E;
assume x
in A;
then x
in B & x
in C by
A1;
hence x
in (B
/\ C) by
XBOOLE_0:def 4;
end;
hence A
c= (B
/\ C) by
Th2;
now
let x be
Element of E;
assume x
in (B
/\ C);
then x
in B & x
in C by
XBOOLE_0:def 4;
hence x
in A by
A1;
end;
hence thesis by
Th2;
end;
theorem ::
SUBSET_1:7
(for x be
Element of E holds x
in A iff x
in B & not x
in C) implies A
= (B
\ C)
proof
assume
A1: for x be
Element of E holds x
in A iff x
in B & not x
in C;
now
let x be
Element of E;
assume x
in A;
then x
in B & not x
in C by
A1;
hence x
in (B
\ C) by
XBOOLE_0:def 5;
end;
hence A
c= (B
\ C) by
Th2;
now
let x be
Element of E;
assume x
in (B
\ C);
then x
in B & not x
in C by
XBOOLE_0:def 5;
hence x
in A by
A1;
end;
hence thesis by
Th2;
end;
theorem ::
SUBSET_1:8
(for x be
Element of E holds x
in A iff not (x
in B iff x
in C)) implies A
= (B
\+\ C)
proof
assume
A1: for x be
Element of E holds x
in A iff not (x
in B iff x
in C);
now
let x be
Element of E;
assume x
in A;
then x
in B & not x
in C or x
in C & not x
in B by
A1;
then x
in (B
\ C) or x
in (C
\ B) by
XBOOLE_0:def 5;
hence x
in (B
\+\ C) by
XBOOLE_0:def 3;
end;
hence A
c= (B
\+\ C) by
Th2;
now
let x be
Element of E;
assume x
in (B
\+\ C);
then x
in (B
\ C) or x
in (C
\ B) by
XBOOLE_0:def 3;
then x
in B & not x
in C or x
in C & not x
in B by
XBOOLE_0:def 5;
hence x
in A by
A1;
end;
hence thesis by
Th2;
end;
theorem ::
SUBSET_1:9
(
[#] E)
= ((
{} E)
` );
theorem ::
SUBSET_1:10
Th10: (A
\/ (A
` ))
= (
[#] E)
proof
A
in (
bool E) by
Def1;
then A
c= E by
ZFMISC_1:def 1;
hence thesis by
XBOOLE_1: 45;
end;
theorem ::
SUBSET_1:11
(A
\/ (
[#] E))
= (
[#] E)
proof
A
in (
bool E) by
Def1;
then A
c= E by
ZFMISC_1:def 1;
hence thesis by
XBOOLE_1: 12;
end;
theorem ::
SUBSET_1:12
Th12: A
c= B iff (B
` )
c= (A
` )
proof
thus A
c= B implies (B
` )
c= (A
` ) by
XBOOLE_1: 34;
A1: (E
\ (B
` ))
= ((B
` )
` )
.= B;
(E
\ (A
` ))
= ((A
` )
` )
.= A;
hence thesis by
A1,
XBOOLE_1: 34;
end;
theorem ::
SUBSET_1:13
(A
\ B)
= (A
/\ (B
` ))
proof
A
in (
bool E) by
Def1;
then
A1: A
c= E by
ZFMISC_1:def 1;
thus (A
/\ (B
` ))
= ((A
/\ E)
\ B) by
XBOOLE_1: 49
.= (A
\ B) by
A1,
XBOOLE_1: 28;
end;
theorem ::
SUBSET_1:14
((A
\ B)
` )
= ((A
` )
\/ B)
proof
B
in (
bool E) by
Def1;
then
A1: B
c= E by
ZFMISC_1:def 1;
thus ((A
\ B)
` )
= ((E
\ A)
\/ (E
/\ B)) by
XBOOLE_1: 52
.= ((A
` )
\/ B) by
A1,
XBOOLE_1: 28;
end;
theorem ::
SUBSET_1:15
((A
\+\ B)
` )
= ((A
/\ B)
\/ ((A
` )
/\ (B
` )))
proof
A
in (
bool E) by
Def1;
then
A1: A
c= E by
ZFMISC_1:def 1;
thus ((A
\+\ B)
` )
= ((E
\ (A
\/ B))
\/ ((E
/\ A)
/\ B)) by
XBOOLE_1: 102
.= ((A
/\ B)
\/ (E
\ (A
\/ B))) by
A1,
XBOOLE_1: 28
.= ((A
/\ B)
\/ ((A
` )
/\ (B
` ))) by
XBOOLE_1: 53;
end;
theorem ::
SUBSET_1:16
A
c= (B
` ) implies B
c= (A
` )
proof
assume A
c= (B
` );
then ((B
` )
` )
c= (A
` ) by
Th12;
hence thesis;
end;
theorem ::
SUBSET_1:17
(A
` )
c= B implies (B
` )
c= A
proof
assume (A
` )
c= B;
then (B
` )
c= ((A
` )
` ) by
Th12;
hence thesis;
end;
theorem ::
SUBSET_1:18
A
c= (A
` ) iff A
= (
{} E) by
XBOOLE_1: 38;
theorem ::
SUBSET_1:19
(A
` )
c= A iff A
= (
[#] E)
proof
thus (A
` )
c= A implies A
= (
[#] E)
proof
assume (A
` )
c= A;
hence A
= (A
\/ (A
` )) by
XBOOLE_1: 12
.= (
[#] E) by
Th10;
end;
thus thesis by
XBOOLE_1: 37;
end;
theorem ::
SUBSET_1:20
X
c= A & X
c= (A
` ) implies X
=
{} by
XBOOLE_1: 67,
XBOOLE_1: 79;
theorem ::
SUBSET_1:21
((A
\/ B)
` )
c= (A
` ) by
Th12,
XBOOLE_1: 7;
theorem ::
SUBSET_1:22
(A
` )
c= ((A
/\ B)
` ) by
Th12,
XBOOLE_1: 17;
theorem ::
SUBSET_1:23
Th23: A
misses B iff A
c= (B
` )
proof
thus A
misses B implies A
c= (B
` )
proof
assume
A1: A
misses B;
let x be
object;
assume
A2: x
in A;
then
A3: not x
in B by
A1,
XBOOLE_0: 3;
x
in E by
A2,
Lm1;
hence thesis by
A3,
XBOOLE_0:def 5;
end;
assume
A4: A
c= (B
` );
assume A
meets B;
then
consider x be
object such that
A5: x
in A and
A6: x
in B by
XBOOLE_0: 3;
x
in (E
\ B) by
A4,
A5;
hence thesis by
A6,
XBOOLE_0:def 5;
end;
theorem ::
SUBSET_1:24
A
misses (B
` ) iff A
c= B
proof
((B
` )
` )
= B;
hence thesis by
Th23;
end;
theorem ::
SUBSET_1:25
A
misses B & (A
` )
misses (B
` ) implies A
= (B
` )
proof
assume that
A1: A
misses B and
A2: (A
` )
misses (B
` );
A3: A
in (
bool E) by
Def1;
thus A
c= (B
` )
proof
let x be
object;
assume
A4: x
in A;
then
A5: not x
in B by
A1,
XBOOLE_0: 3;
A
c= E by
A3,
ZFMISC_1:def 1;
then x
in E by
A4;
hence thesis by
A5,
XBOOLE_0:def 5;
end;
let x be
object;
A6: x
in (A
` ) implies not x
in (B
` ) by
A2,
XBOOLE_0: 3;
assume
A7: x
in (B
` );
then x
in E by
XBOOLE_0:def 5;
hence thesis by
A7,
A6,
XBOOLE_0:def 5;
end;
theorem ::
SUBSET_1:26
A
c= B & C
misses B implies A
c= (C
` )
proof
assume A
c= B & C
misses B;
then A
misses C by
XBOOLE_1: 63;
hence thesis by
Th23;
end;
theorem ::
SUBSET_1:27
(for a be
Element of A holds a
in B) implies A
c= B
proof
assume
A1: for a be
Element of A holds a
in B;
let a be
object;
assume
A2: a
in A;
reconsider a as
set by
TARSKI: 1;
a is
Element of A by
Def1,
A2;
hence thesis by
A1;
end;
theorem ::
SUBSET_1:28
(for x be
Element of E holds x
in A) implies E
= A
proof
assume
A1: for x be
Element of E holds x
in A;
thus E
c= A
proof
let a be
object;
assume
A2: a
in E;
reconsider a as
set by
TARSKI: 1;
a is
Element of E by
Def1,
A2;
hence thesis by
A1;
end;
A
in (
bool E) by
Def1;
hence thesis by
ZFMISC_1:def 1;
end;
theorem ::
SUBSET_1:29
E
<>
{} implies for B holds for x be
Element of E st not x
in B holds x
in (B
` )
proof
assume
A1: E
<>
{} ;
let B be
Subset of E;
let x be
Element of E;
assume
A2: not x
in B;
x
in E by
A1,
Def1;
hence thesis by
A2,
XBOOLE_0:def 5;
end;
theorem ::
SUBSET_1:30
Th30: for A, B st for x be
Element of E holds x
in A iff not x
in B holds A
= (B
` )
proof
let A,B be
Subset of E;
assume
A1: for x be
Element of E holds x
in A iff not x
in B;
thus A
c= (B
` )
proof
let x be
object;
assume
A2: x
in A;
reconsider x as
set by
TARSKI: 1;
A
in (
bool E) by
Def1;
then A
c= E by
ZFMISC_1:def 1;
then x
in E by
A2;
then x is
Element of E by
Def1;
then
A3: not x
in B by
A1,
A2;
x
in E by
A2,
Lm1;
hence thesis by
A3,
XBOOLE_0:def 5;
end;
let x be
object;
assume
A4: x
in (B
` );
reconsider x as
set by
TARSKI: 1;
(B
` )
in (
bool E) by
Def1;
then (B
` )
c= E by
ZFMISC_1:def 1;
then x
in E by
A4;
then
reconsider x as
Element of E by
Def1;
not x
in B by
A4,
XBOOLE_0:def 5;
hence thesis by
A1;
end;
theorem ::
SUBSET_1:31
for A, B st for x be
Element of E holds not x
in A iff x
in B holds A
= (B
` )
proof
let A, B;
assume for x be
Element of E holds not x
in A iff x
in B;
then for x be
Element of E holds x
in A iff not x
in B;
hence thesis by
Th30;
end;
theorem ::
SUBSET_1:32
for A, B st for x be
Element of E holds not (x
in A iff x
in B) holds A
= (B
` )
proof
let A, B;
assume for x be
Element of E holds not (x
in A iff x
in B);
then for x be
Element of E holds x
in A iff not x
in B;
hence thesis by
Th30;
end;
reserve x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 for
Element of X;
theorem ::
SUBSET_1:33
X
<>
{} implies
{x1} is
Subset of X
proof
assume X
<>
{} ;
then
A1: x1
in X by
Def1;
{x1}
c= X by
A1,
TARSKI:def 1;
then
{x1}
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
theorem ::
SUBSET_1:34
X
<>
{} implies
{x1, x2} is
Subset of X
proof
assume X
<>
{} ;
then
A1: x1
in X & x2
in X by
Def1;
{x1, x2}
c= X by
A1,
TARSKI:def 2;
then
{x1, x2}
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
theorem ::
SUBSET_1:35
X
<>
{} implies
{x1, x2, x3} is
Subset of X
proof
set A =
{x1, x2, x3};
assume
A1: X
<>
{} ;
then
A2: x3
in X by
Def1;
x1
in X & x2
in X by
A1,
Def1;
then A
c= X by
A2,
ENUMSET1:def 1;
then A
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
theorem ::
SUBSET_1:36
X
<>
{} implies
{x1, x2, x3, x4} is
Subset of X
proof
set A =
{x1, x2, x3, x4};
assume
A1: X
<>
{} ;
then
A2: x3
in X & x4
in X by
Def1;
x1
in X & x2
in X by
A1,
Def1;
then A
c= X by
A2,
ENUMSET1:def 2;
then A
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
theorem ::
SUBSET_1:37
X
<>
{} implies
{x1, x2, x3, x4, x5} is
Subset of X
proof
set A =
{x1, x2, x3, x4, x5};
assume
A1: X
<>
{} ;
A
c= X
proof
let x be
object;
x
in A implies x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 by
ENUMSET1:def 3;
hence thesis by
A1,
Def1;
end;
then A
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
theorem ::
SUBSET_1:38
X
<>
{} implies
{x1, x2, x3, x4, x5, x6} is
Subset of X
proof
set A =
{x1, x2, x3, x4, x5, x6};
assume
A1: X
<>
{} ;
A
c= X
proof
let x be
object;
x
in A implies x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6 by
ENUMSET1:def 4;
hence thesis by
A1,
Def1;
end;
then A
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
theorem ::
SUBSET_1:39
X
<>
{} implies
{x1, x2, x3, x4, x5, x6, x7} is
Subset of X
proof
set A =
{x1, x2, x3, x4, x5, x6, x7};
assume
A1: X
<>
{} ;
A
c= X
proof
let x be
object;
x
in A implies x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6 or x
= x7 by
ENUMSET1:def 5;
hence thesis by
A1,
Def1;
end;
then A
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
theorem ::
SUBSET_1:40
X
<>
{} implies
{x1, x2, x3, x4, x5, x6, x7, x8} is
Subset of X
proof
set A =
{x1, x2, x3, x4, x5, x6, x7, x8};
assume
A1: X
<>
{} ;
A
c= X
proof
let x be
object;
x
in A implies x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6 or x
= x7 or x
= x8 by
ENUMSET1:def 6;
hence thesis by
A1,
Def1;
end;
then A
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
theorem ::
SUBSET_1:41
x
in X implies
{x} is
Subset of X
proof
assume x
in X;
then
{x}
c= X by
ZFMISC_1: 31;
then
{x}
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
scheme ::
SUBSET_1:sch1
SubsetEx { A() ->
set , P[
object] } :
ex X be
Subset of A() st for x holds x
in X iff x
in A() & P[x];
consider X be
set such that
A1: for x be
object holds x
in X iff x
in A() & P[x] from
XBOOLE_0:sch 1;
X
c= A() by
A1;
then X
in (
bool A()) by
ZFMISC_1:def 1;
then
reconsider X as
Subset of A() by
Def1;
take X;
thus thesis by
A1;
end;
scheme ::
SUBSET_1:sch2
SubsetEq { X() ->
set , X1,X2() ->
Subset of X() , P[
set] } :
X1()
= X2()
provided
A1: for y be
Element of X() holds y
in X1() iff P[y]
and
A2: for y be
Element of X() holds y
in X2() iff P[y];
for x be
Element of X() holds x
in X1() iff x
in X2() by
A1,
A2;
hence thesis by
Th2;
end;
definition
let X,Y be non
empty
set;
:: original:
misses
redefine
pred X
misses Y;
irreflexivity ;
end
definition
let X,Y be non
empty
set;
:: original:
meets
redefine
pred X
meets Y;
reflexivity ;
end
definition
::$Canceled
end
begin
Lm2: (for x be
object st x
in X holds x
in Y) implies X is
Subset of Y
proof
assume for x be
object st x
in X holds x
in Y;
then X
c= Y;
then X
in (
bool Y) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
Lm3: for x be
object holds x
in A implies x is
Element of E
proof
let x be
object;
assume
A1: x
in A;
reconsider x as
set by
TARSKI: 1;
x
in E by
Lm1,
A1;
hence thesis by
Def1;
end;
scheme ::
SUBSET_1:sch3
SubsetEx { A() -> non
empty
set , P[
object] } :
ex B be
Subset of A() st for x be
Element of A() holds x
in B iff P[x];
consider B be
set such that
A1: for x be
object holds x
in B iff x
in A() & P[x] from
XBOOLE_0:sch 1;
for x be
object holds x
in B implies x
in A() by
A1;
then
reconsider B as
Subset of A() by
Lm2;
take B;
let x be
Element of A();
x
in A() by
Def1;
hence thesis by
A1;
end;
scheme ::
SUBSET_1:sch4
SubComp { A() ->
set , F1,F2() ->
Subset of A() , P[
set] } :
F1()
= F2()
provided
A1: for X be
Element of A() holds X
in F1() iff P[X]
and
A2: for X be
Element of A() holds X
in F2() iff P[X];
thus F1()
c= F2()
proof
let x be
object;
assume
A3: x
in F1();
then
reconsider X = x as
Element of A() by
Lm3;
P[X] by
A1,
A3;
hence thesis by
A2;
end;
let x be
object;
assume
A4: x
in F2();
then
reconsider X = x as
Element of A() by
Lm3;
P[X] by
A2,
A4;
hence thesis by
A1;
end;
theorem ::
SUBSET_1:42
(A
` )
= (B
` ) implies A
= B
proof
assume (A
` )
= (B
` );
hence A
= ((B
` )
` )
.= B;
end;
registration
let X be
empty
set;
cluster ->
empty for
Subset of X;
coherence
proof
let Y be
Subset of X;
Y
in (
bool X) by
Def1;
then Y
c= X by
ZFMISC_1:def 1;
hence thesis;
end;
end
definition
let E be
set;
let A be
Subset of E;
::
SUBSET_1:def6
attr A is
proper means A
<> E;
end
registration
let E be
set;
cluster (
[#] E) -> non
proper;
coherence ;
end
registration
let E be
set;
cluster non
proper for
Subset of E;
existence
proof
take (
[#] E);
thus thesis;
end;
end
registration
let E be non
empty
set;
cluster non
proper -> non
empty for
Subset of E;
coherence ;
cluster
empty ->
proper for
Subset of E;
coherence ;
end
registration
let E be non
empty
set;
cluster
proper for
Subset of E;
existence
proof
take (
{} E);
thus (
{} E)
<> E;
end;
end
registration
let E be
empty
set;
cluster -> non
proper for
Subset of E;
coherence ;
end
theorem ::
SUBSET_1:43
for X,Y,A be
set, z be
set st z
in A & A
c=
[:X, Y:] holds ex x be
Element of X, y be
Element of Y st z
=
[x, y]
proof
let X,Y,A be
set, z be
set;
assume z
in A & A
c=
[:X, Y:];
then
consider x,y be
object such that
A1: x
in X and
A2: y
in Y and
A3: z
=
[x, y] by
ZFMISC_1: 84;
reconsider x, y as
set by
TARSKI: 1;
reconsider y as
Element of Y by
A2,
Def1;
reconsider x as
Element of X by
A1,
Def1;
take x, y;
thus thesis by
A3;
end;
theorem ::
SUBSET_1:44
for X be non
empty
set, A,B be non
empty
Subset of X st A
c< B holds ex p be
Element of X st p
in B & A
c= (B
\
{p})
proof
let X be non
empty
set, A,B be non
empty
Subset of X;
assume
A1: A
c< B;
then
consider p be
Element of X such that
A2: p
in (B
\ A) by
Th4,
XBOOLE_1: 105;
A3: not p
in A by
A2,
XBOOLE_0:def 5;
take p;
thus thesis by
A1,
A2,
A3,
XBOOLE_0:def 5,
ZFMISC_1: 34;
end;
definition
let X be
set;
:: original:
trivial
redefine
::
SUBSET_1:def7
attr X is
trivial means for x,y be
Element of X holds x
= y;
compatibility
proof
thus X is
trivial implies for x,y be
Element of X holds x
= y
proof
assume
A1: X is
trivial;
let x,y be
Element of X;
per cases ;
suppose X is non
empty;
then x
in X & y
in X by
Def1;
hence x
= y by
A1;
end;
suppose X is
empty;
then x
=
{} & y
=
{} by
Def1;
hence x
= y;
end;
end;
assume
A2: for x,y be
Element of X holds x
= y;
let x,y be
object;
assume
A3: x
in X & y
in X;
reconsider x, y as
set by
TARSKI: 1;
x is
Element of X & y is
Element of X by
Def1,
A3;
hence thesis by
A2;
end;
end
registration
let X be non
empty
set;
cluster non
empty
trivial for
Subset of X;
existence
proof
the
Element of X
in X by
Def1;
then
{ the
Element of X}
c= X by
ZFMISC_1: 31;
then
{ the
Element of X}
in (
bool X) by
ZFMISC_1:def 1;
then
reconsider A =
{ the
Element of X} as
Subset of X by
Def1;
take A;
thus A is non
empty;
let x,y be
Element of A;
x
in A & y
in A by
Def1;
then x
= the
Element of X & y
= the
Element of X by
TARSKI:def 1;
hence thesis;
end;
end
registration
let X be
trivial
set;
cluster ->
trivial for
Subset of X;
coherence
proof
let Y be
Subset of X;
let x,y be
Element of Y;
per cases ;
suppose Y is non
empty;
then x
in Y & y
in Y by
Def1;
then x
in X & y
in X by
Lm1;
hence thesis by
ZFMISC_1:def 10;
end;
suppose Y is
empty;
then x
=
{} & y
=
{} by
Def1;
hence thesis;
end;
end;
end
registration
let X be non
trivial
set;
cluster non
trivial for
Subset of X;
existence
proof
take (
[#] X);
thus thesis;
end;
end
theorem ::
SUBSET_1:45
for D be
set, A be
Subset of D st A is non
trivial holds ex d1,d2 be
Element of D st d1
in A & d2
in A & d1
<> d2
proof
let D be
set, A be
Subset of D;
assume A is non
trivial;
then
consider d1,d2 be
object such that
A1: d1
in A & d2
in A and
A2: d1
<> d2;
reconsider d1, d2 as
set by
TARSKI: 1;
d1
in D & d2
in D by
A1,
Lm1;
then
reconsider d1, d2 as
Element of D by
Def1;
take d1, d2;
thus d1
in A & d2
in A & d1
<> d2 by
A1,
A2;
end;
theorem ::
SUBSET_1:46
Th46: for X be
trivial non
empty
set holds ex x be
Element of X st X
=
{x}
proof
let X be
trivial non
empty
set;
consider x be
object such that
A1: X
=
{x} by
ZFMISC_1: 131;
reconsider x as
set by
TARSKI: 1;
x
in X by
A1,
TARSKI:def 1;
then
reconsider x as
Element of X by
Def1;
take x;
thus X
=
{x} by
A1;
end;
theorem ::
SUBSET_1:47
for X be non
empty
set, A be non
empty
Subset of X holds A is
trivial implies ex x be
Element of X st A
=
{x}
proof
let X be non
empty
set, A be non
empty
Subset of X;
assume A is
trivial;
then ex s be
Element of A st A
=
{s} by
Th46;
hence thesis;
end;
theorem ::
SUBSET_1:48
for X be non
trivial
set, x be
Element of X holds ex y be
object st y
in X & x
<> y
proof
let X be non
trivial
set;
let x be
Element of X;
consider d1,d2 be
object such that
A1: d1
in X & d2
in X and
A2: d1
<> d2 by
ZFMISC_1:def 10;
x
<> d1 or x
<> d2 by
A2;
hence thesis by
A1;
end;
reserve x for
object;
definition
let x, X;
assume
A1: x
in X;
::
SUBSET_1:def8
func
In (x,X) ->
Element of X equals
:
Def7: x;
correctness
proof
reconsider x as
set by
TARSKI: 1;
x
in X by
A1;
hence thesis by
Def1;
end;
end
registration
let X be non
empty
set, x be
Element of X;
reduce (
In (x,X)) to x;
reducibility
proof
x
in X by
Def1;
hence thesis by
Def7;
end;
end
theorem ::
SUBSET_1:49
x
in (X
/\ Y) implies (
In (x,X))
= (
In (x,Y))
proof
assume
A1: x
in (X
/\ Y);
then
A2: x
in Y by
XBOOLE_0:def 4;
x
in X by
A1,
XBOOLE_0:def 4;
hence (
In (x,X))
= x by
Def7
.= (
In (x,Y)) by
A2,
Def7;
end;
theorem ::
SUBSET_1:50
for X be non
trivial
set, p be
set holds ex q be
Element of X st q
<> p
proof
let X be non
trivial
set, p be
set;
(X
\
{p}) is non
empty by
ZFMISC_1: 139;
then
consider q be
object such that
A1: q
in (X
\
{p});
reconsider q as
set by
TARSKI: 1;
(X
\
{p})
c= X by
XBOOLE_1: 36;
then q
in X by
A1;
then
reconsider q as
Element of X by
Def1;
take q;
thus thesis by
A1,
ZFMISC_1: 56;
end;
theorem ::
SUBSET_1:51
for T be non
trivial
set, X be non
trivial
Subset of T, p be
set holds ex q be
Element of T st q
in X & q
<> p
proof
let T be non
trivial
set, X be non
trivial
Subset of T, p be
set;
(X
\
{p}) is non
empty by
ZFMISC_1: 139;
then
consider q be
object such that
A1: q
in (X
\
{p});
reconsider q as
set by
TARSKI: 1;
q
in T by
A1,
Lm1;
then
reconsider q as
Element of T by
Def1;
take q;
thus thesis by
A1,
ZFMISC_1: 56;
end;
scheme ::
SUBSET_1:sch5
Union1 { A() ->
set , a() ->
Element of A() , F(
object) ->
set } :
(
union { F(j) where j be
Element of A() : j
in
{a()} })
= F(a);
set X = { F(j) where j be
Element of A() : j
in
{a()} };
for x be
object holds x
in F(a) iff ex Y be
set st x
in Y & Y
in X
proof
let x be
object;
thus x
in F(a) implies ex Y be
set st x
in Y & Y
in X
proof
assume
A1: x
in F(a);
take F(a);
thus x
in F(a) by
A1;
a()
in
{a()} by
TARSKI:def 1;
hence F(a)
in X;
end;
given Y be
set such that
A2: x
in Y and
A3: Y
in X;
ex j be
Element of A() st Y
= F(j) & j
in
{a()} by
A3;
hence x
in F(a) by
A2,
TARSKI:def 1;
end;
hence thesis by
TARSKI:def 4;
end;
scheme ::
SUBSET_1:sch6
Union2 { A() ->
set , a,b() ->
Element of A() , F(
object) ->
set } :
(
union { F(j) where j be
Element of A() : j
in
{a(), b()} })
= (F(a)
\/ F(b));
set X = { F(j) where j be
Element of A() : j
in
{a(), b()} };
for x be
object holds x
in (F(a)
\/ F(b)) iff ex Y be
set st x
in Y & Y
in X
proof
let x be
object;
thus x
in (F(a)
\/ F(b)) implies ex Y be
set st x
in Y & Y
in X
proof
assume x
in (F(a)
\/ F(b));
per cases by
XBOOLE_0:def 3;
suppose
A1: x
in F(a);
take F(a);
thus x
in F(a) by
A1;
a()
in
{a(), b()} by
TARSKI:def 2;
hence F(a)
in X;
end;
suppose
A2: x
in F(b);
take F(b);
thus x
in F(b) by
A2;
b()
in
{a(), b()} by
TARSKI:def 2;
hence F(b)
in X;
end;
end;
given Y be
set such that
A3: x
in Y and
A4: Y
in X;
consider j be
Element of A() such that
A5: Y
= F(j) and
A6: j
in
{a(), b()} by
A4;
now
per cases by
A6,
TARSKI:def 2;
case j
= a();
hence x
in F(a) by
A3,
A5;
end;
case j
= b();
hence x
in F(b) by
A3,
A5;
end;
end;
hence x
in (F(a)
\/ F(b)) by
XBOOLE_0:def 3;
end;
hence thesis by
TARSKI:def 4;
end;
theorem ::
SUBSET_1:52
X
<>
{} implies
{x1, x2, x3, x4, x5, x6, x7, x8, x9} is
Subset of X
proof
set A =
{x1, x2, x3, x4, x5, x6, x7, x8, x9};
assume
A1: X
<>
{} ;
A
c= X
proof
let x be
object;
x
in A implies x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6 or x
= x7 or x
= x8 or x
= x9 by
ENUMSET1:def 7;
hence thesis by
A1,
Def1;
end;
then A
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;
theorem ::
SUBSET_1:53
X
<>
{} implies
{x1, x2, x3, x4, x5, x6, x7, x8, x9, x10} is
Subset of X
proof
set A =
{x1, x2, x3, x4, x5, x6, x7, x8, x9, x10};
assume
A1: X
<>
{} ;
A
c= X
proof
let x be
object;
x
in A implies x
= x1 or x
= x2 or x
= x3 or x
= x4 or x
= x5 or x
= x6 or x
= x7 or x
= x8 or x
= x9 or x
= x10 by
ENUMSET1:def 8;
hence thesis by
A1,
Def1;
end;
then A
in (
bool X) by
ZFMISC_1:def 1;
hence thesis by
Def1;
end;