setfam_1.miz
begin
reserve X,Y,Z,Z1,Z2,D for
set,
x,y for
object;
definition
let X;
::
SETFAM_1:def1
func
meet X ->
set means
:
Def1: for x be
object holds x
in it iff for Y holds Y
in X implies x
in Y if X
<>
{}
otherwise it
=
{} ;
existence
proof
thus X
<>
{} implies ex Z1 st for x be
object holds x
in Z1 iff for Z st Z
in X holds x
in Z
proof
defpred
X[
object] means for Z st Z
in X holds $1
in Z;
assume
A1: X
<>
{} ;
consider Y such that
A2: for x be
object holds x
in Y iff x
in (
union X) &
X[x] from
XBOOLE_0:sch 1;
take Y;
for x be
object holds (for Z st Z
in X holds x
in Z) implies x
in Y
proof
set y = the
Element of X;
let x be
object such that
A3: for Z st Z
in X holds x
in Z;
x
in y by
A1,
A3;
then x
in (
union X) by
A1,
TARSKI:def 4;
hence thesis by
A2,
A3;
end;
hence thesis by
A2;
end;
thus thesis;
end;
uniqueness
proof
let Z1, Z2;
now
assume that X
<>
{} and
A4: for x be
object holds x
in Z1 iff for Y holds Y
in X implies x
in Y and
A5: for x be
object holds x
in Z2 iff for Y holds Y
in X implies x
in Y;
now
let x be
object;
x
in Z1 iff for Y holds Y
in X implies x
in Y by
A4;
hence x
in Z1 iff x
in Z2 by
A5;
end;
hence Z1
= Z2 by
TARSKI: 2;
end;
hence thesis;
end;
consistency ;
end
theorem ::
SETFAM_1:1
(
meet
{} )
=
{} by
Def1;
theorem ::
SETFAM_1:2
Th2: (
meet X)
c= (
union X)
proof
A1:
now
assume
A2: X
<>
{} ;
now
set y = the
Element of X;
let x be
object;
assume x
in (
meet X);
then x
in y by
A2,
Def1;
hence x
in (
union X) by
A2,
TARSKI:def 4;
end;
hence thesis;
end;
X
=
{} implies thesis by
Def1;
hence thesis by
A1;
end;
theorem ::
SETFAM_1:3
Th3: Z
in X implies (
meet X)
c= Z by
Def1;
theorem ::
SETFAM_1:4
{}
in X implies (
meet X)
=
{} by
Th3,
XBOOLE_1: 3;
theorem ::
SETFAM_1:5
X
<>
{} & (for Z1 st Z1
in X holds Z
c= Z1) implies Z
c= (
meet X)
proof
assume that
A1: X
<>
{} and
A2: for Z1 st Z1
in X holds Z
c= Z1;
thus Z
c= (
meet X)
proof
let x be
object such that
A3: x
in Z;
for Y st Y
in X holds x
in Y
proof
let Y;
assume Y
in X;
then Z
c= Y by
A2;
hence thesis by
A3;
end;
hence thesis by
A1,
Def1;
end;
end;
theorem ::
SETFAM_1:6
Th6: X
<>
{} & X
c= Y implies (
meet Y)
c= (
meet X)
proof
assume that
A1: X
<>
{} and
A2: X
c= Y;
let x be
object;
assume x
in (
meet Y);
then for Z st Z
in X holds x
in Z by
A2,
Def1;
hence thesis by
A1,
Def1;
end;
theorem ::
SETFAM_1:7
X
in Y & X
c= Z implies (
meet Y)
c= Z
proof
assume that
A1: X
in Y and
A2: X
c= Z;
(
meet Y)
c= X by
A1,
Th3;
hence thesis by
A2;
end;
theorem ::
SETFAM_1:8
X
in Y & X
misses Z implies (
meet Y)
misses Z by
Th3,
XBOOLE_1: 63;
theorem ::
SETFAM_1:9
X
<>
{} & Y
<>
{} implies (
meet (X
\/ Y))
= ((
meet X)
/\ (
meet Y))
proof
assume that
A1: X
<>
{} and
A2: Y
<>
{} ;
A3: ((
meet X)
/\ (
meet Y))
c= (
meet (X
\/ Y))
proof
let x be
object;
assume x
in ((
meet X)
/\ (
meet Y));
then
A4: x
in (
meet X) & x
in (
meet Y) by
XBOOLE_0:def 4;
now
let Z;
assume Z
in (X
\/ Y);
then Z
in X or Z
in Y by
XBOOLE_0:def 3;
hence x
in Z by
A4,
Def1;
end;
hence thesis by
A1,
Def1;
end;
(
meet (X
\/ Y))
c= (
meet X) & (
meet (X
\/ Y))
c= (
meet Y) by
A1,
A2,
Th6,
XBOOLE_1: 7;
then (
meet (X
\/ Y))
c= ((
meet X)
/\ (
meet Y)) by
XBOOLE_1: 19;
hence thesis by
A3;
end;
theorem ::
SETFAM_1:10
(
meet
{X})
= X
proof
A1: X
c= (
meet
{X})
proof
let y be
object;
assume y
in X;
then for Z st Z
in
{X} holds y
in Z by
TARSKI:def 1;
hence thesis by
Def1;
end;
X
in
{X} by
TARSKI:def 1;
then (
meet
{X})
c= X by
Th3;
hence thesis by
A1;
end;
theorem ::
SETFAM_1:11
(
meet
{X, Y})
= (X
/\ Y)
proof
A1: X
in
{X, Y} & Y
in
{X, Y} by
TARSKI:def 2;
for x be
object holds x
in (
meet
{X, Y}) iff x
in X & x
in Y
proof
let x be
object;
thus x
in (
meet
{X, Y}) implies x
in X & x
in Y by
A1,
Def1;
assume x
in X & x
in Y;
then for Z holds Z
in
{X, Y} implies x
in Z by
TARSKI:def 2;
hence thesis by
Def1;
end;
hence thesis by
XBOOLE_0:def 4;
end;
reserve SFX,SFY,SFZ for
set;
definition
let SFX, SFY;
::
SETFAM_1:def2
pred SFX
is_finer_than SFY means for X st X
in SFX holds ex Y st Y
in SFY & X
c= Y;
reflexivity ;
::
SETFAM_1:def3
pred SFY
is_coarser_than SFX means for Y st Y
in SFY holds ex X st X
in SFX & X
c= Y;
reflexivity ;
end
theorem ::
SETFAM_1:12
SFX
c= SFY implies SFX
is_finer_than SFY;
theorem ::
SETFAM_1:13
SFX
is_finer_than SFY implies (
union SFX)
c= (
union SFY)
proof
assume
A1: for X st X
in SFX holds ex Y st Y
in SFY & X
c= Y;
thus (
union SFX)
c= (
union SFY)
proof
let x be
object;
assume x
in (
union SFX);
then
consider Y such that
A2: x
in Y and
A3: Y
in SFX by
TARSKI:def 4;
ex Z st Z
in SFY & Y
c= Z by
A1,
A3;
hence thesis by
A2,
TARSKI:def 4;
end;
end;
theorem ::
SETFAM_1:14
SFY
<>
{} & SFY
is_coarser_than SFX implies (
meet SFX)
c= (
meet SFY)
proof
assume that
A1: SFY
<>
{} and
A2: for Z2 st Z2
in SFY holds ex Z1 st Z1
in SFX & Z1
c= Z2;
(
meet SFX)
c= (
meet SFY)
proof
let x be
object such that
A3: x
in (
meet SFX);
for Z st Z
in SFY holds x
in Z
proof
let Z;
assume Z
in SFY;
then
consider Z1 such that
A4: Z1
in SFX and
A5: Z1
c= Z by
A2;
x
in Z1 by
A3,
A4,
Def1;
hence thesis by
A5;
end;
hence thesis by
A1,
Def1;
end;
hence thesis;
end;
theorem ::
SETFAM_1:15
{}
is_finer_than SFX;
theorem ::
SETFAM_1:16
SFX
is_finer_than
{} implies SFX
=
{}
proof
assume
A1: for X st X
in SFX holds ex Y st Y
in
{} & X
c= Y;
set x = the
Element of SFX;
assume not thesis;
then ex Y st Y
in
{} & x
c= Y by
A1;
hence contradiction;
end;
theorem ::
SETFAM_1:17
SFX
is_finer_than SFY & SFY
is_finer_than SFZ implies SFX
is_finer_than SFZ
proof
assume that
A1: for X st X
in SFX holds ex Y st Y
in SFY & X
c= Y and
A2: for X st X
in SFY holds ex Y st Y
in SFZ & X
c= Y;
let X;
assume X
in SFX;
then
consider Y such that
A3: Y
in SFY and
A4: X
c= Y by
A1;
consider Z such that
A5: Z
in SFZ & Y
c= Z by
A2,
A3;
take Z;
thus thesis by
A4,
A5;
end;
theorem ::
SETFAM_1:18
SFX
is_finer_than
{Y} implies for X st X
in SFX holds X
c= Y
proof
assume
A1: for X st X
in SFX holds ex Z st Z
in
{Y} & X
c= Z;
let X;
assume X
in SFX;
then ex Z st Z
in
{Y} & X
c= Z by
A1;
hence thesis by
TARSKI:def 1;
end;
theorem ::
SETFAM_1:19
SFX
is_finer_than
{X, Y} implies for Z st Z
in SFX holds Z
c= X or Z
c= Y
proof
assume
A1: for Z1 st Z1
in SFX holds ex Z2 st Z2
in
{X, Y} & Z1
c= Z2;
let Z;
assume Z
in SFX;
then
consider Z2 such that
A2: Z2
in
{X, Y} and
A3: Z
c= Z2 by
A1;
{X, Y}
= (
{X}
\/
{Y}) by
ENUMSET1: 1;
then Z2
in
{X} or Z2
in
{Y} by
A2,
XBOOLE_0:def 3;
hence thesis by
A3,
TARSKI:def 1;
end;
definition
let SFX, SFY;
::
SETFAM_1:def4
func
UNION (SFX,SFY) ->
set means
:
Def4: Z
in it iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\/ Y);
existence
proof
defpred
X[
set] means ex Z be
set st $1
= Z & ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\/ Y);
consider XX be
set such that
A1: for x be
set holds x
in XX iff x
in (
bool ((
union SFX)
\/ (
union SFY))) &
X[x] from
XFAMILY:sch 1;
take XX;
for Z holds Z
in XX iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\/ Y)
proof
let Z;
A2:
now
given X, Y such that
A3: X
in SFX & Y
in SFY and
A4: Z
= (X
\/ Y);
X
c= (
union SFX) & Y
c= (
union SFY) by
A3,
ZFMISC_1: 74;
then Z
c= ((
union SFX)
\/ (
union SFY)) by
A4,
XBOOLE_1: 13;
hence Z
in XX by
A1,
A3,
A4;
end;
now
assume Z
in XX;
then ex Z1 st Z
= Z1 & ex X, Y st X
in SFX & Y
in SFY & Z1
= (X
\/ Y) by
A1;
hence ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\/ Y);
end;
hence thesis by
A2;
end;
hence thesis;
end;
uniqueness
proof
let Z1,Z2 be
set;
assume that
A5: for Z holds Z
in Z1 iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\/ Y) and
A6: for Z holds Z
in Z2 iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\/ Y);
now
let Z be
object;
Z
in Z1 iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\/ Y) by
A5;
hence Z
in Z1 iff Z
in Z2 by
A6;
end;
hence thesis by
TARSKI: 2;
end;
commutativity
proof
let SFZ, SFX, SFY;
assume
A7: for Z holds Z
in SFZ iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\/ Y);
let Z;
hereby
assume Z
in SFZ;
then ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\/ Y) by
A7;
hence ex Y, X st Y
in SFY & X
in SFX & Z
= (Y
\/ X);
end;
thus thesis by
A7;
end;
::
SETFAM_1:def5
func
INTERSECTION (SFX,SFY) ->
set means
:
Def5: Z
in it iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
/\ Y);
existence
proof
defpred
X[
set] means ex Z be
set st $1
= Z & ex X, Y st X
in SFX & Y
in SFY & Z
= (X
/\ Y);
consider XX be
set such that
A8: for x be
set holds x
in XX iff x
in (
bool ((
union SFX)
/\ (
union SFY))) &
X[x] from
XFAMILY:sch 1;
take XX;
for Z holds Z
in XX iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
/\ Y)
proof
let Z;
A9:
now
given X, Y such that
A10: X
in SFX & Y
in SFY and
A11: Z
= (X
/\ Y);
X
c= (
union SFX) & Y
c= (
union SFY) by
A10,
ZFMISC_1: 74;
then Z
c= ((
union SFX)
/\ (
union SFY)) by
A11,
XBOOLE_1: 27;
hence Z
in XX by
A8,
A10,
A11;
end;
now
assume Z
in XX;
then ex Z1 st Z
= Z1 & ex X, Y st X
in SFX & Y
in SFY & Z1
= (X
/\ Y) by
A8;
hence ex X, Y st X
in SFX & Y
in SFY & Z
= (X
/\ Y);
end;
hence thesis by
A9;
end;
hence thesis;
end;
uniqueness
proof
let Z1,Z2 be
set;
assume that
A12: for Z holds Z
in Z1 iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
/\ Y) and
A13: for Z holds Z
in Z2 iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
/\ Y);
now
let Z be
object;
Z
in Z1 iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
/\ Y) by
A12;
hence Z
in Z1 iff Z
in Z2 by
A13;
end;
hence thesis by
TARSKI: 2;
end;
commutativity
proof
let SFZ, SFX, SFY;
assume
A14: for Z holds Z
in SFZ iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
/\ Y);
let Z;
hereby
assume Z
in SFZ;
then ex X, Y st X
in SFX & Y
in SFY & Z
= (X
/\ Y) by
A14;
hence ex Y, X st Y
in SFY & X
in SFX & Z
= (Y
/\ X);
end;
thus thesis by
A14;
end;
::
SETFAM_1:def6
func
DIFFERENCE (SFX,SFY) ->
set means
:
Def6: Z
in it iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\ Y);
existence
proof
defpred
X[
set] means ex Z be
set st $1
= Z & ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\ Y);
consider XX be
set such that
A15: for x be
set holds x
in XX iff x
in (
bool (
union SFX)) &
X[x] from
XFAMILY:sch 1;
take XX;
for Z holds Z
in XX iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\ Y)
proof
let Z;
A16:
now
given X, Y such that
A17: X
in SFX and
A18: Y
in SFY and
A19: Z
= (X
\ Y);
X
c= (
union SFX) by
A17,
ZFMISC_1: 74;
then Z
c= (
union SFX) by
A19;
hence Z
in XX by
A15,
A17,
A18,
A19;
end;
now
assume Z
in XX;
then ex Z1 st Z
= Z1 & ex X, Y st X
in SFX & Y
in SFY & Z1
= (X
\ Y) by
A15;
hence ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\ Y);
end;
hence thesis by
A16;
end;
hence thesis;
end;
uniqueness
proof
let Z1,Z2 be
set;
assume that
A20: for Z holds Z
in Z1 iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\ Y) and
A21: for Z holds Z
in Z2 iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\ Y);
now
let Z be
object;
Z
in Z1 iff ex X, Y st X
in SFX & Y
in SFY & Z
= (X
\ Y) by
A20;
hence Z
in Z1 iff Z
in Z2 by
A21;
end;
hence thesis by
TARSKI: 2;
end;
end
theorem ::
SETFAM_1:20
SFX
is_finer_than (
UNION (SFX,SFX))
proof
let X such that
A1: X
in SFX;
take X;
X
= (X
\/ X);
hence thesis by
A1,
Def4;
end;
theorem ::
SETFAM_1:21
(
INTERSECTION (SFX,SFX))
is_finer_than SFX
proof
let X;
assume X
in (
INTERSECTION (SFX,SFX));
then
consider Z1, Z2 such that
A1: Z1
in SFX and Z2
in SFX and
A2: X
= (Z1
/\ Z2) by
Def5;
take Z1;
thus thesis by
A1,
A2,
XBOOLE_1: 17;
end;
theorem ::
SETFAM_1:22
(
DIFFERENCE (SFX,SFX))
is_finer_than SFX
proof
let X;
assume X
in (
DIFFERENCE (SFX,SFX));
then
consider Z1, Z2 such that
A1: Z1
in SFX and Z2
in SFX and
A2: X
= (Z1
\ Z2) by
Def6;
take Z1;
thus thesis by
A1,
A2;
end;
theorem ::
SETFAM_1:23
SFX
meets SFY implies ((
meet SFX)
/\ (
meet SFY))
= (
meet (
INTERSECTION (SFX,SFY)))
proof
set y = the
Element of (SFX
/\ SFY);
assume
A1: (SFX
/\ SFY)
<>
{} ;
then
A2: SFY
<>
{} ;
A3: y
in SFX by
A1,
XBOOLE_0:def 4;
A4: y
in SFY by
A1,
XBOOLE_0:def 4;
A5: SFX
<>
{} by
A1;
A6: (
meet (
INTERSECTION (SFX,SFY)))
c= ((
meet SFX)
/\ (
meet SFY))
proof
let x be
object such that
A7: x
in (
meet (
INTERSECTION (SFX,SFY)));
for Z st Z
in SFY holds x
in Z
proof
let Z;
assume Z
in SFY;
then (y
/\ Z)
in (
INTERSECTION (SFX,SFY)) by
A3,
Def5;
then x
in (y
/\ Z) by
A7,
Def1;
hence thesis by
XBOOLE_0:def 4;
end;
then
A8: x
in (
meet SFY) by
A2,
Def1;
for Z st Z
in SFX holds x
in Z
proof
let Z;
assume Z
in SFX;
then (Z
/\ y)
in (
INTERSECTION (SFX,SFY)) by
A4,
Def5;
then x
in (Z
/\ y) by
A7,
Def1;
hence thesis by
XBOOLE_0:def 4;
end;
then x
in (
meet SFX) by
A5,
Def1;
hence thesis by
A8,
XBOOLE_0:def 4;
end;
A9: (y
/\ y)
in (
INTERSECTION (SFX,SFY)) by
A3,
A4,
Def5;
((
meet SFX)
/\ (
meet SFY))
c= (
meet (
INTERSECTION (SFX,SFY)))
proof
let x be
object;
assume x
in ((
meet SFX)
/\ (
meet SFY));
then
A10: x
in (
meet SFX) & x
in (
meet SFY) by
XBOOLE_0:def 4;
for Z st Z
in (
INTERSECTION (SFX,SFY)) holds x
in Z
proof
let Z;
assume Z
in (
INTERSECTION (SFX,SFY));
then
consider Z1, Z2 such that
A11: Z1
in SFX & Z2
in SFY and
A12: Z
= (Z1
/\ Z2) by
Def5;
x
in Z1 & x
in Z2 by
A10,
A11,
Def1;
hence thesis by
A12,
XBOOLE_0:def 4;
end;
hence thesis by
A9,
Def1;
end;
hence thesis by
A6;
end;
theorem ::
SETFAM_1:24
SFY
<>
{} implies (X
\/ (
meet SFY))
= (
meet (
UNION (
{X},SFY)))
proof
assume
A1: SFY
<>
{} ;
set y = the
Element of SFY;
X
in
{X} by
TARSKI:def 1;
then
A2: (X
\/ y)
in (
UNION (
{X},SFY)) by
A1,
Def4;
A3: (X
\/ (
meet SFY))
c= (
meet (
UNION (
{X},SFY)))
proof
let x be
object;
assume x
in (X
\/ (
meet SFY));
then
A4: x
in X or x
in (
meet SFY) by
XBOOLE_0:def 3;
for Z st Z
in (
UNION (
{X},SFY)) holds x
in Z
proof
let Z;
assume Z
in (
UNION (
{X},SFY));
then
consider Z1, Z2 such that
A5: Z1
in
{X} & Z2
in SFY and
A6: Z
= (Z1
\/ Z2) by
Def4;
x
in Z1 or x
in Z2 by
A4,
A5,
Def1,
TARSKI:def 1;
hence thesis by
A6,
XBOOLE_0:def 3;
end;
hence thesis by
A2,
Def1;
end;
(
meet (
UNION (
{X},SFY)))
c= (X
\/ (
meet SFY))
proof
let x be
object;
assume
A7: x
in (
meet (
UNION (
{X},SFY)));
assume
A8: not x
in (X
\/ (
meet SFY));
then
A9: not x
in X by
XBOOLE_0:def 3;
not x
in (
meet SFY) by
A8,
XBOOLE_0:def 3;
then
consider Z such that
A10: Z
in SFY and
A11: not x
in Z by
A1,
Def1;
X
in
{X} by
TARSKI:def 1;
then (X
\/ Z)
in (
UNION (
{X},SFY)) by
A10,
Def4;
then x
in (X
\/ Z) by
A7,
Def1;
hence contradiction by
A9,
A11,
XBOOLE_0:def 3;
end;
hence thesis by
A3;
end;
theorem ::
SETFAM_1:25
(X
/\ (
union SFY))
= (
union (
INTERSECTION (
{X},SFY)))
proof
A1: (
union (
INTERSECTION (
{X},SFY)))
c= (X
/\ (
union SFY))
proof
let x be
object;
assume x
in (
union (
INTERSECTION (
{X},SFY)));
then
consider Z such that
A2: x
in Z and
A3: Z
in (
INTERSECTION (
{X},SFY)) by
TARSKI:def 4;
consider X1,X2 be
set such that
A4: X1
in
{X} and
A5: X2
in SFY and
A6: Z
= (X1
/\ X2) by
A3,
Def5;
x
in X2 by
A2,
A6,
XBOOLE_0:def 4;
then
A7: x
in (
union SFY) by
A5,
TARSKI:def 4;
X1
= X by
A4,
TARSKI:def 1;
then x
in X by
A2,
A6,
XBOOLE_0:def 4;
hence thesis by
A7,
XBOOLE_0:def 4;
end;
(X
/\ (
union SFY))
c= (
union (
INTERSECTION (
{X},SFY)))
proof
let x be
object;
assume
A8: x
in (X
/\ (
union SFY));
then x
in (
union SFY) by
XBOOLE_0:def 4;
then
consider Y such that
A9: x
in Y and
A10: Y
in SFY by
TARSKI:def 4;
x
in X by
A8,
XBOOLE_0:def 4;
then
A11: x
in (X
/\ Y) by
A9,
XBOOLE_0:def 4;
X
in
{X} by
TARSKI:def 1;
then (X
/\ Y)
in (
INTERSECTION (
{X},SFY)) by
A10,
Def5;
hence thesis by
A11,
TARSKI:def 4;
end;
hence thesis by
A1;
end;
theorem ::
SETFAM_1:26
SFY
<>
{} implies (X
\ (
union SFY))
= (
meet (
DIFFERENCE (
{X},SFY)))
proof
set y = the
Element of SFY;
A1: X
in
{X} by
TARSKI:def 1;
assume SFY
<>
{} ;
then
A2: (X
\ y)
in (
DIFFERENCE (
{X},SFY)) by
A1,
Def6;
A3: (
meet (
DIFFERENCE (
{X},SFY)))
c= (X
\ (
union SFY))
proof
let x be
object;
assume
A4: x
in (
meet (
DIFFERENCE (
{X},SFY)));
for Z st Z
in SFY holds not x
in Z
proof
let Z;
assume Z
in SFY;
then (X
\ Z)
in (
DIFFERENCE (
{X},SFY)) by
A1,
Def6;
then x
in (X
\ Z) by
A4,
Def1;
hence thesis by
XBOOLE_0:def 5;
end;
then for Z st x
in Z holds not Z
in SFY;
then
A5: not x
in (
union SFY) by
TARSKI:def 4;
x
in (X
\ y) by
A2,
A4,
Def1;
hence thesis by
A5,
XBOOLE_0:def 5;
end;
(X
\ (
union SFY))
c= (
meet (
DIFFERENCE (
{X},SFY)))
proof
let x be
object;
assume x
in (X
\ (
union SFY));
then
A6: x
in X & not x
in (
union SFY) by
XBOOLE_0:def 5;
for Z st Z
in (
DIFFERENCE (
{X},SFY)) holds x
in Z
proof
let Z;
assume Z
in (
DIFFERENCE (
{X},SFY));
then
consider Z1, Z2 such that
A7: Z1
in
{X} & Z2
in SFY and
A8: Z
= (Z1
\ Z2) by
Def6;
x
in Z1 & not x
in Z2 by
A6,
A7,
TARSKI:def 1,
TARSKI:def 4;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
hence thesis by
A2,
Def1;
end;
hence thesis by
A3;
end;
theorem ::
SETFAM_1:27
SFY
<>
{} implies (X
\ (
meet SFY))
= (
union (
DIFFERENCE (
{X},SFY)))
proof
A1: X
in
{X} by
TARSKI:def 1;
A2: (
union (
DIFFERENCE (
{X},SFY)))
c= (X
\ (
meet SFY))
proof
let x be
object;
assume x
in (
union (
DIFFERENCE (
{X},SFY)));
then
consider Z such that
A3: x
in Z and
A4: Z
in (
DIFFERENCE (
{X},SFY)) by
TARSKI:def 4;
consider Z1, Z2 such that
A5: Z1
in
{X} and
A6: Z2
in SFY and
A7: Z
= (Z1
\ Z2) by
A4,
Def6;
not x
in Z2 by
A3,
A7,
XBOOLE_0:def 5;
then
A8: not x
in (
meet SFY) by
A6,
Def1;
Z1
= X by
A5,
TARSKI:def 1;
hence thesis by
A3,
A7,
A8,
XBOOLE_0:def 5;
end;
assume
A9: SFY
<>
{} ;
(X
\ (
meet SFY))
c= (
union (
DIFFERENCE (
{X},SFY)))
proof
let x be
object;
assume
A10: x
in (X
\ (
meet SFY));
then not x
in (
meet SFY) by
XBOOLE_0:def 5;
then
consider Z such that
A11: Z
in SFY and
A12: not x
in Z by
A9,
Def1;
A13: x
in (X
\ Z) by
A10,
A12,
XBOOLE_0:def 5;
(X
\ Z)
in (
DIFFERENCE (
{X},SFY)) by
A1,
A11,
Def6;
hence thesis by
A13,
TARSKI:def 4;
end;
hence thesis by
A2;
end;
theorem ::
SETFAM_1:28
(
union (
INTERSECTION (SFX,SFY)))
= ((
union SFX)
/\ (
union SFY))
proof
thus (
union (
INTERSECTION (SFX,SFY)))
c= ((
union SFX)
/\ (
union SFY))
proof
let x be
object;
assume x
in (
union (
INTERSECTION (SFX,SFY)));
then
consider Z such that
A1: x
in Z and
A2: Z
in (
INTERSECTION (SFX,SFY)) by
TARSKI:def 4;
consider X, Y such that
A3: X
in SFX and
A4: Y
in SFY and
A5: Z
= (X
/\ Y) by
A2,
Def5;
x
in Y by
A1,
A5,
XBOOLE_0:def 4;
then
A6: x
in (
union SFY) by
A4,
TARSKI:def 4;
x
in X by
A1,
A5,
XBOOLE_0:def 4;
then x
in (
union SFX) by
A3,
TARSKI:def 4;
hence thesis by
A6,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A7: x
in ((
union SFX)
/\ (
union SFY));
then x
in (
union SFX) by
XBOOLE_0:def 4;
then
consider X0 be
set such that
A8: x
in X0 & X0
in SFX by
TARSKI:def 4;
x
in (
union SFY) by
A7,
XBOOLE_0:def 4;
then
consider Y0 be
set such that
A9: x
in Y0 & Y0
in SFY by
TARSKI:def 4;
(X0
/\ Y0)
in (
INTERSECTION (SFX,SFY)) & x
in (X0
/\ Y0) by
A8,
A9,
Def5,
XBOOLE_0:def 4;
hence thesis by
TARSKI:def 4;
end;
theorem ::
SETFAM_1:29
SFX
<>
{} & SFY
<>
{} implies ((
meet SFX)
\/ (
meet SFY))
c= (
meet (
UNION (SFX,SFY)))
proof
set y = the
Element of SFX;
set z = the
Element of SFY;
assume SFX
<>
{} & SFY
<>
{} ;
then
A1: (y
\/ z)
in (
UNION (SFX,SFY)) by
Def4;
let x be
object;
assume x
in ((
meet SFX)
\/ (
meet SFY));
then
A2: x
in (
meet SFX) or x
in (
meet SFY) by
XBOOLE_0:def 3;
for Z st Z
in (
UNION (SFX,SFY)) holds x
in Z
proof
let Z;
assume Z
in (
UNION (SFX,SFY));
then
consider X, Y such that
A3: X
in SFX & Y
in SFY and
A4: Z
= (X
\/ Y) by
Def4;
x
in X or x
in Y by
A2,
A3,
Def1;
hence thesis by
A4,
XBOOLE_0:def 3;
end;
hence thesis by
A1,
Def1;
end;
theorem ::
SETFAM_1:30
(
meet (
DIFFERENCE (SFX,SFY)))
c= ((
meet SFX)
\ (
meet SFY))
proof
per cases ;
suppose
A1: SFX
=
{} or SFY
=
{} ;
now
assume (
DIFFERENCE (SFX,SFY))
<>
{} ;
then
consider e be
object such that
A2: e
in (
DIFFERENCE (SFX,SFY)) by
XBOOLE_0:def 1;
ex X, Y st X
in SFX & Y
in SFY & e
= (X
\ Y) by
A2,
Def6;
hence contradiction by
A1;
end;
then (
meet (
DIFFERENCE (SFX,SFY)))
=
{} by
Def1;
hence thesis;
end;
suppose
A3: SFX
<>
{} & SFY
<>
{} ;
set z = the
Element of SFX;
set y = the
Element of SFY;
let x be
object such that
A4: x
in (
meet (
DIFFERENCE (SFX,SFY)));
for Z st Z
in SFX holds x
in Z
proof
let Z;
assume Z
in SFX;
then (Z
\ y)
in (
DIFFERENCE (SFX,SFY)) by
A3,
Def6;
then x
in (Z
\ y) by
A4,
Def1;
hence thesis;
end;
then
A5: x
in (
meet SFX) by
A3,
Def1;
(z
\ y)
in (
DIFFERENCE (SFX,SFY)) by
A3,
Def6;
then x
in (z
\ y) by
A4,
Def1;
then not x
in y by
XBOOLE_0:def 5;
then not x
in (
meet SFY) by
A3,
Def1;
hence thesis by
A5,
XBOOLE_0:def 5;
end;
end;
definition
let D be
set;
mode
Subset-Family of D is
Subset of (
bool D);
end
reserve F,G for
Subset-Family of D;
reserve P for
Subset of D;
definition
let D, F;
:: original:
union
redefine
func
union F ->
Subset of D ;
coherence
proof
(
union F)
c= D
proof
let x be
object;
assume x
in (
union F);
then ex Z st x
in Z & Z
in F by
TARSKI:def 4;
hence thesis;
end;
hence thesis;
end;
end
definition
let D, F;
:: original:
meet
redefine
func
meet F ->
Subset of D ;
coherence
proof
(
meet F)
c= D
proof
A1: (
meet F)
c= (
union F) by
Th2;
let x be
object;
assume x
in (
meet F);
then x
in (
union F) by
A1;
hence thesis;
end;
hence thesis;
end;
end
theorem ::
SETFAM_1:31
Th31: (for P holds P
in F iff P
in G) implies F
= G
proof
assume
A1: for P holds P
in F iff P
in G;
thus F
c= G by
A1;
let x be
object;
assume x
in G;
hence thesis by
A1;
end;
definition
let D, F;
::
SETFAM_1:def7
func
COMPLEMENT (F) ->
Subset-Family of D means
:
Def7: for P be
Subset of D holds P
in it iff (P
` )
in F;
existence
proof
defpred
X[
Subset of D] means ($1
` )
in F;
thus ex G be
Subset-Family of D st for P be
Subset of D holds P
in G iff
X[P] from
SUBSET_1:sch 3;
end;
uniqueness
proof
let G,H be
Subset-Family of D;
assume that
A1: for P holds P
in G iff (P
` )
in F and
A2: for P holds P
in H iff (P
` )
in F;
now
let P;
P
in G iff (P
` )
in F by
A1;
hence P
in G iff P
in H by
A2;
end;
hence thesis by
Th31;
end;
involutiveness
proof
let F, G such that
A3: for P be
Subset of D holds P
in F iff (P
` )
in G;
let P be
Subset of D;
((P
` )
` )
= P;
hence thesis by
A3;
end;
end
theorem ::
SETFAM_1:32
Th32: F
<>
{} implies (
COMPLEMENT F)
<>
{}
proof
set X = the
Element of F;
assume
A1: F
<>
{} ;
then
reconsider X as
Subset of D by
TARSKI:def 3;
((X
` )
` )
= X;
hence thesis by
A1,
Def7;
end;
theorem ::
SETFAM_1:33
F
<>
{} implies ((
[#] D)
\ (
union F))
= (
meet (
COMPLEMENT F))
proof
A1: for x st x
in D holds (for X st X
in F holds not x
in X) iff for Y st Y
in (
COMPLEMENT F) holds x
in Y
proof
let x such that
A2: x
in D;
thus (for X st X
in F holds not x
in X) implies for Y st Y
in (
COMPLEMENT F) holds x
in Y
proof
assume
A3: for X st X
in F holds not x
in X;
let Y;
assume
A4: Y
in (
COMPLEMENT F);
then
reconsider Y as
Subset of D;
(Y
` )
in F by
A4,
Def7;
then not x
in (Y
` ) by
A3;
hence thesis by
A2,
XBOOLE_0:def 5;
end;
assume
A5: for Y st Y
in (
COMPLEMENT F) holds x
in Y;
let X;
assume
A6: X
in F;
then
reconsider X as
Subset of D;
((X
` )
` )
= X;
then (X
` )
in (
COMPLEMENT F) by
A6,
Def7;
then x
in (X
` ) by
A5;
hence thesis by
XBOOLE_0:def 5;
end;
assume F
<>
{} ;
then
A7: (
COMPLEMENT F)
<>
{} by
Th32;
A8: ((
[#] D)
\ (
union F))
c= (
meet (
COMPLEMENT F))
proof
let x be
object;
assume
A9: x
in ((
[#] D)
\ (
union F));
then not x
in (
union F) by
XBOOLE_0:def 5;
then for X st X
in F holds not x
in X by
TARSKI:def 4;
then for Y st Y
in (
COMPLEMENT F) holds x
in Y by
A1,
A9;
hence thesis by
A7,
Def1;
end;
(
meet (
COMPLEMENT F))
c= ((
[#] D)
\ (
union F))
proof
let x be
object;
assume
A10: x
in (
meet (
COMPLEMENT F));
then for X holds X
in (
COMPLEMENT F) implies x
in X by
Def1;
then for Y st x
in Y holds not Y
in F by
A1;
then not x
in (
union F) by
TARSKI:def 4;
hence thesis by
A10,
XBOOLE_0:def 5;
end;
hence thesis by
A8;
end;
theorem ::
SETFAM_1:34
F
<>
{} implies (
union (
COMPLEMENT F))
= ((
[#] D)
\ (
meet F))
proof
assume
A1: F
<>
{} ;
A2: ((
[#] D)
\ (
meet F))
c= (
union (
COMPLEMENT F))
proof
let x be
object;
assume
A3: x
in ((
[#] D)
\ (
meet F));
then not x
in (
meet F) by
XBOOLE_0:def 5;
then
consider X such that
A4: X
in F and
A5: not x
in X by
A1,
Def1;
reconsider X as
Subset of D by
A4;
reconsider XX = (X
` ) as
set;
A6: ((X
` )
` )
= X;
ex Y st x
in Y & Y
in (
COMPLEMENT F)
proof
take XX;
thus thesis by
A3,
A4,
A5,
A6,
Def7,
XBOOLE_0:def 5;
end;
hence thesis by
TARSKI:def 4;
end;
(
union (
COMPLEMENT F))
c= ((
[#] D)
\ (
meet F))
proof
let x be
object;
assume
A7: x
in (
union (
COMPLEMENT F));
then
consider X such that
A8: x
in X and
A9: X
in (
COMPLEMENT F) by
TARSKI:def 4;
reconsider X as
Subset of D by
A9;
reconsider XX = (X
` ) as
set;
ex Y st Y
in F & not x
in Y
proof
take Y = XX;
thus Y
in F by
A9,
Def7;
thus thesis by
A8,
XBOOLE_0:def 5;
end;
then not x
in (
meet F) by
Def1;
hence thesis by
A7,
XBOOLE_0:def 5;
end;
hence thesis by
A2;
end;
begin
theorem ::
SETFAM_1:35
for X be
set, F be
Subset-Family of X holds for P be
Subset of X holds (P
` )
in (
COMPLEMENT F) iff P
in F
proof
let X be
set, F be
Subset-Family of X;
let P be
Subset of X;
P
= ((P
` )
` );
hence thesis by
Def7;
end;
theorem ::
SETFAM_1:36
Th36: for X be
set, F,G be
Subset-Family of X st (
COMPLEMENT F)
c= (
COMPLEMENT G) holds F
c= G
proof
let X be
set, F,G be
Subset-Family of X such that
A1: (
COMPLEMENT F)
c= (
COMPLEMENT G);
let x be
object;
assume
A2: x
in F;
then
reconsider A = x as
Subset of X;
A
in (
COMPLEMENT (
COMPLEMENT F)) by
A2;
then (A
` )
in (
COMPLEMENT F) by
Def7;
then ((A
` )
` )
in G by
A1,
Def7;
hence thesis;
end;
theorem ::
SETFAM_1:37
for X be
set, F,G be
Subset-Family of X holds (
COMPLEMENT F)
c= G iff F
c= (
COMPLEMENT G)
proof
let X be
set, F,G be
Subset-Family of X;
hereby
assume (
COMPLEMENT F)
c= G;
then (
COMPLEMENT F)
c= (
COMPLEMENT (
COMPLEMENT G));
hence F
c= (
COMPLEMENT G) by
Th36;
end;
assume F
c= (
COMPLEMENT G);
then (
COMPLEMENT (
COMPLEMENT F))
c= (
COMPLEMENT G);
hence thesis by
Th36;
end;
theorem ::
SETFAM_1:38
for X be
set, F,G be
Subset-Family of X st (
COMPLEMENT F)
= (
COMPLEMENT G) holds F
= G
proof
let X be
set, F,G be
Subset-Family of X;
assume (
COMPLEMENT F)
= (
COMPLEMENT G);
hence F
= (
COMPLEMENT (
COMPLEMENT G))
.= G;
end;
theorem ::
SETFAM_1:39
for X be
set, F,G be
Subset-Family of X holds (
COMPLEMENT (F
\/ G))
= ((
COMPLEMENT F)
\/ (
COMPLEMENT G))
proof
let X be
set, F,G be
Subset-Family of X;
for P be
Subset of X holds P
in ((
COMPLEMENT F)
\/ (
COMPLEMENT G)) iff (P
` )
in (F
\/ G)
proof
let P be
Subset of X;
P
in (
COMPLEMENT F) or P
in (
COMPLEMENT G) iff (P
` )
in F or (P
` )
in G by
Def7;
hence thesis by
XBOOLE_0:def 3;
end;
hence thesis by
Def7;
end;
theorem ::
SETFAM_1:40
for X be
set, F be
Subset-Family of X st F
=
{X} holds (
COMPLEMENT F)
=
{
{} }
proof
let X be
set, F be
Subset-Family of X such that
A1: F
=
{X};
{}
c= X;
then
reconsider G =
{
{} } as
Subset-Family of X by
ZFMISC_1: 31;
reconsider G as
Subset-Family of X;
for P be
Subset of X holds P
in G iff (P
` )
in F
proof
let P be
Subset of X;
hereby
assume P
in G;
then P
= (
{} X) by
TARSKI:def 1;
hence (P
` )
in F by
A1,
TARSKI:def 1;
end;
assume (P
` )
in F;
then
A2: (P
` )
= (
[#] X) by
A1,
TARSKI:def 1;
P
= ((P
` )
` )
.=
{} by
A2,
XBOOLE_1: 37;
hence thesis by
TARSKI:def 1;
end;
hence thesis by
Def7;
end;
registration
let X be
set, F be
empty
Subset-Family of X;
cluster (
COMPLEMENT F) ->
empty;
coherence by
Def7;
end
definition
let IT be
set;
::
SETFAM_1:def8
attr IT is
with_non-empty_elements means
:
Def8: not
{}
in IT;
end
registration
cluster non
empty
with_non-empty_elements for
set;
existence
proof
take
{
{
{} }};
thus
{
{
{} }} is non
empty;
assume
{}
in
{
{
{} }};
hence contradiction by
TARSKI:def 1;
end;
end
registration
let A be non
empty
set;
cluster
{A} ->
with_non-empty_elements;
coherence by
TARSKI:def 1;
let B be non
empty
set;
cluster
{A, B} ->
with_non-empty_elements;
coherence by
TARSKI:def 2;
let C be non
empty
set;
cluster
{A, B, C} ->
with_non-empty_elements;
coherence by
ENUMSET1:def 1;
let D be non
empty
set;
cluster
{A, B, C, D} ->
with_non-empty_elements;
coherence by
ENUMSET1:def 2;
let E be non
empty
set;
cluster
{A, B, C, D, E} ->
with_non-empty_elements;
coherence by
ENUMSET1:def 3;
let F be non
empty
set;
cluster
{A, B, C, D, E, F} ->
with_non-empty_elements;
coherence by
ENUMSET1:def 4;
let G be non
empty
set;
cluster
{A, B, C, D, E, F, G} ->
with_non-empty_elements;
coherence by
ENUMSET1:def 5;
let H be non
empty
set;
cluster
{A, B, C, D, E, F, G, H} ->
with_non-empty_elements;
coherence by
ENUMSET1:def 6;
let I be non
empty
set;
cluster
{A, B, C, D, E, F, G, H, I} ->
with_non-empty_elements;
coherence by
ENUMSET1:def 7;
let J be non
empty
set;
cluster
{A, B, C, D, E, F, G, H, I, J} ->
with_non-empty_elements;
coherence by
ENUMSET1:def 8;
end
registration
let A,B be
with_non-empty_elements
set;
cluster (A
\/ B) ->
with_non-empty_elements;
coherence
proof
( not
{}
in A) & not
{}
in B by
Def8;
then not
{}
in (A
\/ B) by
XBOOLE_0:def 3;
hence thesis;
end;
end
theorem ::
SETFAM_1:41
(
union Y)
c= Z & X
in Y implies X
c= Z
proof
assume that
A1: (
union Y)
c= Z and
A2: X
in Y;
thus X
c= Z
proof
let x be
object;
assume x
in X;
then x
in (
union Y) by
A2,
TARSKI:def 4;
hence thesis by
A1;
end;
end;
theorem ::
SETFAM_1:42
for A,B,X be
set holds (X
c= (
union (A
\/ B)) & for Y be
set st Y
in B holds Y
misses X) implies X
c= (
union A)
proof
let A,B,X be
set;
assume X
c= (
union (A
\/ B));
then X
c= ((
union (A
\/ B))
/\ X) by
XBOOLE_1: 19;
then X
c= (((
union A)
\/ (
union B))
/\ X) by
ZFMISC_1: 78;
then
A1: X
c= (((
union A)
/\ X)
\/ ((
union B)
/\ X)) by
XBOOLE_1: 23;
assume for Y st Y
in B holds Y
misses X;
then (
union B)
misses X by
ZFMISC_1: 80;
then
A2: ((
union B)
/\ X)
=
{} ;
((
union A)
/\ X)
c= (
union A) by
XBOOLE_1: 17;
hence thesis by
A2,
A1;
end;
definition
let M be
set;
let B be
Subset-Family of M;
::
SETFAM_1:def9
func
Intersect B ->
Subset of M equals
:
Def9: (
meet B) if B
<>
{}
otherwise M;
coherence
proof
M
c= M;
hence thesis;
end;
consistency ;
end
theorem ::
SETFAM_1:43
Th43: for X,x be
set, R be
Subset-Family of X st x
in X holds x
in (
Intersect R) iff for Y be
set st Y
in R holds x
in Y
proof
let X,x be
set, R be
Subset-Family of X;
assume
A1: x
in X;
hereby
assume
A2: x
in (
Intersect R);
let Y be
set;
assume
A3: Y
in R;
then (
Intersect R)
= (
meet R) by
Def9;
hence x
in Y by
A2,
A3,
Def1;
end;
assume
A4: for Y be
set st Y
in R holds x
in Y;
per cases ;
suppose
A5: R
<>
{} ;
then x
in (
meet R) by
A4,
Def1;
hence thesis by
A5,
Def9;
end;
suppose R
=
{} ;
hence thesis by
A1,
Def9;
end;
end;
theorem ::
SETFAM_1:44
for X be
set holds for H,J be
Subset-Family of X st H
c= J holds (
Intersect J)
c= (
Intersect H)
proof
let X be
set;
let H,J be
Subset-Family of X such that
A1: H
c= J;
let x be
object;
assume
A2: x
in (
Intersect J);
then for Y be
set st Y
in H holds x
in Y by
A1,
Th43;
hence thesis by
A2,
Th43;
end;
registration
let X be non
empty
with_non-empty_elements
set;
cluster -> non
empty for
Element of X;
coherence by
Def8;
end
reserve E for
set;
definition
let E;
::
SETFAM_1:def10
attr E is
empty-membered means
:
Def10: not ex x be non
empty
set st x
in E;
end
notation
let E;
antonym E is
with_non-empty_element for E is
empty-membered;
end
registration
cluster
with_non-empty_element for
set;
existence
proof
take
{
{
{} }},
{
{} };
thus thesis by
TARSKI:def 1;
end;
end
registration
cluster
with_non-empty_element -> non
empty for
set;
coherence ;
end
registration
let X be
with_non-empty_element
set;
cluster non
empty for
Element of X;
existence
proof
ex x be non
empty
set st x
in X by
Def10;
hence thesis;
end;
end
registration
let D be non
empty
with_non-empty_elements
set;
cluster (
union D) -> non
empty;
coherence
proof
set d = the
Element of D;
d
c= (
union D) by
ZFMISC_1: 74;
hence thesis;
end;
end
registration
cluster non
empty
with_non-empty_elements ->
with_non-empty_element for
set;
coherence ;
end
definition
let X be
set;
::
SETFAM_1:def11
mode
Cover of X ->
set means
:
Def11: X
c= (
union it );
existence
proof
take
{X};
thus thesis by
ZFMISC_1: 25;
end;
end
theorem ::
SETFAM_1:45
for X be
set, F be
Subset-Family of X holds F is
Cover of X iff (
union F)
= X by
Def11;
theorem ::
SETFAM_1:46
Th46:
{
{} } is
Subset-Family of X
proof
{}
c= X;
hence thesis by
ZFMISC_1: 31;
end;
definition
let X be
set;
let F be
Subset-Family of X;
::
SETFAM_1:def12
attr F is
with_proper_subsets means
:
Def12: not X
in F;
end
theorem ::
SETFAM_1:47
for TS be
set, F,G be
Subset-Family of TS st F is
with_proper_subsets & G
c= F holds G is
with_proper_subsets;
registration
let TS be non
empty
set;
cluster
with_proper_subsets for
Subset-Family of TS;
existence
proof
reconsider F =
{
{} } as
Subset-Family of TS by
Th46;
take F;
assume TS
in F;
hence thesis by
TARSKI:def 1;
end;
end
theorem ::
SETFAM_1:48
for TS be non
empty
set, A,B be
with_proper_subsets
Subset-Family of TS holds (A
\/ B) is
with_proper_subsets
proof
let TS be non
empty
set, A,B be
with_proper_subsets
Subset-Family of TS;
assume TS
in (A
\/ B);
then TS
in A or TS
in B by
XBOOLE_0:def 3;
hence thesis by
Def12;
end;
registration
cluster non
trivial ->
with_non-empty_element for
set;
coherence
proof
let W be
set;
assume W is non
trivial;
then
consider w1,w2 be
object such that
A1: w1
in W & w2
in W and
A2: w1
<> w2 by
ZFMISC_1:def 10;
w1
<>
{} or w2
<>
{} by
A2;
hence thesis by
A1;
end;
end
definition
let X be
set;
:: original:
bool
redefine
func
bool X ->
Subset-Family of X ;
coherence by
ZFMISC_1:def 1;
end
theorem ::
SETFAM_1:49
for A be non
empty
set, b be
object st A
<>
{b} holds ex a be
Element of A st a
<> b
proof
let A be non
empty
set, b be
object such that
A1: A
<>
{b};
assume
A2: for a be
Element of A holds a
= b;
now
set a0 = the
Element of A;
let a be
object;
thus a
in A implies a
= b by
A2;
assume
A3: a
= b;
a0
= b by
A2;
hence a
in A by
A3;
end;
hence contradiction by
A1,
TARSKI:def 1;
end;