zfmisc_1.miz
begin
reserve u,v,x,x1,x2,y,y1,y2,z,p,a for
object,
A,B,X,X1,X2,X3,X4,Y,Y1,Y2,Z,N,M for
set;
Lm1:
{x}
c= X iff x
in X
proof
x
in
{x} by
TARSKI:def 1;
hence
{x}
c= X implies x
in X;
assume
A1: x
in X;
let y;
thus thesis by
A1,
TARSKI:def 1;
end;
Lm2: Y
c= X & not x
in Y implies Y
c= (X
\
{x})
proof
assume
A1: Y
c= X & not x
in Y;
let y;
assume y
in Y;
then y
in X & not y
in
{x} by
A1,
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 5;
end;
Lm3: Y
c=
{x} iff Y
=
{} or Y
=
{x}
proof
thus Y
c=
{x} implies Y
=
{} or Y
=
{x}
proof
assume
A1: Y
c=
{x};
x
in Y or not x
in Y;
then
{x}
c= Y or Y
c= (
{x}
\
{x}) by
A1,
Lm1,
Lm2;
then
{x}
= Y or Y
c=
{} by
A1,
XBOOLE_1: 37;
hence thesis by
XBOOLE_1: 3;
end;
thus thesis;
end;
definition
let X;
defpred
IT[
set] means $1
c= X;
::
ZFMISC_1:def1
func
bool X ->
set means
:
Def1: Z
in it iff Z
c= X;
existence
proof
consider M such that
A1: X
in M & for X, Y holds X
in M & Y
c= X implies Y
in M and for X st X
in M holds ex Z st Z
in M & for Y st Y
c= X holds Y
in Z and for X holds X
c= M implies (X,M)
are_equipotent or X
in M by
TARSKI_A: 1;
consider IT be
set such that
A2: Y
in IT iff Y
in M &
IT[Y] from
XFAMILY:sch 1;
take IT;
thus thesis by
A2,
A1;
end;
uniqueness
proof
thus for X1,X2 be
set st (for x be
set holds x
in X1 iff
IT[x]) & (for x be
set holds x
in X2 iff
IT[x]) holds X1
= X2 from
XFAMILY:sch 3;
end;
end
definition
let X1, X2;
defpred
X[
object] means ex x, y st x
in X1 & y
in X2 & $1
=
[x, y];
::
ZFMISC_1:def2
func
[:X1,X2:] ->
set means
:
Def2: z
in it iff ex x, y st x
in X1 & y
in X2 & z
=
[x, y];
existence
proof
A1: X1
c= (X1
\/ X2) by
XBOOLE_1: 7;
consider X such that
A2: for z holds z
in X iff z
in (
bool (
bool (X1
\/ X2))) &
X[z] from
XBOOLE_0:sch 1;
take X;
let z;
thus z
in X implies ex x, y st x
in X1 & y
in X2 & z
=
[x, y] by
A2;
given x, y such that
A3: x
in X1 and
A4: y
in X2 and
A5: z
=
[x, y];
{x, y}
c= (X1
\/ X2)
proof
let z;
assume z
in
{x, y};
then z
= x or z
= y by
TARSKI:def 2;
hence thesis by
A3,
A4,
XBOOLE_0:def 3;
end;
then
A6:
{x, y}
in (
bool (X1
\/ X2)) by
Def1;
{x}
c= (X1
\/ X2) by
A1,
A3,
Lm1;
then
A7:
{x}
in (
bool (X1
\/ X2)) by
Def1;
{
{x, y},
{x}}
c= (
bool (X1
\/ X2)) by
A7,
A6,
TARSKI:def 2;
then
{
{x, y},
{x}}
in (
bool (
bool (X1
\/ X2))) by
Def1;
hence thesis by
A2,
A3,
A4,
A5;
end;
uniqueness
proof
thus for X1,X2 be
set st (for x holds x
in X1 iff
X[x]) & (for x holds x
in X2 iff
X[x]) holds X1
= X2 from
XBOOLE_0:sch 3;
end;
end
definition
let X1, X2, X3;
::
ZFMISC_1:def3
func
[:X1,X2,X3:] ->
set equals
[:
[:X1, X2:], X3:];
coherence ;
end
definition
let X1, X2, X3, X4;
::
ZFMISC_1:def4
func
[:X1,X2,X3,X4:] ->
set equals
[:
[:X1, X2, X3:], X4:];
coherence ;
end
begin
theorem ::
ZFMISC_1:1
(
bool
{} )
=
{
{} }
proof
now
let x;
reconsider xx = x as
set by
TARSKI: 1;
xx
c=
{} iff x
=
{} by
XBOOLE_1: 3;
hence x
in (
bool
{} ) iff x
in
{
{} } by
Def1,
TARSKI:def 1;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ZFMISC_1:2
(
union
{} )
=
{}
proof
now
given x such that
A1: x
in (
union
{} );
ex X be
set st x
in X & X
in
{} by
A1,
TARSKI:def 4;
hence contradiction;
end;
hence thesis by
XBOOLE_0: 7;
end;
theorem ::
ZFMISC_1:3
Th3:
{x}
c=
{y} implies x
= y
proof
x
in
{x} by
TARSKI:def 1;
then
{x}
=
{y} implies x
= y by
TARSKI:def 1;
hence thesis by
Lm3;
end;
theorem ::
ZFMISC_1:4
Th4:
{x}
=
{y1, y2} implies x
= y1
proof
assume
{x}
=
{y1, y2};
then y1
in
{x} by
TARSKI:def 2;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:5
{x}
=
{y1, y2} implies y1
= y2
proof
assume
A1:
{x}
=
{y1, y2};
then x
= y1 by
Th4;
hence thesis by
A1,
Th4;
end;
theorem ::
ZFMISC_1:6
Th6:
{x1, x2}
=
{y1, y2} implies x1
= y1 or x1
= y2
proof
x1
in
{x1, x2} by
TARSKI:def 2;
hence thesis by
TARSKI:def 2;
end;
theorem ::
ZFMISC_1:7
Th7:
{x}
c=
{x, y}
proof
let z;
assume z
in
{x};
then z
= x by
TARSKI:def 1;
hence thesis by
TARSKI:def 2;
end;
Lm4: (
{x}
\/ X)
c= X implies x
in X
proof
assume
A1: (
{x}
\/ X)
c= X;
assume not x
in X;
then not x
in (
{x}
\/ X) by
A1;
then not x
in
{x} by
XBOOLE_0:def 3;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:8
(
{x}
\/
{y})
=
{x} implies x
= y
proof
assume (
{x}
\/
{y})
=
{x};
then y
in
{x} or x
in
{y} by
Lm4;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:9
(
{x}
\/
{x, y})
=
{x, y}
proof
x
in
{x, y} by
TARSKI:def 2;
hence thesis by
Lm1,
XBOOLE_1: 12;
end;
Lm5:
{x}
misses X implies not x
in X
proof
A1: x
in
{x} by
TARSKI:def 1;
assume (
{x}
/\ X)
=
{} & x
in X;
hence contradiction by
A1,
XBOOLE_0:def 4;
end;
theorem ::
ZFMISC_1:10
{x}
misses
{y} implies x
<> y;
Lm6: not x
in X implies
{x}
misses X
proof
assume
A1: not x
in X;
thus (
{x}
/\ X)
c=
{}
proof
let y;
assume y
in (
{x}
/\ X);
then y
in
{x} & y
in X by
XBOOLE_0:def 4;
hence thesis by
A1,
TARSKI:def 1;
end;
thus thesis;
end;
theorem ::
ZFMISC_1:11
Th11: x
<> y implies
{x}
misses
{y}
proof
assume x
<> y;
then not x
in
{y} by
TARSKI:def 1;
hence thesis by
Lm6;
end;
Lm7: (X
/\
{x})
=
{x} implies x
in X
proof
assume (X
/\
{x})
=
{x};
then x
in (X
/\
{x}) by
TARSKI:def 1;
hence thesis by
XBOOLE_0:def 4;
end;
theorem ::
ZFMISC_1:12
(
{x}
/\
{y})
=
{x} implies x
= y
proof
assume (
{x}
/\
{y})
=
{x};
then x
in
{y} or y
in
{x} by
Lm7;
hence thesis by
TARSKI:def 1;
end;
Lm8: x
in X implies (X
/\
{x})
=
{x} by
Lm1,
XBOOLE_1: 28;
theorem ::
ZFMISC_1:13
(
{x}
/\
{x, y})
=
{x}
proof
x
in
{x, y} by
TARSKI:def 2;
hence thesis by
Lm1,
XBOOLE_1: 28;
end;
Lm9: (
{x}
\ X)
=
{x} iff not x
in X by
Lm5,
Lm6,
XBOOLE_1: 83;
theorem ::
ZFMISC_1:14
(
{x}
\
{y})
=
{x} iff x
<> y
proof
(
{x}
\
{y})
=
{x} iff not x
in
{y} by
Lm5,
Lm6,
XBOOLE_1: 83;
hence thesis by
TARSKI:def 1;
end;
Lm10: (
{x}
\ X)
=
{} iff x
in X by
Lm1,
XBOOLE_1: 37;
theorem ::
ZFMISC_1:15
(
{x}
\
{y})
=
{} implies x
= y
proof
assume (
{x}
\
{y})
=
{} ;
then x
in
{y} by
Lm1,
XBOOLE_1: 37;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:16
(
{x}
\
{x, y})
=
{}
proof
x
in
{x, y} by
TARSKI:def 2;
hence thesis by
Lm1,
XBOOLE_1: 37;
end;
Lm11: (
{x, y}
\ X)
=
{x} iff not x
in X & (y
in X or x
= y)
proof
thus (
{x, y}
\ X)
=
{x} implies not x
in X & (y
in X or x
= y)
proof
assume
A1: (
{x, y}
\ X)
=
{x};
then x
in (
{x, y}
\ X) by
TARSKI:def 1;
hence not x
in X by
XBOOLE_0:def 5;
A2: y
in
{x, y} by
TARSKI:def 2;
assume not y
in X;
then y
in
{x} by
A1,
A2,
XBOOLE_0:def 5;
hence thesis by
TARSKI:def 1;
end;
assume
A3: ( not x
in X) & (y
in X or x
= y);
for z holds z
in (
{x, y}
\ X) iff z
= x
proof
let z;
z
in (
{x, y}
\ X) iff z
in
{x, y} & not z
in X by
XBOOLE_0:def 5;
hence thesis by
A3,
TARSKI:def 2;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:17
x
<> y implies (
{x, y}
\
{y})
=
{x}
proof
assume x
<> y;
then
A1: not x
in
{y} by
TARSKI:def 1;
y
in
{y} by
TARSKI:def 1;
hence thesis by
A1,
Lm11;
end;
theorem ::
ZFMISC_1:18
{x}
c=
{y} implies x
= y by
Th3;
theorem ::
ZFMISC_1:19
{z}
c=
{x, y} implies z
= x or z
= y
proof
A1: z
in
{z} by
TARSKI:def 1;
assume
{z}
c=
{x, y};
then z
in
{x, y} by
A1;
hence thesis by
TARSKI:def 2;
end;
theorem ::
ZFMISC_1:20
Th20:
{x, y}
c=
{z} implies x
= z
proof
A1: x
in
{x, y} by
TARSKI:def 2;
assume
{x, y}
c=
{z};
then x
in
{z} by
A1;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:21
{x, y}
c=
{z} implies
{x, y}
=
{z}
proof
assume
{x, y}
c=
{z};
then x
= z & y
= z by
Th20;
hence thesis by
ENUMSET1: 29;
end;
Lm12: X
<>
{x} & X
<>
{} implies ex y st y
in X & y
<> x
proof
assume that
A1: X
<>
{x} and
A2: X
<>
{} ;
per cases ;
suppose
A3: not x
in X;
consider y such that
A4: y
in X by
A2,
XBOOLE_0: 7;
take y;
thus thesis by
A3,
A4;
end;
suppose
A5: x
in X;
consider y such that
A6: y
in X & not y
in
{x} or y
in
{x} & not y
in X by
A1,
TARSKI: 2;
take y;
thus thesis by
A5,
A6,
TARSKI:def 1;
end;
end;
Lm13: Z
c=
{x1, x2} iff Z
=
{} or Z
=
{x1} or Z
=
{x2} or Z
=
{x1, x2}
proof
thus Z
c=
{x1, x2} implies Z
=
{} or Z
=
{x1} or Z
=
{x2} or Z
=
{x1, x2}
proof
assume that
A1: Z
c=
{x1, x2} and
A2: Z
<>
{} and
A3: Z
<>
{x1} and
A4: Z
<>
{x2};
now
let z;
thus z
in Z implies z
in
{x1, x2} by
A1;
A5:
now
assume
A6: not x1
in Z;
consider y such that
A7: y
in Z and
A8: y
<> x2 by
A2,
A4,
Lm12;
y
in
{x1, x2} by
A1,
A7;
hence contradiction by
A6,
A7,
A8,
TARSKI:def 2;
end;
A9:
now
assume
A10: not x2
in Z;
consider y such that
A11: y
in Z and
A12: y
<> x1 by
A2,
A3,
Lm12;
y
in
{x1, x2} by
A1,
A11;
hence contradiction by
A10,
A11,
A12,
TARSKI:def 2;
end;
assume z
in
{x1, x2};
hence z
in Z by
A5,
A9,
TARSKI:def 2;
end;
hence thesis by
TARSKI: 2;
end;
thus thesis by
Th7;
end;
theorem ::
ZFMISC_1:22
{x1, x2}
c=
{y1, y2} implies x1
= y1 or x1
= y2
proof
assume
{x1, x2}
c=
{y1, y2};
then
{x1, x2}
=
{} or
{x1, x2}
=
{y1} or
{x1, x2}
=
{y2} or
{x1, x2}
=
{y1, y2} by
Lm13;
hence thesis by
Th4,
Th6;
end;
theorem ::
ZFMISC_1:23
x
<> y implies (
{x}
\+\
{y})
=
{x, y}
proof
assume
A1: x
<> y;
for z holds z
in (
{x}
\+\
{y}) iff z
= x or z
= y
proof
let z;
A2: z
in
{y} iff z
= y by
TARSKI:def 1;
z
in
{x} iff z
= x by
TARSKI:def 1;
hence thesis by
A1,
A2,
XBOOLE_0: 1;
end;
hence thesis by
TARSKI:def 2;
end;
theorem ::
ZFMISC_1:24
(
bool
{x})
=
{
{} ,
{x}}
proof
now
let y;
reconsider yy = y as
set by
TARSKI: 1;
yy
c=
{x} iff y
=
{} or y
=
{x} by
Lm3;
hence y
in (
bool
{x}) iff y
in
{
{} ,
{x}} by
Def1,
TARSKI:def 2;
end;
hence thesis by
TARSKI: 2;
end;
Lm14: X
in A implies X
c= (
union A) by
TARSKI:def 4;
registration
let x be
object;
reduce (
union
{x}) to x;
reducibility
proof
reconsider X = x as
set by
TARSKI: 1;
A1: (
union
{X})
c= X
proof
let y;
assume y
in (
union
{X});
then ex Y be
set st y
in Y & Y
in
{X} by
TARSKI:def 4;
hence thesis by
TARSKI:def 1;
end;
X
in
{X} by
TARSKI:def 1;
then X
c= (
union
{X}) by
Lm14;
hence thesis by
A1,
XBOOLE_0:def 10;
end;
end
theorem ::
ZFMISC_1:25
(
union
{x})
= x;
Lm15: (
union
{X, Y})
= (X
\/ Y)
proof
x
in (
union
{X, Y}) iff x
in X or x
in Y
proof
thus x
in (
union
{X, Y}) implies x
in X or x
in Y
proof
assume x
in (
union
{X, Y});
then ex Z st x
in Z & Z
in
{X, Y} by
TARSKI:def 4;
hence thesis by
TARSKI:def 2;
end;
X
in
{X, Y} & Y
in
{X, Y} by
TARSKI:def 2;
hence thesis by
TARSKI:def 4;
end;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
ZFMISC_1:26
(
union
{
{x},
{y}})
=
{x, y}
proof
thus (
union
{
{x},
{y}})
= (
{x}
\/
{y}) by
Lm15
.=
{x, y} by
ENUMSET1: 1;
end;
Lm16:
[x, y]
in
[:X, Y:] iff x
in X & y
in Y
proof
thus
[x, y]
in
[:X, Y:] implies x
in X & y
in Y
proof
assume
[x, y]
in
[:X, Y:];
then ex x1, y1 st x1
in X & y1
in Y &
[x, y]
=
[x1, y1] by
Def2;
hence thesis by
XTUPLE_0: 1;
end;
thus thesis by
Def2;
end;
::$Canceled
theorem ::
ZFMISC_1:28
[x, y]
in
[:
{x1},
{y1}:] iff x
= x1 & y
= y1
proof
x
= x1 & y
= y1 iff x
in
{x1} & y
in
{y1} by
TARSKI:def 1;
hence thesis by
Lm16;
end;
theorem ::
ZFMISC_1:29
Th28:
[:
{x},
{y}:]
=
{
[x, y]}
proof
now
let z;
thus z
in
[:
{x},
{y}:] implies z
in
{
[x, y]}
proof
assume z
in
[:
{x},
{y}:];
then
consider x1, y1 such that
A1: x1
in
{x} & y1
in
{y} and
A2: z
=
[x1, y1] by
Def2;
x1
= x & y1
= y by
A1,
TARSKI:def 1;
hence thesis by
A2,
TARSKI:def 1;
end;
assume z
in
{
[x, y]};
then
A3: z
=
[x, y] by
TARSKI:def 1;
x
in
{x} & y
in
{y} by
TARSKI:def 1;
hence z
in
[:
{x},
{y}:] by
A3,
Lm16;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ZFMISC_1:30
Th29:
[:
{x},
{y, z}:]
=
{
[x, y],
[x, z]} &
[:
{x, y},
{z}:]
=
{
[x, z],
[y, z]}
proof
now
let v;
A1: z
in
{y, z} by
TARSKI:def 2;
thus v
in
[:
{x},
{y, z}:] implies v
in
{
[x, y],
[x, z]}
proof
assume v
in
[:
{x},
{y, z}:];
then
consider x1, y1 such that
A2: x1
in
{x} and
A3: y1
in
{y, z} and
A4: v
=
[x1, y1] by
Def2;
A5: y1
= y or y1
= z by
A3,
TARSKI:def 2;
x1
= x by
A2,
TARSKI:def 1;
hence thesis by
A4,
A5,
TARSKI:def 2;
end;
assume v
in
{
[x, y],
[x, z]};
then
A6: v
=
[x, y] or v
=
[x, z] by
TARSKI:def 2;
x
in
{x} & y
in
{y, z} by
TARSKI:def 1,
TARSKI:def 2;
hence v
in
[:
{x},
{y, z}:] by
A6,
A1,
Lm16;
end;
hence
[:
{x},
{y, z}:]
=
{
[x, y],
[x, z]} by
TARSKI: 2;
now
let v;
A7: z
in
{z} by
TARSKI:def 1;
thus v
in
[:
{x, y},
{z}:] implies v
in
{
[x, z],
[y, z]}
proof
assume v
in
[:
{x, y},
{z}:];
then
consider x1, y1 such that
A8: x1
in
{x, y} and
A9: y1
in
{z} and
A10: v
=
[x1, y1] by
Def2;
A11: x1
= x or x1
= y by
A8,
TARSKI:def 2;
y1
= z by
A9,
TARSKI:def 1;
hence thesis by
A10,
A11,
TARSKI:def 2;
end;
assume v
in
{
[x, z],
[y, z]};
then
A12: v
=
[x, z] or v
=
[y, z] by
TARSKI:def 2;
x
in
{x, y} & y
in
{x, y} by
TARSKI:def 2;
hence v
in
[:
{x, y},
{z}:] by
A12,
A7,
Lm16;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ZFMISC_1:31
{x}
c= X iff x
in X by
Lm1;
theorem ::
ZFMISC_1:32
Th31:
{x1, x2}
c= Z iff x1
in Z & x2
in Z
proof
x1
in
{x1, x2} & x2
in
{x1, x2} by
TARSKI:def 2;
hence
{x1, x2}
c= Z implies x1
in Z & x2
in Z;
assume
A1: x1
in Z & x2
in Z;
let z;
assume z
in
{x1, x2};
hence thesis by
A1,
TARSKI:def 2;
end;
theorem ::
ZFMISC_1:33
Y
c=
{x} iff Y
=
{} or Y
=
{x} by
Lm3;
theorem ::
ZFMISC_1:34
Y
c= X & not x
in Y implies Y
c= (X
\
{x}) by
Lm2;
theorem ::
ZFMISC_1:35
X
<>
{x} & X
<>
{} implies ex y st y
in X & y
<> x by
Lm12;
theorem ::
ZFMISC_1:36
Z
c=
{x1, x2} iff Z
=
{} or Z
=
{x1} or Z
=
{x2} or Z
=
{x1, x2} by
Lm13;
theorem ::
ZFMISC_1:37
Th36:
{z}
= (X
\/ Y) implies X
=
{z} & Y
=
{z} or X
=
{} & Y
=
{z} or X
=
{z} & Y
=
{}
proof
assume
A1:
{z}
= (X
\/ Y);
X
<>
{} or Y
<>
{} by
A1;
hence thesis by
A1,
Lm3,
XBOOLE_1: 7;
end;
theorem ::
ZFMISC_1:38
{z}
= (X
\/ Y) & X
<> Y implies X
=
{} or Y
=
{}
proof
assume
{z}
= (X
\/ Y);
then X
=
{z} & Y
=
{z} or X
=
{} & Y
=
{z} or X
=
{z} & Y
=
{} by
Th36;
hence thesis;
end;
theorem ::
ZFMISC_1:39
(
{x}
\/ X)
c= X implies x
in X by
Lm4;
theorem ::
ZFMISC_1:40
x
in X implies (
{x}
\/ X)
= X by
Lm1,
XBOOLE_1: 12;
theorem ::
ZFMISC_1:41
(
{x, y}
\/ Z)
c= Z implies x
in Z
proof
assume
A1: (
{x, y}
\/ Z)
c= Z;
assume not x
in Z;
then not x
in (
{x, y}
\/ Z) by
A1;
then not x
in
{x, y} by
XBOOLE_0:def 3;
hence thesis by
TARSKI:def 2;
end;
theorem ::
ZFMISC_1:42
x
in Z & y
in Z implies (
{x, y}
\/ Z)
= Z by
Th31,
XBOOLE_1: 12;
theorem ::
ZFMISC_1:43
(
{x}
\/ X)
<>
{} ;
theorem ::
ZFMISC_1:44
(
{x, y}
\/ X)
<>
{} ;
theorem ::
ZFMISC_1:45
(X
/\
{x})
=
{x} implies x
in X by
Lm7;
theorem ::
ZFMISC_1:46
x
in X implies (X
/\
{x})
=
{x} by
Lm1,
XBOOLE_1: 28;
theorem ::
ZFMISC_1:47
x
in Z & y
in Z implies (
{x, y}
/\ Z)
=
{x, y} by
Th31,
XBOOLE_1: 28;
theorem ::
ZFMISC_1:48
{x}
misses X implies not x
in X by
Lm5;
theorem ::
ZFMISC_1:49
Th48:
{x, y}
misses Z implies not x
in Z
proof
A1: x
in
{x, y} by
TARSKI:def 2;
assume (
{x, y}
/\ Z)
=
{} & x
in Z;
hence contradiction by
A1,
XBOOLE_0:def 4;
end;
theorem ::
ZFMISC_1:50
not x
in X implies
{x}
misses X by
Lm6;
theorem ::
ZFMISC_1:51
Th50: not x
in Z & not y
in Z implies
{x, y}
misses Z
proof
assume
A1: ( not x
in Z) & not y
in Z;
assume
{x, y}
meets Z;
then
consider z such that
A2: z
in (
{x, y}
/\ Z) by
XBOOLE_0: 4;
z
in
{x, y} & z
in Z by
A2,
XBOOLE_0:def 4;
hence contradiction by
A1,
TARSKI:def 2;
end;
theorem ::
ZFMISC_1:52
{x}
misses X or (
{x}
/\ X)
=
{x} by
Lm6,
Lm8;
theorem ::
ZFMISC_1:53
(
{x, y}
/\ X)
=
{x} implies not y
in X or x
= y
proof
A1: y
in
{x, y} by
TARSKI:def 2;
assume (
{x, y}
/\ X)
=
{x} & y
in X;
then y
in
{x} by
A1,
XBOOLE_0:def 4;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:54
x
in X & ( not y
in X or x
= y) implies (
{x, y}
/\ X)
=
{x}
proof
assume
A1: x
in X & ( not y
in X or x
= y);
for z holds z
in (
{x, y}
/\ X) iff z
= x
proof
let z be
object;
z
in (
{x, y}
/\ X) iff z
in
{x, y} & z
in X by
XBOOLE_0:def 4;
hence thesis by
A1,
TARSKI:def 2;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:55
(
{x, y}
/\ X)
=
{x, y} implies x
in X
proof
assume (
{x, y}
/\ X)
=
{x, y};
then x
in (
{x, y}
/\ X) & y
in (
{x, y}
/\ X) or x
in (X
/\
{x, y}) & y
in (X
/\
{x, y}) by
TARSKI:def 2;
hence thesis by
XBOOLE_0:def 4;
end;
theorem ::
ZFMISC_1:56
Th55: z
in (X
\
{x}) iff z
in X & z
<> x
proof
z
in (X
\
{x}) iff z
in X & not z
in
{x} by
XBOOLE_0:def 5;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:57
Th56: (X
\
{x})
= X iff not x
in X
proof
(X
\
{x})
= X iff X
misses
{x} by
XBOOLE_1: 83;
hence thesis by
Lm5,
Lm6;
end;
theorem ::
ZFMISC_1:58
(X
\
{x})
=
{} implies X
=
{} or X
=
{x}
proof
assume (X
\
{x})
=
{} ;
then X
c=
{x} by
XBOOLE_1: 37;
hence thesis by
Lm3;
end;
theorem ::
ZFMISC_1:59
(
{x}
\ X)
=
{x} iff not x
in X by
Lm5,
Lm6,
XBOOLE_1: 83;
theorem ::
ZFMISC_1:60
(
{x}
\ X)
=
{} iff x
in X by
Lm1,
XBOOLE_1: 37;
theorem ::
ZFMISC_1:61
(
{x}
\ X)
=
{} or (
{x}
\ X)
=
{x} by
Lm9,
Lm10;
theorem ::
ZFMISC_1:62
(
{x, y}
\ X)
=
{x} iff not x
in X & (y
in X or x
= y) by
Lm11;
theorem ::
ZFMISC_1:63
(
{x, y}
\ X)
=
{x, y} iff not x
in X & not y
in X by
Th48,
Th50,
XBOOLE_1: 83;
theorem ::
ZFMISC_1:64
Th63: (
{x, y}
\ X)
=
{} iff x
in X & y
in X
proof
(
{x, y}
\ X)
=
{} iff
{x, y}
c= X by
XBOOLE_1: 37;
hence thesis by
Th31;
end;
theorem ::
ZFMISC_1:65
(
{x, y}
\ X)
=
{} or (
{x, y}
\ X)
=
{x} or (
{x, y}
\ X)
=
{y} or (
{x, y}
\ X)
=
{x, y}
proof
assume that
A1: (
{x, y}
\ X)
<>
{} and
A2: (
{x, y}
\ X)
<>
{x} and
A3: (
{x, y}
\ X)
<>
{y};
A4: not x
in X & x
<> y or y
in X by
A3,
Lm11;
x
in X or not y
in X & x
<> y by
A2,
Lm11;
hence thesis by
A1,
A4,
Th50,
Th63,
XBOOLE_1: 83;
end;
theorem ::
ZFMISC_1:66
(X
\
{x, y})
=
{} iff X
=
{} or X
=
{x} or X
=
{y} or X
=
{x, y}
proof
(X
\
{x, y})
=
{} iff X
c=
{x, y} by
XBOOLE_1: 37;
hence thesis by
Lm13;
end;
theorem ::
ZFMISC_1:67
A
c= B implies (
bool A)
c= (
bool B)
proof
assume
A1: A
c= B;
let x;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in (
bool A);
then xx
c= A by
Def1;
then xx
c= B by
A1;
hence thesis by
Def1;
end;
theorem ::
ZFMISC_1:68
{A}
c= (
bool A)
proof
A
in (
bool A) by
Def1;
hence thesis by
Lm1;
end;
theorem ::
ZFMISC_1:69
((
bool A)
\/ (
bool B))
c= (
bool (A
\/ B))
proof
let x;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in ((
bool A)
\/ (
bool B));
then x
in (
bool A) or x
in (
bool B) by
XBOOLE_0:def 3;
then
A1: xx
c= A or xx
c= B by
Def1;
A
c= (A
\/ B) & B
c= (A
\/ B) by
XBOOLE_1: 7;
then xx
c= (A
\/ B) by
A1;
hence thesis by
Def1;
end;
theorem ::
ZFMISC_1:70
((
bool A)
\/ (
bool B))
= (
bool (A
\/ B)) implies (A,B)
are_c=-comparable
proof
assume
A1: ((
bool A)
\/ (
bool B))
= (
bool (A
\/ B));
(A
\/ B)
in (
bool (A
\/ B)) by
Def1;
then (A
\/ B)
in (
bool A) or (A
\/ B)
in (
bool B) by
A1,
XBOOLE_0:def 3;
then
A2: (A
\/ B)
c= A or (A
\/ B)
c= B by
Def1;
A
c= (A
\/ B) & B
c= (A
\/ B) by
XBOOLE_1: 7;
hence A
c= B or B
c= A by
A2;
end;
theorem ::
ZFMISC_1:71
(
bool (A
/\ B))
= ((
bool A)
/\ (
bool B))
proof
now
let x;
reconsider xx = x as
set by
TARSKI: 1;
(A
/\ B)
c= A & (A
/\ B)
c= B by
XBOOLE_1: 17;
then xx
c= A & xx
c= B iff xx
c= (A
/\ B) by
XBOOLE_1: 19;
then x
in (
bool A) & x
in (
bool B) iff x
in (
bool (A
/\ B)) by
Def1;
hence x
in (
bool (A
/\ B)) iff x
in ((
bool A)
/\ (
bool B)) by
XBOOLE_0:def 4;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ZFMISC_1:72
(
bool (A
\ B))
c= (
{
{} }
\/ ((
bool A)
\ (
bool B)))
proof
let x;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in (
bool (A
\ B));
then
A1: xx
c= (A
\ B) by
Def1;
then xx
misses B by
XBOOLE_1: 63,
XBOOLE_1: 79;
then (A
\ B)
c= A & (xx
/\ B)
=
{} by
XBOOLE_1: 36;
then x
=
{} or xx
c= A & not xx
c= B by
A1,
XBOOLE_1: 28;
then x
in
{
{} } or x
in (
bool A) & not x
in (
bool B) by
Def1,
TARSKI:def 1;
then x
in
{
{} } or x
in ((
bool A)
\ (
bool B)) by
XBOOLE_0:def 5;
hence thesis by
XBOOLE_0:def 3;
end;
theorem ::
ZFMISC_1:73
((
bool (A
\ B))
\/ (
bool (B
\ A)))
c= (
bool (A
\+\ B))
proof
let x;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in ((
bool (A
\ B))
\/ (
bool (B
\ A)));
then x
in (
bool (A
\ B)) or x
in (
bool (B
\ A)) by
XBOOLE_0:def 3;
then
A1: xx
c= (A
\ B) or xx
c= (B
\ A) by
Def1;
xx
c= ((A
\ B)
\/ (B
\ A))
proof
let z;
assume z
in xx;
then z
in (A
\ B) or z
in (B
\ A) by
A1;
hence thesis by
XBOOLE_0:def 3;
end;
hence thesis by
Def1;
end;
theorem ::
ZFMISC_1:74
X
in A implies X
c= (
union A) by
Lm14;
theorem ::
ZFMISC_1:75
(
union
{X, Y})
= (X
\/ Y) by
Lm15;
theorem ::
ZFMISC_1:76
(for X st X
in A holds X
c= Z) implies (
union A)
c= Z
proof
assume
A1: for X st X
in A holds X
c= Z;
let y;
assume y
in (
union A);
then
consider Y such that
A2: y
in Y and
A3: Y
in A by
TARSKI:def 4;
Y
c= Z by
A1,
A3;
hence thesis by
A2;
end;
theorem ::
ZFMISC_1:77
Th76: A
c= B implies (
union A)
c= (
union B)
proof
assume
A1: A
c= B;
let x;
assume x
in (
union A);
then
consider Y such that
A2: x
in Y and
A3: Y
in A by
TARSKI:def 4;
Y
in B by
A1,
A3;
hence thesis by
A2,
TARSKI:def 4;
end;
theorem ::
ZFMISC_1:78
(
union (A
\/ B))
= ((
union A)
\/ (
union B))
proof
A1: (
union (A
\/ B))
c= ((
union A)
\/ (
union B))
proof
let x;
assume x
in (
union (A
\/ B));
then
consider Y such that
A2: x
in Y and
A3: Y
in (A
\/ B) by
TARSKI:def 4;
Y
in A or Y
in B by
A3,
XBOOLE_0:def 3;
then x
in (
union A) or x
in (
union B) by
A2,
TARSKI:def 4;
hence thesis by
XBOOLE_0:def 3;
end;
(
union A)
c= (
union (A
\/ B)) & (
union B)
c= (
union (A
\/ B)) by
Th76,
XBOOLE_1: 7;
hence thesis by
A1,
XBOOLE_1: 8;
end;
theorem ::
ZFMISC_1:79
Th78: (
union (A
/\ B))
c= ((
union A)
/\ (
union B))
proof
let x;
assume x
in (
union (A
/\ B));
then
consider Y such that
A1: x
in Y and
A2: Y
in (A
/\ B) by
TARSKI:def 4;
Y
in B by
A2,
XBOOLE_0:def 4;
then
A3: x
in (
union B) by
A1,
TARSKI:def 4;
Y
in A by
A2,
XBOOLE_0:def 4;
then x
in (
union A) by
A1,
TARSKI:def 4;
hence thesis by
A3,
XBOOLE_0:def 4;
end;
theorem ::
ZFMISC_1:80
Th79: (for X st X
in A holds X
misses B) implies (
union A)
misses B
proof
assume
A1: for X st X
in A holds X
misses B;
assume (
union A)
meets B;
then
consider z such that
A2: z
in ((
union A)
/\ B) by
XBOOLE_0: 4;
z
in (
union A) by
A2,
XBOOLE_0:def 4;
then
consider X such that
A3: z
in X and
A4: X
in A by
TARSKI:def 4;
z
in B by
A2,
XBOOLE_0:def 4;
then z
in (X
/\ B) by
A3,
XBOOLE_0:def 4;
hence contradiction by
A1,
A4,
XBOOLE_0: 4;
end;
theorem ::
ZFMISC_1:81
(
union (
bool A))
= A
proof
now
let x;
thus x
in (
union (
bool A)) implies x
in A
proof
assume x
in (
union (
bool A));
then
consider X such that
A1: x
in X and
A2: X
in (
bool A) by
TARSKI:def 4;
X
c= A by
A2,
Def1;
hence thesis by
A1;
end;
assume x
in A;
then
{x}
c= A by
Lm1;
then
A3:
{x}
in (
bool A) by
Def1;
x
in
{x} by
TARSKI:def 1;
hence x
in (
union (
bool A)) by
A3,
TARSKI:def 4;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ZFMISC_1:82
A
c= (
bool (
union A))
proof
let x;
reconsider xx = x as
set by
TARSKI: 1;
assume x
in A;
then xx
c= (
union A) by
Lm14;
hence thesis by
Def1;
end;
theorem ::
ZFMISC_1:83
(for X, Y st X
<> Y & X
in (A
\/ B) & Y
in (A
\/ B) holds X
misses Y) implies (
union (A
/\ B))
= ((
union A)
/\ (
union B))
proof
assume
A1: for X, Y st X
<> Y & X
in (A
\/ B) & Y
in (A
\/ B) holds X
misses Y;
((
union A)
/\ (
union B))
c= (
union (A
/\ B))
proof
let x;
assume
A2: x
in ((
union A)
/\ (
union B));
then x
in (
union A) by
XBOOLE_0:def 4;
then
consider X such that
A3: x
in X and
A4: X
in A by
TARSKI:def 4;
x
in (
union B) by
A2,
XBOOLE_0:def 4;
then
consider Y such that
A5: x
in Y and
A6: Y
in B by
TARSKI:def 4;
now
A7: x
in (X
/\ Y) by
A3,
A5,
XBOOLE_0:def 4;
assume
A8: X
<> Y;
X
in (A
\/ B) & Y
in (A
\/ B) by
A4,
A6,
XBOOLE_0:def 3;
hence contradiction by
A1,
A8,
A7,
XBOOLE_0: 4;
end;
then Y
in (A
/\ B) by
A4,
A6,
XBOOLE_0:def 4;
hence thesis by
A5,
TARSKI:def 4;
end;
hence thesis by
Th78;
end;
theorem ::
ZFMISC_1:84
Th83: A
c=
[:X, Y:] & z
in A implies ex x, y st x
in X & y
in Y & z
=
[x, y]
proof
assume A
c=
[:X, Y:] & z
in A;
then z
in
[:X, Y:];
hence thesis by
Def2;
end;
theorem ::
ZFMISC_1:85
Th84: z
in (
[:X1, Y1:]
/\
[:X2, Y2:]) implies ex x, y st z
=
[x, y] & x
in (X1
/\ X2) & y
in (Y1
/\ Y2)
proof
assume
A1: z
in (
[:X1, Y1:]
/\
[:X2, Y2:]);
then z
in
[:X1, Y1:] by
XBOOLE_0:def 4;
then
consider x1, y1 such that
A2: x1
in X1 and
A3: y1
in Y1 and
A4: z
=
[x1, y1] by
Def2;
z
in
[:X2, Y2:] by
A1,
XBOOLE_0:def 4;
then
consider x2, y2 such that
A5: x2
in X2 and
A6: y2
in Y2 and
A7: z
=
[x2, y2] by
Def2;
y1
= y2 by
A4,
A7,
XTUPLE_0: 1;
then
A8: y1
in (Y1
/\ Y2) by
A3,
A6,
XBOOLE_0:def 4;
x1
= x2 by
A4,
A7,
XTUPLE_0: 1;
then x1
in (X1
/\ X2) by
A2,
A5,
XBOOLE_0:def 4;
hence thesis by
A4,
A8;
end;
theorem ::
ZFMISC_1:86
[:X, Y:]
c= (
bool (
bool (X
\/ Y)))
proof
let z;
reconsider zz = z as
set by
TARSKI: 1;
assume z
in
[:X, Y:];
then
consider x, y such that
A1: x
in X and
A2: y
in Y and
A3: z
=
[x, y] by
Def2;
zz
c= (
bool (X
\/ Y))
proof
let u;
assume u
in zz;
then
A4: u
=
{x, y} or u
=
{x} by
A3,
TARSKI:def 2;
X
c= (X
\/ Y) &
{x}
c= X by
A1,
Lm1,
XBOOLE_1: 7;
then
A5:
{x}
c= (X
\/ Y);
x
in (X
\/ Y) & y
in (X
\/ Y) by
A1,
A2,
XBOOLE_0:def 3;
then
{x, y}
c= (X
\/ Y) by
Th31;
hence thesis by
A5,
A4,
Def1;
end;
hence thesis by
Def1;
end;
theorem ::
ZFMISC_1:87
for x,y be
object holds
[x, y]
in
[:X, Y:] iff x
in X & y
in Y by
Lm16;
theorem ::
ZFMISC_1:88
Th87:
[x, y]
in
[:X, Y:] implies
[y, x]
in
[:Y, X:]
proof
[x, y]
in
[:X, Y:] implies x
in X & y
in Y by
Lm16;
hence thesis by
Lm16;
end;
theorem ::
ZFMISC_1:89
(for x, y holds
[x, y]
in
[:X1, Y1:] iff
[x, y]
in
[:X2, Y2:]) implies
[:X1, Y1:]
=
[:X2, Y2:]
proof
assume
A1: for x, y holds
[x, y]
in
[:X1, Y1:] iff
[x, y]
in
[:X2, Y2:];
now
let z;
thus z
in
[:X1, Y1:] implies z
in
[:X2, Y2:]
proof
assume
A2: z
in
[:X1, Y1:];
then ex x, y st x
in X1 & y
in Y1 &
[x, y]
= z by
Def2;
hence thesis by
A1,
A2;
end;
assume
A3: z
in
[:X2, Y2:];
then ex x, y st x
in X2 & y
in Y2 &
[x, y]
= z by
Def2;
hence z
in
[:X1, Y1:] by
A1,
A3;
end;
hence thesis by
TARSKI: 2;
end;
Lm17: A
c=
[:X1, Y1:] & B
c=
[:X2, Y2:] & (for x, y holds
[x, y]
in A iff
[x, y]
in B) implies A
= B
proof
assume that
A1: A
c=
[:X1, Y1:] and
A2: B
c=
[:X2, Y2:] and
A3: for x, y holds
[x, y]
in A iff
[x, y]
in B;
now
let z;
A4: z
in B implies ex x, y st x
in X2 & y
in Y2 & z
=
[x, y] by
A2,
Th83;
z
in A implies ex x, y st x
in X1 & y
in Y1 & z
=
[x, y] by
A1,
Th83;
hence z
in A iff z
in B by
A3,
A4;
end;
hence thesis by
TARSKI: 2;
end;
Lm18: (for z st z
in A holds ex x, y st z
=
[x, y]) & (for z st z
in B holds ex x, y st z
=
[x, y]) & (for x, y holds
[x, y]
in A iff
[x, y]
in B) implies A
= B
proof
assume that
A1: for z st z
in A holds ex x, y st z
=
[x, y] and
A2: for z st z
in B holds ex x, y st z
=
[x, y] and
A3: for x, y holds
[x, y]
in A iff
[x, y]
in B;
now
let z;
A4: z
in B implies ex x, y st z
=
[x, y] by
A2;
z
in A implies ex x, y st z
=
[x, y] by
A1;
hence z
in A iff z
in B by
A3,
A4;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ZFMISC_1:90
Th89:
[:X, Y:]
=
{} iff X
=
{} or Y
=
{}
proof
thus
[:X, Y:]
=
{} implies X
=
{} or Y
=
{}
proof
assume
A1:
[:X, Y:]
=
{} ;
assume X
<>
{} ;
then
consider x such that
A2: x
in X by
XBOOLE_0: 7;
assume Y
<>
{} ;
then
consider y such that
A3: y
in Y by
XBOOLE_0: 7;
[x, y]
in
[:X, Y:] by
A2,
A3,
Def2;
hence contradiction by
A1;
end;
assume
A4: not thesis;
then
consider z such that
A5: z
in
[:X, Y:] by
XBOOLE_0: 7;
ex x, y st x
in X & y
in Y &
[x, y]
= z by
A5,
Def2;
hence contradiction by
A4;
end;
theorem ::
ZFMISC_1:91
X
<>
{} & Y
<>
{} &
[:X, Y:]
=
[:Y, X:] implies X
= Y
proof
assume X
<>
{} ;
then
consider x such that
A1: x
in X by
XBOOLE_0: 7;
assume Y
<>
{} ;
then
consider y such that
A2: y
in Y by
XBOOLE_0: 7;
assume
A3:
[:X, Y:]
=
[:Y, X:];
for z holds z
in X iff z
in Y
proof
let z;
thus z
in X implies z
in Y
proof
assume z
in X;
then
[z, y]
in
[:Y, X:] by
A2,
A3,
Lm16;
hence thesis by
Lm16;
end;
assume z
in Y;
then
[z, x]
in
[:X, Y:] by
A1,
A3,
Lm16;
hence thesis by
Lm16;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ZFMISC_1:92
[:X, X:]
=
[:Y, Y:] implies X
= Y
proof
assume
A1:
[:X, X:]
=
[:Y, Y:];
for x holds x
in X iff x
in Y
proof
let x;
x
in X iff
[x, x]
in
[:X, X:] by
Lm16;
hence thesis by
A1,
Lm16;
end;
hence thesis by
TARSKI: 2;
end;
Lm19: z
in
[:X, Y:] implies ex x, y st
[x, y]
= z
proof
assume z
in
[:X, Y:];
then ex x, y st x
in X & y
in Y &
[x, y]
= z by
Def2;
hence thesis;
end;
theorem ::
ZFMISC_1:93
X
c=
[:X, Y:] implies X
=
{}
proof
assume
A1: X
c=
[:X, Y:];
assume X
<>
{} ;
then
consider z such that
A2: z
in X by
XBOOLE_0: 7;
consider M such that
A3: M
in (X
\/ (
union X)) and
A4: (X
\/ (
union X))
misses M by
A2,
XREGULAR: 1;
now
assume
A5: M
in X;
then
consider x, y such that
A6: M
=
[x, y] by
Lm19,
A1;
A7:
{x}
in M by
A6,
TARSKI:def 2;
M
c= (
union X) by
A5,
Lm14;
then
{x}
in (
union X) by
A7;
then
{x}
in (X
\/ (
union X)) by
XBOOLE_0:def 3;
hence contradiction by
A4,
A7,
XBOOLE_0: 3;
end;
then M
in (
union X) by
A3,
XBOOLE_0:def 3;
then
consider Z such that
A8: M
in Z and
A9: Z
in X by
TARSKI:def 4;
Z
in
[:X, Y:] by
A1,
A9;
then
consider x, y such that
A10: x
in X and y
in Y and
A11: Z
=
[x, y] by
Def2;
M
=
{x} or M
=
{x, y} by
A8,
A11,
TARSKI:def 2;
then
A12: x
in M by
TARSKI:def 1,
TARSKI:def 2;
x
in (X
\/ (
union X)) by
A10,
XBOOLE_0:def 3;
hence contradiction by
A4,
A12,
XBOOLE_0: 3;
end;
theorem ::
ZFMISC_1:94
Z
<>
{} & (
[:X, Z:]
c=
[:Y, Z:] or
[:Z, X:]
c=
[:Z, Y:]) implies X
c= Y
proof
assume Z
<>
{} ;
then
consider z such that
A1: z
in Z by
XBOOLE_0: 7;
assume
A2:
[:X, Z:]
c=
[:Y, Z:] or
[:Z, X:]
c=
[:Z, Y:];
let x;
assume x
in X;
then
[x, z]
in
[:X, Z:] &
[z, x]
in
[:Z, X:] by
A1,
Def2;
then
[x, z]
in
[:Y, Z:] or
[z, x]
in
[:Z, Y:] by
A2;
hence thesis by
Lm16;
end;
theorem ::
ZFMISC_1:95
Th94: X
c= Y implies
[:X, Z:]
c=
[:Y, Z:] &
[:Z, X:]
c=
[:Z, Y:]
proof
assume
A1: X
c= Y;
thus
[:X, Z:]
c=
[:Y, Z:]
proof
let z;
assume z
in
[:X, Z:];
then
consider x, y such that
A2: x
in X and
A3: y
in Z & z
=
[x, y] by
Def2;
x
in Y by
A1,
A2;
hence thesis by
A3,
Def2;
end;
let z;
assume z
in
[:Z, X:];
then
consider y, x such that
A4: y
in Z and
A5: x
in X and
A6: z
=
[y, x] by
Def2;
x
in Y by
A1,
A5;
hence thesis by
A4,
A6,
Def2;
end;
theorem ::
ZFMISC_1:96
Th95: X1
c= Y1 & X2
c= Y2 implies
[:X1, X2:]
c=
[:Y1, Y2:]
proof
assume X1
c= Y1 & X2
c= Y2;
then
[:X1, X2:]
c=
[:Y1, X2:] &
[:Y1, X2:]
c=
[:Y1, Y2:] by
Th94;
hence thesis;
end;
theorem ::
ZFMISC_1:97
Th96:
[:(X
\/ Y), Z:]
= (
[:X, Z:]
\/
[:Y, Z:]) &
[:Z, (X
\/ Y):]
= (
[:Z, X:]
\/
[:Z, Y:])
proof
A1: for z st z
in
[:(X
\/ Y), Z:] holds ex x, y st z
=
[x, y] by
Lm19;
A2: for x, y holds
[x, y]
in
[:(X
\/ Y), Z:] iff
[x, y]
in (
[:X, Z:]
\/
[:Y, Z:])
proof
let x, y;
thus
[x, y]
in
[:(X
\/ Y), Z:] implies
[x, y]
in (
[:X, Z:]
\/
[:Y, Z:])
proof
assume
A3:
[x, y]
in
[:(X
\/ Y), Z:];
then x
in (X
\/ Y) by
Lm16;
then
A4: x
in X or x
in Y by
XBOOLE_0:def 3;
y
in Z by
A3,
Lm16;
then
[x, y]
in
[:X, Z:] or
[x, y]
in
[:Y, Z:] by
A4,
Lm16;
hence thesis by
XBOOLE_0:def 3;
end;
assume
[x, y]
in (
[:X, Z:]
\/
[:Y, Z:]);
then
[x, y]
in
[:X, Z:] or
[x, y]
in
[:Y, Z:] by
XBOOLE_0:def 3;
then
A5: x
in X & y
in Z or x
in Y & y
in Z by
Lm16;
then x
in (X
\/ Y) by
XBOOLE_0:def 3;
hence thesis by
A5,
Lm16;
end;
A6: z
in (
[:X1, X2:]
\/
[:Y1, Y2:]) implies ex x, y st z
=
[x, y]
proof
assume z
in (
[:X1, X2:]
\/
[:Y1, Y2:]);
then z
in
[:X1, X2:] or z
in
[:Y1, Y2:] by
XBOOLE_0:def 3;
hence thesis by
Lm19;
end;
then for z st z
in (
[:X, Z:]
\/
[:Y, Z:]) holds ex x, y st z
=
[x, y];
hence
A7:
[:(X
\/ Y), Z:]
= (
[:X, Z:]
\/
[:Y, Z:]) by
A1,
A2,
Lm18;
A8: for y, x holds
[y, x]
in
[:Z, (X
\/ Y):] iff
[y, x]
in (
[:Z, X:]
\/
[:Z, Y:])
proof
let y, x;
A9:
[x, y]
in
[:X, Z:] or
[x, y]
in
[:Y, Z:] iff
[y, x]
in
[:Z, X:] or
[y, x]
in
[:Z, Y:] by
Th87;
[y, x]
in
[:Z, (X
\/ Y):] iff
[x, y]
in
[:(X
\/ Y), Z:] by
Th87;
hence thesis by
A7,
A9,
XBOOLE_0:def 3;
end;
A10: for z st z
in
[:Z, (X
\/ Y):] holds ex x, y st z
=
[x, y] by
Lm19;
for z st z
in (
[:Z, X:]
\/
[:Z, Y:]) holds ex x, y st z
=
[x, y] by
A6;
hence thesis by
A10,
A8,
Lm18;
end;
theorem ::
ZFMISC_1:98
[:(X1
\/ X2), (Y1
\/ Y2):]
= (((
[:X1, Y1:]
\/
[:X1, Y2:])
\/
[:X2, Y1:])
\/
[:X2, Y2:])
proof
thus
[:(X1
\/ X2), (Y1
\/ Y2):]
= (
[:X1, (Y1
\/ Y2):]
\/
[:X2, (Y1
\/ Y2):]) by
Th96
.= ((
[:X1, Y1:]
\/
[:X1, Y2:])
\/
[:X2, (Y1
\/ Y2):]) by
Th96
.= ((
[:X1, Y1:]
\/
[:X1, Y2:])
\/ (
[:X2, Y1:]
\/
[:X2, Y2:])) by
Th96
.= (((
[:X1, Y1:]
\/
[:X1, Y2:])
\/
[:X2, Y1:])
\/
[:X2, Y2:]) by
XBOOLE_1: 4;
end;
theorem ::
ZFMISC_1:99
[:(X
/\ Y), Z:]
= (
[:X, Z:]
/\
[:Y, Z:]) &
[:Z, (X
/\ Y):]
= (
[:Z, X:]
/\
[:Z, Y:])
proof
A1: for x, y holds
[x, y]
in
[:(X
/\ Y), Z:] iff
[x, y]
in (
[:X, Z:]
/\
[:Y, Z:])
proof
let x, y;
thus
[x, y]
in
[:(X
/\ Y), Z:] implies
[x, y]
in (
[:X, Z:]
/\
[:Y, Z:])
proof
assume
A2:
[x, y]
in
[:(X
/\ Y), Z:];
then
A3: x
in (X
/\ Y) by
Lm16;
A4: y
in Z by
A2,
Lm16;
x
in Y by
A3,
XBOOLE_0:def 4;
then
A5:
[x, y]
in
[:Y, Z:] by
A4,
Lm16;
x
in X by
A3,
XBOOLE_0:def 4;
then
[x, y]
in
[:X, Z:] by
A4,
Lm16;
hence thesis by
A5,
XBOOLE_0:def 4;
end;
assume
A6:
[x, y]
in (
[:X, Z:]
/\
[:Y, Z:]);
then
[x, y]
in
[:Y, Z:] by
XBOOLE_0:def 4;
then
A7: x
in Y by
Lm16;
A8:
[x, y]
in
[:X, Z:] by
A6,
XBOOLE_0:def 4;
then x
in X by
Lm16;
then
A9: x
in (X
/\ Y) by
A7,
XBOOLE_0:def 4;
y
in Z by
A8,
Lm16;
hence thesis by
A9,
Lm16;
end;
(
[:X, Z:]
/\
[:Y, Z:])
c=
[:X, Z:] by
XBOOLE_1: 17;
hence
A10:
[:(X
/\ Y), Z:]
= (
[:X, Z:]
/\
[:Y, Z:]) by
A1,
Lm17;
A11: for y, x holds
[y, x]
in
[:Z, (X
/\ Y):] iff
[y, x]
in (
[:Z, X:]
/\
[:Z, Y:])
proof
let y, x;
A12:
[x, y]
in
[:X, Z:] &
[x, y]
in
[:Y, Z:] iff
[y, x]
in
[:Z, X:] &
[y, x]
in
[:Z, Y:] by
Th87;
[y, x]
in
[:Z, (X
/\ Y):] iff
[x, y]
in
[:(X
/\ Y), Z:] by
Th87;
hence thesis by
A10,
A12,
XBOOLE_0:def 4;
end;
(
[:Z, X:]
/\
[:Z, Y:])
c=
[:Z, X:] by
XBOOLE_1: 17;
hence thesis by
A11,
Lm17;
end;
theorem ::
ZFMISC_1:100
Th99:
[:(X1
/\ X2), (Y1
/\ Y2):]
= (
[:X1, Y1:]
/\
[:X2, Y2:])
proof
(Y1
/\ Y2)
c= Y2 & (X1
/\ X2)
c= X2 by
XBOOLE_1: 17;
then
A1:
[:(X1
/\ X2), (Y1
/\ Y2):]
c=
[:X2, Y2:] by
Th95;
A2: (
[:X1, Y1:]
/\
[:X2, Y2:])
c=
[:(X1
/\ X2), (Y1
/\ Y2):]
proof
let z;
assume z
in (
[:X1, Y1:]
/\
[:X2, Y2:]);
then ex x, y st z
=
[x, y] & x
in (X1
/\ X2) & y
in (Y1
/\ Y2) by
Th84;
hence thesis by
Def2;
end;
(Y1
/\ Y2)
c= Y1 & (X1
/\ X2)
c= X1 by
XBOOLE_1: 17;
then
[:(X1
/\ X2), (Y1
/\ Y2):]
c=
[:X1, Y1:] by
Th95;
hence thesis by
A2,
A1,
XBOOLE_1: 19;
end;
theorem ::
ZFMISC_1:101
A
c= X & B
c= Y implies (
[:A, Y:]
/\
[:X, B:])
=
[:A, B:]
proof
assume that
A1: A
c= X and
A2: B
c= Y;
A3: (
[:A, Y:]
/\
[:X, B:])
=
[:(A
/\ X), (Y
/\ B):] by
Th99;
(A
/\ X)
= A by
A1,
XBOOLE_1: 28;
hence thesis by
A2,
A3,
XBOOLE_1: 28;
end;
theorem ::
ZFMISC_1:102
Th101:
[:(X
\ Y), Z:]
= (
[:X, Z:]
\
[:Y, Z:]) &
[:Z, (X
\ Y):]
= (
[:Z, X:]
\
[:Z, Y:])
proof
A1: for x, y holds
[x, y]
in
[:(X
\ Y), Z:] iff
[x, y]
in (
[:X, Z:]
\
[:Y, Z:])
proof
let x, y;
thus
[x, y]
in
[:(X
\ Y), Z:] implies
[x, y]
in (
[:X, Z:]
\
[:Y, Z:])
proof
assume
A2:
[x, y]
in
[:(X
\ Y), Z:];
then
A3: x
in (X
\ Y) by
Lm16;
then
A4: x
in X by
XBOOLE_0:def 5;
not x
in Y by
A3,
XBOOLE_0:def 5;
then
A5: not
[x, y]
in
[:Y, Z:] by
Lm16;
y
in Z by
A2,
Lm16;
then
[x, y]
in
[:X, Z:] by
A4,
Lm16;
hence thesis by
A5,
XBOOLE_0:def 5;
end;
assume
A6:
[x, y]
in (
[:X, Z:]
\
[:Y, Z:]);
then
A7:
[x, y]
in
[:X, Z:] by
XBOOLE_0:def 5;
then
A8: y
in Z by
Lm16;
not
[x, y]
in
[:Y, Z:] by
A6,
XBOOLE_0:def 5;
then
A9: not (x
in Y & y
in Z) by
Lm16;
x
in X by
A7,
Lm16;
then x
in (X
\ Y) by
A7,
A9,
Lm16,
XBOOLE_0:def 5;
hence thesis by
A8,
Lm16;
end;
(
[:X, Z:]
\
[:Y, Z:])
c=
[:X, Z:] by
XBOOLE_1: 36;
hence
A10:
[:(X
\ Y), Z:]
= (
[:X, Z:]
\
[:Y, Z:]) by
A1,
Lm17;
A11: for y, x holds
[y, x]
in
[:Z, (X
\ Y):] iff
[y, x]
in (
[:Z, X:]
\
[:Z, Y:])
proof
let y, x;
A12:
[x, y]
in
[:X, Z:] & not
[x, y]
in
[:Y, Z:] iff
[y, x]
in
[:Z, X:] & not
[y, x]
in
[:Z, Y:] by
Th87;
[y, x]
in
[:Z, (X
\ Y):] iff
[x, y]
in
[:(X
\ Y), Z:] by
Th87;
hence thesis by
A10,
A12,
XBOOLE_0:def 5;
end;
(
[:Z, X:]
\
[:Z, Y:])
c=
[:Z, X:] by
XBOOLE_1: 36;
hence thesis by
A11,
Lm17;
end;
theorem ::
ZFMISC_1:103
(
[:X1, X2:]
\
[:Y1, Y2:])
= (
[:(X1
\ Y1), X2:]
\/
[:X1, (X2
\ Y2):])
proof
A1: (
[:Y1, X2:]
/\
[:X1, Y2:])
=
[:(Y1
/\ X1), (X2
/\ Y2):] by
Th99;
(Y1
/\ X1)
c= Y1 & (X2
/\ Y2)
c= Y2 by
XBOOLE_1: 17;
then
A2:
[:(Y1
/\ X1), (X2
/\ Y2):]
c=
[:Y1, Y2:] by
Th95;
A3: (
[:(X1
\ Y1), X2:]
\/
[:X1, (X2
\ Y2):])
c= (
[:X1, X2:]
\
[:Y1, Y2:])
proof
let z;
A4:
now
assume z
in
[:(X1
\ Y1), X2:];
then
consider x, y such that
A5: x
in (X1
\ Y1) and
A6: y
in X2 and
A7: z
=
[x, y] by
Def2;
not x
in Y1 by
A5,
XBOOLE_0:def 5;
then
A8: not z
in
[:Y1, Y2:] by
A7,
Lm16;
x
in X1 by
A5,
XBOOLE_0:def 5;
then z
in
[:X1, X2:] by
A6,
A7,
Lm16;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
A9:
now
assume z
in
[:X1, (X2
\ Y2):];
then
consider x, y such that
A10: x
in X1 and
A11: y
in (X2
\ Y2) and
A12: z
=
[x, y] by
Def2;
not y
in Y2 by
A11,
XBOOLE_0:def 5;
then
A13: not z
in
[:Y1, Y2:] by
A12,
Lm16;
y
in X2 by
A11,
XBOOLE_0:def 5;
then z
in
[:X1, X2:] by
A10,
A12,
Lm16;
hence thesis by
A13,
XBOOLE_0:def 5;
end;
assume z
in (
[:(X1
\ Y1), X2:]
\/
[:X1, (X2
\ Y2):]);
hence thesis by
A4,
A9,
XBOOLE_0:def 3;
end;
[:(X1
\ Y1), X2:]
= (
[:X1, X2:]
\
[:Y1, X2:]) &
[:X1, (X2
\ Y2):]
= (
[:X1, X2:]
\
[:X1, Y2:]) by
Th101;
then (
[:(X1
\ Y1), X2:]
\/
[:X1, (X2
\ Y2):])
= (
[:X1, X2:]
\
[:(Y1
/\ X1), (X2
/\ Y2):]) by
A1,
XBOOLE_1: 54;
hence thesis by
A3,
A2,
XBOOLE_1: 34;
end;
theorem ::
ZFMISC_1:104
Th103: X1
misses X2 or Y1
misses Y2 implies
[:X1, Y1:]
misses
[:X2, Y2:]
proof
assume
A1: X1
misses X2 or Y1
misses Y2;
assume not thesis;
then
consider z such that
A2: z
in (
[:X1, Y1:]
/\
[:X2, Y2:]) by
XBOOLE_0: 4;
ex x, y st z
=
[x, y] & x
in (X1
/\ X2) & y
in (Y1
/\ Y2) by
A2,
Th84;
hence contradiction by
A1;
end;
theorem ::
ZFMISC_1:105
[x, y]
in
[:
{z}, Y:] iff x
= z & y
in Y
proof
A1: x
in
{z} iff x
= z by
TARSKI:def 1;
hence
[x, y]
in
[:
{z}, Y:] implies x
= z & y
in Y by
Lm16;
thus thesis by
A1,
Lm16;
end;
theorem ::
ZFMISC_1:106
[x, y]
in
[:X,
{z}:] iff x
in X & y
= z
proof
A1: y
in
{z} iff y
= z by
TARSKI:def 1;
hence
[x, y]
in
[:X,
{z}:] implies x
in X & y
= z by
Lm16;
thus thesis by
A1,
Lm16;
end;
theorem ::
ZFMISC_1:107
X
<>
{} implies
[:
{x}, X:]
<>
{} &
[:X,
{x}:]
<>
{} by
Th89;
theorem ::
ZFMISC_1:108
x
<> y implies
[:
{x}, X:]
misses
[:
{y}, Y:] &
[:X,
{x}:]
misses
[:Y,
{y}:]
proof
assume x
<> y;
then
{x}
misses
{y} by
Th11;
hence thesis by
Th103;
end;
theorem ::
ZFMISC_1:109
[:
{x, y}, X:]
= (
[:
{x}, X:]
\/
[:
{y}, X:]) &
[:X,
{x, y}:]
= (
[:X,
{x}:]
\/
[:X,
{y}:])
proof
{x, y}
= (
{x}
\/
{y}) by
ENUMSET1: 1;
hence thesis by
Th96;
end;
theorem ::
ZFMISC_1:110
Th109: X1
<>
{} & Y1
<>
{} &
[:X1, Y1:]
=
[:X2, Y2:] implies X1
= X2 & Y1
= Y2
proof
assume
A1: X1
<>
{} ;
then
consider x such that
A2: x
in X1 by
XBOOLE_0: 7;
assume
A3: Y1
<>
{} ;
then
consider y such that
A4: y
in Y1 by
XBOOLE_0: 7;
assume
A5:
[:X1, Y1:]
=
[:X2, Y2:];
then
A6:
[:X2, Y2:]
<>
{} by
A1,
A3,
Th89;
then
A7: Y2
<>
{} by
Th89;
for z holds z
in X1 iff z
in X2
proof
let z;
consider y2 such that
A8: y2
in Y2 by
A7,
XBOOLE_0: 7;
thus z
in X1 implies z
in X2
proof
assume z
in X1;
then
[z, y]
in
[:X2, Y2:] by
A4,
A5,
Lm16;
hence thesis by
Lm16;
end;
assume z
in X2;
then
[z, y2]
in
[:X2, Y2:] by
A8,
Lm16;
hence thesis by
A5,
Lm16;
end;
hence X1
= X2 by
TARSKI: 2;
A9: X2
<>
{} by
A6,
Th89;
for z holds z
in Y1 iff z
in Y2
proof
let z;
consider x2 such that
A10: x2
in X2 by
A9,
XBOOLE_0: 7;
thus z
in Y1 implies z
in Y2
proof
assume z
in Y1;
then
[x, z]
in
[:X2, Y2:] by
A2,
A5,
Lm16;
hence thesis by
Lm16;
end;
assume z
in Y2;
then
[x2, z]
in
[:X2, Y2:] by
A10,
Lm16;
hence thesis by
A5,
Lm16;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
ZFMISC_1:111
X
c=
[:X, Y:] or X
c=
[:Y, X:] implies X
=
{}
proof
assume
A1: X
c=
[:X, Y:] or X
c=
[:Y, X:];
assume
A2: X
<>
{} ;
A3:
now
defpred
P[
object] means ex Y st $1
= Y & ex z st z
in Y & z
in X;
consider Z such that
A4: for y holds y
in Z iff y
in (
union X) &
P[y] from
XBOOLE_0:sch 1;
consider Y2 such that
A5: Y2
in (X
\/ Z) and
A6: (X
\/ Z)
misses Y2 by
A2,
XREGULAR: 1;
now
assume
A7: not ex Y2 st Y2
in X & for Y1 st Y1
in Y2 holds for z holds not z
in Y1 or not z
in X;
now
assume
A8: Y2
in X;
then
consider Y1 such that
A9: Y1
in Y2 and
A10: ex z st z
in Y1 & z
in X by
A7;
Y1
in (
union X) by
A8,
A9,
TARSKI:def 4;
then Y1
in Z by
A4,
A10;
then Y1
in (X
\/ Z) by
XBOOLE_0:def 3;
hence contradiction by
A6,
A9,
XBOOLE_0: 3;
end;
then Y2
in Z by
A5,
XBOOLE_0:def 3;
then ex X2 st Y2
= X2 & ex z st z
in X2 & z
in X by
A4;
then
consider z such that
A11: z
in Y2 and
A12: z
in X;
z
in (X
\/ Z) by
A12,
XBOOLE_0:def 3;
hence contradiction by
A6,
A11,
XBOOLE_0: 3;
end;
then
consider Y1 such that
A13: Y1
in X and
A14: not ex Y2 st Y2
in Y1 & ex z st z
in Y2 & z
in X;
A15:
now
given y, x such that
A16: x
in X and
A17: Y1
=
[y, x];
A18: x
in
{y, x} by
TARSKI:def 2;
{y, x}
in Y1 by
A17,
TARSKI:def 2;
hence contradiction by
A14,
A16,
A18;
end;
assume X
c=
[:Y, X:];
then Y1
in
[:Y, X:] by
A13;
then ex y,x be
object st y
in Y & x
in X & Y1
=
[y, x] by
Def2;
hence contradiction by
A15;
end;
now
consider z be
object such that
A19: z
in X by
A2,
XBOOLE_0: 7;
consider Y1 such that
A20: Y1
in (X
\/ (
union X)) and
A21: (X
\/ (
union X))
misses Y1 by
A19,
XREGULAR: 1;
assume
A22: X
c=
[:X, Y:];
now
assume
A23: Y1
in X;
then
consider x, y such that
A24: Y1
=
[x, y] by
Lm19,
A22;
A25:
{x}
in Y1 by
A24,
TARSKI:def 2;
Y1
c= (
union X) by
A23,
Lm14;
then
{x}
in (
union X) by
A25;
then
{x}
in (X
\/ (
union X)) by
XBOOLE_0:def 3;
hence contradiction by
A21,
A25,
XBOOLE_0: 3;
end;
then Y1
in (
union X) by
A20,
XBOOLE_0:def 3;
then
consider Y2 such that
A26: Y1
in Y2 and
A27: Y2
in X by
TARSKI:def 4;
Y2
in
[:X, Y:] by
A22,
A27;
then
consider x,y be
object such that
A28: x
in X and y
in Y and
A29: Y2
=
[x, y] by
Def2;
Y1
=
{x} or Y1
=
{x, y} by
A26,
A29,
TARSKI:def 2;
then
A30: x
in Y1 by
TARSKI:def 1,
TARSKI:def 2;
x
in (X
\/ (
union X)) by
A28,
XBOOLE_0:def 3;
hence contradiction by
A21,
A30,
XBOOLE_0: 3;
end;
hence thesis by
A1,
A3;
end;
theorem ::
ZFMISC_1:112
ex M st N
in M & (for X, Y holds X
in M & Y
c= X implies Y
in M) & (for X holds X
in M implies (
bool X)
in M) & for X holds X
c= M implies (X,M)
are_equipotent or X
in M
proof
consider M such that
A1: N
in M and
A2: for X, Y holds X
in M & Y
c= X implies Y
in M and
A3: for X st X
in M holds ex Z st Z
in M & for Y st Y
c= X holds Y
in Z and
A4: for X holds X
c= M implies (X,M)
are_equipotent or X
in M by
TARSKI_A: 1;
take M;
thus N
in M by
A1;
thus for X, Y holds X
in M & Y
c= X implies Y
in M by
A2;
thus for X holds X
in M implies (
bool X)
in M
proof
let X;
assume X
in M;
then
consider Z such that
A5: Z
in M and
A6: for Y st Y
c= X holds Y
in Z by
A3;
now
let Y be
object;
reconsider YY = Y as
set by
TARSKI: 1;
assume Y
in (
bool X);
then YY
c= X by
Def1;
hence Y
in Z by
A6;
end;
hence thesis by
A2,
A5,
TARSKI:def 3;
end;
thus thesis by
A4;
end;
reserve e for
object,
X,X1,X2,Y1,Y2 for
set;
theorem ::
ZFMISC_1:113
e
in
[:X1, Y1:] & e
in
[:X2, Y2:] implies e
in
[:(X1
/\ X2), (Y1
/\ Y2):]
proof
assume e
in
[:X1, Y1:] & e
in
[:X2, Y2:];
then e
in (
[:X1, Y1:]
/\
[:X2, Y2:]) by
XBOOLE_0:def 4;
hence thesis by
Th99;
end;
begin
theorem ::
ZFMISC_1:114
Th113:
[:X1, X2:]
c=
[:Y1, Y2:] &
[:X1, X2:]
<>
{} implies X1
c= Y1 & X2
c= Y2
proof
assume that
A1:
[:X1, X2:]
c=
[:Y1, Y2:] and
A2:
[:X1, X2:]
<>
{} ;
A3:
[:X1, X2:]
= (
[:X1, X2:]
/\
[:Y1, Y2:]) by
A1,
XBOOLE_1: 28
.=
[:(X1
/\ Y1), (X2
/\ Y2):] by
Th99;
X1
<>
{} & X2
<>
{} by
A2,
Th89;
then X1
= (X1
/\ Y1) & X2
= (X2
/\ Y2) by
A3,
Th109;
hence thesis by
XBOOLE_1: 17;
end;
theorem ::
ZFMISC_1:115
for A be non
empty
set, B,C,D be
set st
[:A, B:]
c=
[:C, D:] or
[:B, A:]
c=
[:D, C:] holds B
c= D
proof
let A be non
empty
set, B,C,D be
set such that
A1:
[:A, B:]
c=
[:C, D:] or
[:B, A:]
c=
[:D, C:];
per cases ;
suppose B
=
{} ;
hence thesis;
end;
suppose B
<>
{} ;
then
[:A, B:]
<>
{} &
[:B, A:]
<>
{} by
Th89;
hence thesis by
A1,
Th113;
end;
end;
theorem ::
ZFMISC_1:116
x
in X implies ((X
\
{x})
\/
{x})
= X
proof
assume
A1: x
in X;
thus ((X
\
{x})
\/
{x})
c= X
proof
let y be
object;
assume y
in ((X
\
{x})
\/
{x});
then y
in (X
\
{x}) or y
in
{x} by
XBOOLE_0:def 3;
hence thesis by
A1,
Th55,
TARSKI:def 1;
end;
thus X
c= ((X
\
{x})
\/
{x})
proof
let y be
object;
assume y
in X;
then y
in
{x} or y
in (X
\
{x}) by
XBOOLE_0:def 5;
hence thesis by
XBOOLE_0:def 3;
end;
end;
theorem ::
ZFMISC_1:117
not x
in X implies ((X
\/
{x})
\
{x})
= X
proof
A1: ((X
\/
{x})
\
{x})
= (X
\
{x}) by
XBOOLE_1: 40;
assume not x
in X;
hence thesis by
A1,
Th56;
end;
theorem ::
ZFMISC_1:118
for x,y,z,Z be
set holds Z
c=
{x, y, z} iff Z
=
{} or Z
=
{x} or Z
=
{y} or Z
=
{z} or Z
=
{x, y} or Z
=
{y, z} or Z
=
{x, z} or Z
=
{x, y, z}
proof
let x,y,z,Z be
set;
hereby
assume that
A1: Z
c=
{x, y, z} and
A2: Z
<>
{} and
A3: Z
<>
{x} and
A4: Z
<>
{y} and
A5: Z
<>
{z} and
A6: Z
<>
{x, y} and
A7: Z
<>
{y, z} and
A8: Z
<>
{x, z};
{x, y, z}
c= Z
proof
let a be
object;
A9:
now
(
{x, y, z}
\
{x})
= ((
{x}
\/
{y, z})
\
{x}) by
ENUMSET1: 2
.= (
{y, z}
\
{x}) by
XBOOLE_1: 40;
then
A10: (
{x, y, z}
\
{x})
c=
{y, z} by
XBOOLE_1: 36;
assume not x
in Z;
then Z
c= (
{x, y, z}
\
{x}) by
A1,
Lm2;
hence contradiction by
A2,
A4,
A5,
A7,
Lm13,
A10,
XBOOLE_1: 1;
end;
A11:
now
(
{x, y, z}
\
{y})
= ((
{x, y}
\/
{z})
\
{y}) by
ENUMSET1: 3
.= (((
{x}
\/
{y})
\/
{z})
\
{y}) by
ENUMSET1: 1
.= (((
{x}
\/
{z})
\/
{y})
\
{y}) by
XBOOLE_1: 4
.= ((
{x, z}
\/
{y})
\
{y}) by
ENUMSET1: 1
.= (
{x, z}
\
{y}) by
XBOOLE_1: 40;
then
A12: (
{x, y, z}
\
{y})
c=
{x, z} by
XBOOLE_1: 36;
assume not y
in Z;
then Z
c= (
{x, y, z}
\
{y}) by
A1,
Lm2;
hence contradiction by
A2,
A3,
A5,
A8,
Lm13,
A12,
XBOOLE_1: 1;
end;
A13:
now
(
{x, y, z}
\
{z})
= ((
{x, y}
\/
{z})
\
{z}) by
ENUMSET1: 3
.= (
{x, y}
\
{z}) by
XBOOLE_1: 40;
then
A14: (
{x, y, z}
\
{z})
c=
{x, y} by
XBOOLE_1: 36;
assume not z
in Z;
then Z
c= (
{x, y, z}
\
{z}) by
A1,
Lm2;
hence contradiction by
A2,
A3,
A4,
A6,
Lm13,
A14,
XBOOLE_1: 1;
end;
assume a
in
{x, y, z};
hence thesis by
A9,
A11,
A13,
ENUMSET1:def 1;
end;
hence Z
=
{x, y, z} by
A1;
end;
assume
A15: Z
=
{} or Z
=
{x} or Z
=
{y} or Z
=
{z} or Z
=
{x, y} or Z
=
{y, z} or Z
=
{x, z} or Z
=
{x, y, z};
per cases by
A15;
suppose Z
=
{} ;
hence thesis;
end;
suppose Z
=
{x};
then Z
c= (
{x}
\/
{y, z}) by
XBOOLE_1: 7;
hence thesis by
ENUMSET1: 2;
end;
suppose
A16: Z
=
{y};
{x, y}
c= (
{x, y}
\/
{z}) by
XBOOLE_1: 7;
then
A17:
{x, y}
c=
{x, y, z} by
ENUMSET1: 3;
Z
c=
{x, y} by
A16,
Th7;
hence thesis by
A17;
end;
suppose Z
=
{z};
then Z
c= (
{x, y}
\/
{z}) by
XBOOLE_1: 7;
hence thesis by
ENUMSET1: 3;
end;
suppose Z
=
{x, y};
then Z
c= (
{x, y}
\/
{z}) by
XBOOLE_1: 7;
hence thesis by
ENUMSET1: 3;
end;
suppose Z
=
{y, z};
then Z
c= (
{x}
\/
{y, z}) by
XBOOLE_1: 7;
hence thesis by
ENUMSET1: 2;
end;
suppose
A18: Z
=
{x, z};
A19: (
{x, z}
\/
{y})
= ((
{x}
\/
{z})
\/
{y}) by
ENUMSET1: 1
.= (
{x}
\/ (
{y}
\/
{z})) by
XBOOLE_1: 4
.= (
{x}
\/
{y, z}) by
ENUMSET1: 1;
Z
c= (
{x, z}
\/
{y}) by
A18,
XBOOLE_1: 7;
hence thesis by
A19,
ENUMSET1: 2;
end;
suppose Z
=
{x, y, z};
hence thesis;
end;
end;
theorem ::
ZFMISC_1:119
N
c=
[:X1, Y1:] & M
c=
[:X2, Y2:] implies (N
\/ M)
c=
[:(X1
\/ X2), (Y1
\/ Y2):]
proof
assume N
c=
[:X1, Y1:] & M
c=
[:X2, Y2:];
then
A1: (N
\/ M)
c= (
[:X1, Y1:]
\/
[:X2, Y2:]) by
XBOOLE_1: 13;
X1
c= (X1
\/ X2) & Y1
c= (Y1
\/ Y2) by
XBOOLE_1: 7;
then
A2:
[:X1, Y1:]
c=
[:(X1
\/ X2), (Y1
\/ Y2):] by
Th95;
Y2
c= (Y1
\/ Y2) & X2
c= (X1
\/ X2) by
XBOOLE_1: 7;
then
[:X2, Y2:]
c=
[:(X1
\/ X2), (Y1
\/ Y2):] by
Th95;
then (
[:X1, Y1:]
\/
[:X2, Y2:])
c=
[:(X1
\/ X2), (Y1
\/ Y2):] by
A2,
XBOOLE_1: 8;
hence thesis by
A1;
end;
Lm20: not x
in X & not y
in X implies
{x, y}
misses X
proof
assume
A1: ( not x
in X) & not y
in X;
thus (
{x, y}
/\ X)
c=
{}
proof
let z be
object;
assume z
in (
{x, y}
/\ X);
then z
in
{x, y} & z
in X by
XBOOLE_0:def 4;
hence thesis by
A1,
TARSKI:def 2;
end;
thus thesis;
end;
theorem ::
ZFMISC_1:120
Th119: not x
in X & not y
in X implies X
= (X
\
{x, y})
proof
(X
\
{x, y})
= X iff X
misses
{x, y} by
XBOOLE_1: 83;
hence thesis by
Lm20;
end;
theorem ::
ZFMISC_1:121
not x
in X & not y
in X implies X
= ((X
\/
{x, y})
\
{x, y})
proof
A1: ((X
\/
{x, y})
\
{x, y})
= (X
\
{x, y}) by
XBOOLE_1: 40;
assume ( not x
in X) & not y
in X;
hence thesis by
A1,
Th119;
end;
definition
let x1,x2,x3 be
object;
::
ZFMISC_1:def5
pred x1,x2,x3
are_mutually_distinct means x1
<> x2 & x1
<> x3 & x2
<> x3;
end
definition
let x1,x2,x3,x4 be
object;
::
ZFMISC_1:def6
pred x1,x2,x3,x4
are_mutually_distinct means x1
<> x2 & x1
<> x3 & x1
<> x4 & x2
<> x3 & x2
<> x4 & x3
<> x4;
end
definition
let x1,x2,x3,x4,x5 be
object;
::
ZFMISC_1:def7
pred x1,x2,x3,x4,x5
are_mutually_distinct means x1
<> x2 & x1
<> x3 & x1
<> x4 & x1
<> x5 & x2
<> x3 & x2
<> x4 & x2
<> x5 & x3
<> x4 & x3
<> x5 & x4
<> x5;
end
definition
let x1,x2,x3,x4,x5,x6 be
object;
::
ZFMISC_1:def8
pred x1,x2,x3,x4,x5,x6
are_mutually_distinct means x1
<> x2 & x1
<> x3 & x1
<> x4 & x1
<> x5 & x1
<> x6 & x2
<> x3 & x2
<> x4 & x2
<> x5 & x2
<> x6 & x3
<> x4 & x3
<> x5 & x3
<> x6 & x4
<> x5 & x4
<> x6 & x5
<> x6;
end
definition
let x1,x2,x3,x4,x5,x6,x7 be
object;
::
ZFMISC_1:def9
pred x1,x2,x3,x4,x5,x6,x7
are_mutually_distinct means x1
<> x2 & x1
<> x3 & x1
<> x4 & x1
<> x5 & x1
<> x6 & x1
<> x7 & x2
<> x3 & x2
<> x4 & x2
<> x5 & x2
<> x6 & x2
<> x7 & x3
<> x4 & x3
<> x5 & x3
<> x6 & x3
<> x7 & x4
<> x5 & x4
<> x6 & x4
<> x7 & x5
<> x6 & x5
<> x7 & x6
<> x7;
end
theorem ::
ZFMISC_1:122
[:
{x1, x2},
{y1, y2}:]
=
{
[x1, y1],
[x1, y2],
[x2, y1],
[x2, y2]}
proof
thus
[:
{x1, x2},
{y1, y2}:]
=
[:(
{x1}
\/
{x2}),
{y1, y2}:] by
ENUMSET1: 1
.= (
[:
{x1},
{y1, y2}:]
\/
[:
{x2},
{y1, y2}:]) by
Th96
.= (
{
[x1, y1],
[x1, y2]}
\/
[:
{x2},
{y1, y2}:]) by
Th29
.= (
{
[x1, y1],
[x1, y2]}
\/
{
[x2, y1],
[x2, y2]}) by
Th29
.=
{
[x1, y1],
[x1, y2],
[x2, y1],
[x2, y2]} by
ENUMSET1: 5;
end;
theorem ::
ZFMISC_1:123
x
<> y implies ((A
\/
{x})
\
{y})
= ((A
\
{y})
\/
{x}) by
Th11,
XBOOLE_1: 87;
definition
let X;
::
ZFMISC_1:def10
attr X is
trivial means x
in X & y
in X implies x
= y;
end
registration
cluster
empty ->
trivial for
set;
coherence ;
end
registration
cluster non
trivial -> non
empty for
set;
coherence ;
end
registration
let x;
cluster
{x} ->
trivial;
coherence
proof
let y, z;
assume that
A1: y
in
{x} and
A2: z
in
{x};
y
= x by
A1,
TARSKI:def 1;
hence thesis by
A2,
TARSKI:def 1;
end;
end
registration
cluster
trivial non
empty for
set;
existence
proof
take
{
{} };
thus thesis;
end;
end
theorem ::
ZFMISC_1:124
for A,B,C be
set, p be
object st A
c= B & (B
/\ C)
=
{p} & p
in A holds (A
/\ C)
=
{p}
proof
let A,B,C be
set, p be
object such that
A1: A
c= B;
assume
A2: (B
/\ C)
=
{p};
p
in (B
/\ C) by
A2,
TARSKI:def 1;
then
A3: p
in C by
XBOOLE_0:def 4;
assume p
in A;
then p
in (A
/\ C) by
A3,
XBOOLE_0:def 4;
hence thesis by
A2,
Lm3,
A1,
XBOOLE_1: 26;
end;
theorem ::
ZFMISC_1:125
for A,B,C be
set st (A
/\ B)
c=
{p} & p
in C & C
misses B holds (A
\/ C)
misses B
proof
let A,B,C be
set such that
A1: (A
/\ B)
c=
{p} and
A2: p
in C and
A3: C
misses B;
{p}
c= C by
A2,
Lm1;
then (A
/\ B)
c= C by
A1;
then ((A
/\ B)
/\ B)
c= (C
/\ B) by
XBOOLE_1: 27;
then
A4: (A
/\ (B
/\ B))
c= (C
/\ B) by
XBOOLE_1: 16;
((A
\/ C)
/\ B)
= ((A
/\ B)
\/ (C
/\ B)) by
XBOOLE_1: 23
.=
{} by
A3,
A4,
XBOOLE_1: 12;
hence thesis;
end;
theorem ::
ZFMISC_1:126
for A,B be
set st for x,y be
set st x
in A & y
in B holds x
misses y holds (
union A)
misses (
union B)
proof
let A,B be
set such that
A1: for x,y be
set st x
in A & y
in B holds x
misses y;
for y be
set st y
in B holds (
union A)
misses y
proof
let y be
set;
assume y
in B;
then for x be
set st x
in A holds x
misses y by
A1;
hence thesis by
Th79;
end;
hence thesis by
Th79;
end;
registration
let X be
set, Y be
empty
set;
cluster
[:X, Y:] ->
empty;
coherence by
Th89;
end
registration
let X be
empty
set, Y be
set;
cluster
[:X, Y:] ->
empty;
coherence by
Th89;
end
theorem ::
ZFMISC_1:127
not A
in
[:A, B:]
proof
assume A
in
[:A, B:];
then
consider x,y be
object such that
A1: x
in A & y
in B & A
=
[x, y] by
Th83;
reconsider x as
set by
TARSKI: 1;
x
=
{x} or x
=
{x, y} by
A1,
TARSKI:def 2;
then x
in x by
TARSKI:def 1,
TARSKI:def 2;
hence contradiction;
end;
theorem ::
ZFMISC_1:128
B
=
[x,
{x}] implies B
in
[:
{x}, B:]
proof
assume
A1: B
=
[x,
{x}];
then
[:
{x}, B:]
=
{
[x,
{x}],
[x,
{x,
{x}}]} by
Th29;
hence thesis by
TARSKI:def 2,
A1;
end;
theorem ::
ZFMISC_1:129
B
in
[:A, B:] implies ex x be
object st x
in A & B
=
[x,
{x}]
proof
assume B
in
[:A, B:];
then
consider x,y be
object such that
A1: x
in A & y
in B & B
=
[x, y] by
Th83;
take x;
thus x
in A by
A1;
per cases by
A1,
TARSKI:def 2;
suppose y
=
{x};
hence thesis by
A1;
end;
suppose
A2: y
=
{x, y};
reconsider y as
set by
TARSKI: 1;
y
in y by
TARSKI:def 2,
A2;
hence thesis;
end;
end;
theorem ::
ZFMISC_1:130
B
c= A & A is
trivial implies B is
trivial
proof
assume that
A1: B
c= A and
A2: A is
trivial;
let x, y;
assume x
in B & y
in B;
then x
in A & y
in A by
A1;
hence thesis by
A2;
end;
registration
cluster non
trivial for
set;
existence
proof
take
{
{} ,
{
{} }},
{} ,
{
{} };
thus
{}
in
{
{} ,
{
{} }} &
{
{} }
in
{
{} ,
{
{} }} by
TARSKI:def 2;
thus
{}
<>
{
{} };
end;
end
theorem ::
ZFMISC_1:131
Th130: X is non
empty
trivial implies ex x st X
=
{x}
proof
assume X is non
empty;
then
consider x be
object such that
A1: x
in X;
assume
A2: X is
trivial;
take x;
for y be
object holds y
in X iff x
= y by
A2,
A1;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:132
for x be
set, X be
trivial
set st x
in X holds X
=
{x}
proof
let x be
set, X be
trivial
set;
assume
A1: x
in X;
then ex x be
object st X
=
{x} by
Th130;
hence thesis by
A1,
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:133
for a,b,c,X be
set st a
in X & b
in X & c
in X holds
{a, b, c}
c= X
proof
let a,b,c,X be
set;
assume a
in X & b
in X & c
in X;
then
{a, b}
c= X &
{c}
c= X by
Lm1,
Th31;
then (
{a, b}
\/
{c})
c= X by
XBOOLE_1: 8;
hence thesis by
ENUMSET1: 3;
end;
theorem ::
ZFMISC_1:134
[x, y]
in X implies x
in (
union (
union X)) & y
in (
union (
union X))
proof
assume
A1:
[x, y]
in X;
{x}
in
{
{x},
{x, y}} by
TARSKI:def 2;
then
A2:
{x}
in (
union X) by
A1,
TARSKI:def 4;
{x, y}
in
{
{x},
{x, y}} by
TARSKI:def 2;
then
A3:
{x, y}
in (
union X) by
A1,
TARSKI:def 4;
y
in
{x, y} & x
in
{x} by
TARSKI:def 1,
TARSKI:def 2;
hence thesis by
A3,
A2,
TARSKI:def 4;
end;
theorem ::
ZFMISC_1:135
Th134: X
c= (Y
\/
{x}) implies x
in X or X
c= Y
proof
assume that
A1: X
c= (Y
\/
{x}) and
A2: not x
in X;
X
= (X
/\ (Y
\/
{x})) by
A1,
XBOOLE_1: 28
.= ((X
/\ Y)
\/ (X
/\
{x})) by
XBOOLE_1: 23
.= ((X
/\ Y)
\/
{} ) by
A2,
Lm6,
XBOOLE_0:def 7
.= (X
/\ Y);
hence thesis by
XBOOLE_1: 17;
end;
theorem ::
ZFMISC_1:136
x
in (X
\/
{y}) iff x
in X or x
= y
proof
x
in (X
\/
{y}) iff x
in X or x
in
{y} by
XBOOLE_0:def 3;
hence thesis by
TARSKI:def 1;
end;
theorem ::
ZFMISC_1:137
(X
\/
{x})
c= Y iff x
in Y & X
c= Y
proof
X
c= Y &
{x}
c= Y implies (X
\/
{x})
c= Y by
XBOOLE_1: 8;
hence thesis by
Lm1,
XBOOLE_1: 11;
end;
theorem ::
ZFMISC_1:138
for A,B be
set st A
c= B & B
c= (A
\/
{a}) holds (A
\/
{a})
= B or A
= B
proof
let A,B be
set;
assume that
A1: A
c= B and
A2: B
c= (A
\/
{a});
assume that
A3: (A
\/
{a})
<> B and
A4: A
<> B;
not a
in B
proof
assume a
in B;
then
{a}
c= B by
Lm1;
hence thesis by
A1,
A2,
A3,
XBOOLE_1: 8;
end;
hence thesis by
A2,
Th134,
A1,
A4;
end;
registration
let A,B be
trivial
set;
cluster
[:A, B:] ->
trivial;
coherence
proof
per cases ;
suppose A is
empty or B is
empty;
hence thesis;
end;
suppose that
A1: not A is
empty and
A2: not B is
empty;
consider a be
object such that
A3: A
=
{a} by
A1,
Th130;
consider b be
object such that
A4: B
=
{b} by
A2,
Th130;
[:A, B:]
=
{
[a, b]} by
A3,
A4,
Th28;
hence thesis;
end;
end;
end
theorem ::
ZFMISC_1:139
for X be
set holds X is non
trivial iff for x holds (X
\
{x}) is non
empty
proof
let X be
set;
hereby
assume
A1: X is non
trivial;
let x be
object;
X
<>
{x} by
A1;
then
consider y be
object such that
A2: y
in X and
A3: x
<> y by
A1,
Lm12;
not y
in
{x} by
A3,
TARSKI:def 1;
hence (X
\
{x}) is non
empty by
A2,
XBOOLE_0:def 5;
end;
assume
A4: for x holds (X
\
{x}) is non
empty;
(X
\
{
{} })
c= X by
XBOOLE_1: 36;
then X is non
empty by
A4;
then
consider x be
object such that
A5: x
in X;
(X
\
{x}) is non
empty by
A4;
then
consider y be
object such that
A6: y
in (X
\
{x});
reconsider x, y as
set by
TARSKI: 1;
take x, y;
thus x
in X by
A5;
(X
\
{x})
c= X by
XBOOLE_1: 36;
hence y
in X by
A6;
x
in
{x} by
TARSKI:def 1;
hence x
<> y by
A6,
XBOOLE_0:def 5;
end;
theorem ::
ZFMISC_1:140
{X}
<> X
proof
X
in
{X} by
TARSKI:def 1;
hence thesis;
end;
theorem ::
ZFMISC_1:141
(
bool X)
<> X
proof
X
in (
bool X) by
Def1;
hence thesis;
end;