setwiseo.miz
begin
reserve x,y,z,X,Y for
set;
theorem ::
SETWISEO:1
Th1:
{x}
c=
{x, y, z}
proof
{x, y, z}
= (
{x}
\/
{y, z}) by
ENUMSET1: 2;
hence thesis by
XBOOLE_1: 7;
end;
theorem ::
SETWISEO:2
Th2:
{x, y}
c=
{x, y, z}
proof
{x, y, z}
= (
{x, y}
\/
{z}) by
ENUMSET1: 3;
hence thesis by
XBOOLE_1: 7;
end;
::$Canceled
theorem ::
SETWISEO:6
Th3: for X, Y holds for f be
Function holds (f
.: (Y
\ (f
" X)))
= ((f
.: Y)
\ X)
proof
let X, Y;
let f be
Function;
now
let x be
object;
thus x
in (f
.: (Y
\ (f
" X))) implies x
in ((f
.: Y)
\ X)
proof
assume x
in (f
.: (Y
\ (f
" X)));
then
consider z be
object such that
A1: z
in (
dom f) and
A2: z
in (Y
\ (f
" X)) and
A3: (f
. z)
= x by
FUNCT_1:def 6;
not z
in (f
" X) by
A2,
XBOOLE_0:def 5;
then
A4: not x
in X by
A1,
A3,
FUNCT_1:def 7;
(f
. z)
in (f
.: Y) by
A1,
A2,
FUNCT_1:def 6;
hence thesis by
A3,
A4,
XBOOLE_0:def 5;
end;
assume
A5: x
in ((f
.: Y)
\ X);
then
consider z be
object such that
A6: z
in (
dom f) and
A7: z
in Y and
A8: (f
. z)
= x by
FUNCT_1:def 6;
not x
in X by
A5,
XBOOLE_0:def 5;
then not z
in (f
" X) by
A8,
FUNCT_1:def 7;
then z
in (Y
\ (f
" X)) by
A7,
XBOOLE_0:def 5;
hence x
in (f
.: (Y
\ (f
" X))) by
A6,
A8,
FUNCT_1:def 6;
end;
hence thesis by
TARSKI: 2;
end;
reserve X,Y for non
empty
set,
f for
Function of X, Y;
theorem ::
SETWISEO:7
Th4: for x be
Element of X holds x
in (f
"
{(f
. x)})
proof
let x be
Element of X;
(f
. x)
in
{(f
. x)} by
TARSKI:def 1;
hence thesis by
FUNCT_2: 38;
end;
theorem ::
SETWISEO:8
Th5: for x be
Element of X holds (
Im (f,x))
=
{(f
. x)}
proof
let x be
Element of X;
for y be
object holds y
in (f
.:
{x}) iff y
= (f
. x)
proof
let y be
object;
thus y
in (f
.:
{x}) implies y
= (f
. x)
proof
assume y
in (f
.:
{x});
then ex z be
object st z
in (
dom f) & z
in
{x} & (f
. z)
= y by
FUNCT_1:def 6;
hence thesis by
TARSKI:def 1;
end;
x
in
{x} by
TARSKI:def 1;
hence thesis by
FUNCT_2: 35;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
SETWISEO:9
Th6: for B be
Element of (
Fin X) holds for x st x
in B holds x is
Element of X
proof
let B be
Element of (
Fin X);
A1: B
c= X by
FINSUB_1:def 5;
let x;
assume x
in B;
hence thesis by
A1;
end;
theorem ::
SETWISEO:10
for A be
Element of (
Fin X), B be
set holds for f be
Function of X, Y st for x be
Element of X holds x
in A implies (f
. x)
in B holds (f
.: A)
c= B
proof
let A be
Element of (
Fin X), B be
set;
let f be
Function of X, Y such that
A1: for x be
Element of X holds x
in A implies (f
. x)
in B;
let x be
object;
assume x
in (f
.: A);
then
consider y be
object such that y
in (
dom f) and
A2: y
in A and
A3: x
= (f
. y) by
FUNCT_1:def 6;
reconsider y as
Element of X by
A2,
Th6;
x
= (f
. y) by
A3;
hence thesis by
A1,
A2;
end;
theorem ::
SETWISEO:11
Th8: for X be
set holds for B be
Element of (
Fin X) holds for A be
set st A
c= B holds A is
Element of (
Fin X)
proof
let X be
set, B be
Element of (
Fin X);
let A be
set such that
A1: A
c= B;
B
c= X by
FINSUB_1:def 5;
then A
c= X by
A1;
hence thesis by
A1,
FINSUB_1:def 5;
end;
Lm1: for A be
Element of (
Fin X) holds (f
.: A) is
Element of (
Fin Y) by
FINSUB_1:def 5;
theorem ::
SETWISEO:12
Th9: for B be
Element of (
Fin X) st B
<>
{} holds ex x be
Element of X st x
in B
proof
let B be
Element of (
Fin X);
set x = the
Element of B;
assume
A1: B
<>
{} ;
then
reconsider x as
Element of X by
Th6;
take x;
thus thesis by
A1;
end;
theorem ::
SETWISEO:13
Th10: for A be
Element of (
Fin X) holds (f
.: A)
=
{} implies A
=
{}
proof
let A be
Element of (
Fin X);
assume
A1: (f
.: A)
=
{} ;
assume A
<>
{} ;
then
consider x be
Element of X such that
A2: x
in A by
Th9;
(f
. x)
in (f
.: A) by
A2,
FUNCT_2: 35;
hence contradiction by
A1;
end;
registration
let X be
set;
cluster
empty for
Element of (
Fin X);
existence
proof
{} is
Element of (
Fin X) by
FINSUB_1: 7;
hence thesis;
end;
end
definition
let X be
set;
::
SETWISEO:def1
func
{}. X ->
empty
Element of (
Fin X) equals
{} ;
coherence by
FINSUB_1: 7;
end
scheme ::
SETWISEO:sch1
FinSubFuncEx { A() -> non
empty
set , B() ->
Element of (
Fin A()) , P[
set,
set] } :
ex f be
Function of A(), (
Fin A()) st for b,a be
Element of A() holds a
in (f
. b) iff a
in B() & P[a, b];
defpred
X[
set,
Element of (
Fin A())] means for a be
Element of A() holds a
in $2 iff a
in B() & P[a, $1];
A1:
now
reconsider B = B() as
Subset of A() by
FINSUB_1:def 5;
let x be
Element of A();
defpred
X[
set] means $1
in B() & P[$1, x];
consider y be
Subset of A() such that
A2: for a be
Element of A() holds a
in y iff
X[a] from
SUBSET_1:sch 3;
for x be
Element of A() holds x
in y implies x
in B by
A2;
then y
c= B();
then
reconsider y as
Element of (
Fin A()) by
FINSUB_1:def 5;
take y9 = y;
thus
X[x, y9] by
A2;
end;
thus ex f be
Function of A(), (
Fin A()) st for x be
Element of A() holds
X[x, (f
. x)] from
FUNCT_2:sch 3(
A1);
end;
definition
let X be non
empty
set, F be
BinOp of X;
::
SETWISEO:def2
attr F is
having_a_unity means ex x be
Element of X st x
is_a_unity_wrt F;
end
theorem ::
SETWISEO:14
Th11: for X be non
empty
set, F be
BinOp of X holds F is
having_a_unity iff (
the_unity_wrt F)
is_a_unity_wrt F by
BINOP_1:def 8;
theorem ::
SETWISEO:15
Th12: for X be non
empty
set, F be
BinOp of X st F is
having_a_unity holds for x be
Element of X holds (F
. ((
the_unity_wrt F),x))
= x & (F
. (x,(
the_unity_wrt F)))
= x
proof
let X be non
empty
set, F be
BinOp of X;
assume F is
having_a_unity;
then
A1: (
the_unity_wrt F)
is_a_unity_wrt F by
Th11;
let x be
Element of X;
thus thesis by
A1,
BINOP_1: 3;
end;
registration
let X be non
empty
set;
cluster non
empty for
Element of (
Fin X);
existence
proof
set x = the
Element of X;
{x} is
Subset of X by
SUBSET_1: 41;
then
{x} is
Element of (
Fin X) by
FINSUB_1:def 5;
hence thesis;
end;
end
notation
let X be non
empty
set, x be
Element of X;
synonym
{.x.} for
{x};
let y be
Element of X;
synonym
{.x,y.} for
{x,y};
let z be
Element of X;
synonym
{.x,y,z.} for
{x,y,z};
end
definition
let X be non
empty
set, x be
Element of X;
:: original:
{.
redefine
func
{.x.} ->
Element of (
Fin X) ;
coherence
proof
{x} is
Subset of X by
SUBSET_1: 41;
hence thesis by
FINSUB_1:def 5;
end;
let y be
Element of X;
:: original:
{.
redefine
func
{.x,y.} ->
Element of (
Fin X) ;
coherence
proof
{x, y} is
Subset of X by
SUBSET_1: 34;
hence thesis by
FINSUB_1:def 5;
end;
let z be
Element of X;
:: original:
{.
redefine
func
{.x,y,z.} ->
Element of (
Fin X) ;
coherence
proof
{x, y, z} is
Subset of X by
SUBSET_1: 35;
hence thesis by
FINSUB_1:def 5;
end;
end
definition
let X be
set;
let A,B be
Element of (
Fin X);
:: original:
\/
redefine
func A
\/ B ->
Element of (
Fin X) ;
coherence by
FINSUB_1: 1;
end
definition
let X be
set;
let A,B be
Element of (
Fin X);
:: original:
\
redefine
func A
\ B ->
Element of (
Fin X) ;
coherence by
FINSUB_1: 1;
end
scheme ::
SETWISEO:sch2
FinSubInd1 { X() -> non
empty
set , P[
set] } :
for B be
Element of (
Fin X()) holds P[B]
provided
A1: P[(
{}. X())]
and
A2: for B9 be
Element of (
Fin X()), b be
Element of X() holds P[B9] & not b
in B9 implies P[(B9
\/
{b})];
defpred
X[
set] means ex B9 be
Element of (
Fin X()) st B9
= $1 & P[B9];
let B be
Element of (
Fin X());
A3: for x,A be
set st x
in B & A
c= B &
X[A] holds
X[(A
\/
{x})]
proof
let x,A be
set such that
A4: x
in B and
A5: A
c= B and
A6: ex B9 be
Element of (
Fin X()) st B9
= A & P[B9];
reconsider x9 = x as
Element of X() by
A4,
Th6;
reconsider A9 = A as
Element of (
Fin X()) by
A5,
Th8;
take Ax = (A9
\/
{.x9.});
thus Ax
= (A
\/
{x});
thus P[Ax] by
A2,
A6,
ZFMISC_1: 40;
end;
A7: B is
finite;
A8:
X[
{} ] by
A1;
X[B] from
FINSET_1:sch 2(
A7,
A8,
A3);
hence thesis;
end;
scheme ::
SETWISEO:sch3
FinSubInd2 { X() -> non
empty
set , P[
Element of (
Fin X())] } :
for B be non
empty
Element of (
Fin X()) holds P[B]
provided
A1: for x be
Element of X() holds P[
{.x.}]
and
A2: for B1,B2 be non
empty
Element of (
Fin X()) st P[B1] & P[B2] holds P[(B1
\/ B2)];
defpred
X[
set] means $1
<>
{} implies ex B9 be
Element of (
Fin X()) st B9
= $1 & P[B9];
let B be non
empty
Element of (
Fin X());
A3: for x,A be
set st x
in B & A
c= B &
X[A] holds
X[(A
\/
{x})]
proof
let x,A be
set such that
A4: x
in B and
A5: A
c= B and
A6: A
<>
{} implies ex B9 be
Element of (
Fin X()) st B9
= A & P[B9] and (A
\/
{x})
<>
{} ;
reconsider x9 = x as
Element of X() by
A4,
Th6;
reconsider A9 = A as
Element of (
Fin X()) by
A5,
Th8;
take (A9
\/
{.x9.});
thus (A9
\/
{.x9.})
= (A
\/
{x});
A7: P[
{.x9.}] by
A1;
per cases ;
suppose A
=
{} ;
hence thesis by
A1;
end;
suppose A
<>
{} ;
hence thesis by
A2,
A6,
A7;
end;
end;
A8:
X[
{} ];
A9: B is
finite;
X[B] from
FINSET_1:sch 2(
A9,
A8,
A3);
hence thesis;
end;
scheme ::
SETWISEO:sch4
FinSubInd3 { X() -> non
empty
set , P[
set] } :
for B be
Element of (
Fin X()) holds P[B]
provided
A1: P[(
{}. X())]
and
A2: for B9 be
Element of (
Fin X()), b be
Element of X() holds P[B9] implies P[(B9
\/
{b})];
A3: for B9 be
Element of (
Fin X()), b be
Element of X() holds P[B9] & not b
in B9 implies P[(B9
\/
{b})] by
A2;
A4: P[(
{}. X())] by
A1;
thus for B be
Element of (
Fin X()) holds P[B] from
FinSubInd1(
A4,
A3);
end;
definition
let X,Y be non
empty
set;
let F be
BinOp of Y;
let B be
Element of (
Fin X);
let f be
Function of X, Y;
assume that
A1: B
<>
{} or F is
having_a_unity and
A2: F is
commutative and
A3: F is
associative;
::
SETWISEO:def3
func F
$$ (B,f) ->
Element of Y means
:
Def3: ex G be
Function of (
Fin X), Y st it
= (G
. B) & (for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e) & (for x be
Element of X holds (G
.
{x})
= (f
. x)) & for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in (B
\ B9) holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)));
existence
proof
defpred
X[
set] means ex G be
Function of (
Fin X), Y st (for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e) & (for x be
Element of X holds (G
.
{x})
= (f
. x)) & for B9 be
Element of (
Fin X) st B9
c= $1 & B9
<>
{} holds for x be
Element of X st x
in ($1
\ B9) holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)));
A4: for B9 be
Element of (
Fin X), b be
Element of X holds
X[B9] & not b
in B9 implies
X[(B9
\/
{b})]
proof
let B be
Element of (
Fin X), x be
Element of X;
given G be
Function of (
Fin X), Y such that
A5: for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e and
A6: for x be
Element of X holds (G
.
{x})
= (f
. x) and
A7: for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in (B
\ B9) holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)));
assume
A8: not x
in B;
thus ex G be
Function of (
Fin X), Y st (for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e) & (for x be
Element of X holds (G
.
{x})
= (f
. x)) & for B9 be
Element of (
Fin X) st B9
c= (B
\/
{x}) & B9
<>
{} holds for x9 be
Element of X st x9
in ((B
\/
{x})
\ B9) holds (G
. (B9
\/
{x9}))
= (F
. ((G
. B9),(f
. x9)))
proof
defpred
X[
set,
set] means (for C be
Element of (
Fin X) st C
<>
{} & C
c= B & $1
= (C
\/
{.x.}) holds $2
= (F
. ((G
. C),(f
. x)))) & (( not ex C be
Element of (
Fin X) st C
<>
{} & C
c= B & $1
= (C
\/
{.x.})) implies $2
= (G
. $1));
A9:
now
let B9 be
Element of (
Fin X);
thus ex y be
Element of Y st
X[B9, y]
proof
A10:
now
given C be
Element of (
Fin X) such that
A11: C
<>
{} and
A12: C
c= B and
A13: B9
= (C
\/
{x});
take y = (F
. ((G
. C),(f
. x)));
for C be
Element of (
Fin X) st C
<>
{} & C
c= B & B9
= (C
\/
{x}) holds y
= (F
. ((G
. C),(f
. x)))
proof
not x
in C by
A8,
A12;
then
A14: C
c= (B9
\
{x}) by
A13,
XBOOLE_1: 7,
ZFMISC_1: 34;
(B9
\
{x})
= (C
\
{x}) by
A13,
XBOOLE_1: 40;
then
A15: (B9
\
{x})
= C by
A14,
XBOOLE_0:def 10;
let C1 be
Element of (
Fin X) such that C1
<>
{} and
A16: C1
c= B and
A17: B9
= (C1
\/
{x});
not x
in C1 by
A8,
A16;
then
A18: C1
c= (B9
\
{x}) by
A17,
XBOOLE_1: 7,
ZFMISC_1: 34;
(B9
\
{x})
= (C1
\
{x}) by
A17,
XBOOLE_1: 40;
hence thesis by
A18,
A15,
XBOOLE_0:def 10;
end;
hence thesis by
A11,
A12,
A13;
end;
now
assume
A19: not ex C be
Element of (
Fin X) st C
<>
{} & C
c= B & B9
= (C
\/
{x});
take y = (G
. B9);
thus for C be
Element of (
Fin X) st C
<>
{} & C
c= B & B9
= (C
\/
{x}) holds y
= (F
. ((G
. C),(f
. x))) by
A19;
thus ( not ex C be
Element of (
Fin X) st C
<>
{} & C
c= B & B9
= (C
\/
{x})) implies y
= (G
. B9);
end;
hence thesis by
A10;
end;
end;
consider H be
Function of (
Fin X), Y such that
A20: for B9 be
Element of (
Fin X) holds
X[B9, (H
. B9)] from
FUNCT_2:sch 3(
A9);
take J = H;
now
given C be
Element of (
Fin X) such that
A21: C
<>
{} and
A22: C
c= B and
A23:
{x}
= (C
\/
{x});
C
=
{x} by
A21,
A23,
XBOOLE_1: 7,
ZFMISC_1: 33;
then x
in C by
TARSKI:def 1;
hence contradiction by
A8,
A22;
end;
then
A24: (J
.
{x})
= (G
.
{.x.}) by
A20;
thus for e be
Element of Y st e
is_a_unity_wrt F holds (J
.
{} )
= e
proof
reconsider E =
{} as
Element of (
Fin X) by
FINSUB_1: 7;
not ex C be
Element of (
Fin X) st C
<>
{} & C
c= B & E
= (C
\/
{x});
then (J
. E)
= (G
. E) by
A20;
hence thesis by
A5;
end;
thus for x be
Element of X holds (J
.
{x})
= (f
. x)
proof
let x9 be
Element of X;
now
given C be
Element of (
Fin X) such that
A25: C
<>
{} and
A26: C
c= B and
A27:
{x9}
= (C
\/
{x});
A28: C
=
{x9} by
A25,
A27,
XBOOLE_1: 7,
ZFMISC_1: 33;
x
= x9 by
A27,
XBOOLE_1: 7,
ZFMISC_1: 18;
then x
in C by
A28,
TARSKI:def 1;
hence contradiction by
A8,
A26;
end;
hence (J
.
{x9})
= (G
.
{.x9.}) by
A20
.= (f
. x9) by
A6;
end;
let B9 be
Element of (
Fin X) such that
A29: B9
c= (B
\/
{x}) and
A30: B9
<>
{} ;
let x9 be
Element of X;
assume
A31: x9
in ((B
\/
{x})
\ B9);
then
A32: not x9
in B9 by
XBOOLE_0:def 5;
per cases ;
suppose
A33: x
in B9;
then
A34: x9
in B by
A31,
A32,
ZFMISC_1: 136;
per cases ;
suppose
A35: B9
=
{x};
hence (J
. (B9
\/
{.x9.}))
= (F
. ((G
.
{.x9.}),(f
. x))) by
A20,
A34,
ZFMISC_1: 31
.= (F
. ((f
. x9),(f
. x))) by
A6
.= (F
. ((f
. x),(f
. x9))) by
A2
.= (F
. ((J
. B9),(f
. x9))) by
A6,
A24,
A35;
end;
suppose B9
<>
{x};
then not B9
c=
{x} by
A30,
ZFMISC_1: 33;
then
A36: (B9
\
{x})
<>
{} by
XBOOLE_1: 37;
set C = ((B9
\
{.x.})
\/
{.x9.});
not x9
in (B9
\
{x}) by
A31,
XBOOLE_0:def 5;
then
A37: x9
in (B
\ (B9
\
{x})) by
A34,
XBOOLE_0:def 5;
(B9
\
{x})
c= B by
A29,
XBOOLE_1: 43;
then
A38: C
c= B by
A33,
A31,
A32,
ZFMISC_1: 136,
ZFMISC_1: 137;
(B9
\/
{.x9.})
= ((B9
\/
{x})
\/
{x9}) by
A33,
ZFMISC_1: 40
.= (((B9
\
{x})
\/
{x})
\/
{x9}) by
XBOOLE_1: 39
.= (C
\/
{.x.}) by
XBOOLE_1: 4;
hence (J
. (B9
\/
{.x9.}))
= (F
. ((G
. C),(f
. x))) by
A20,
A38
.= (F
. ((F
. ((G
. (B9
\
{.x.})),(f
. x9))),(f
. x))) by
A7,
A29,
A36,
A37,
XBOOLE_1: 43
.= (F
. ((G
. (B9
\
{.x.})),(F
. ((f
. x9),(f
. x))))) by
A3
.= (F
. ((G
. (B9
\
{x})),(F
. ((f
. x),(f
. x9))))) by
A2
.= (F
. ((F
. ((G
. (B9
\
{.x.})),(f
. x))),(f
. x9))) by
A3
.= (F
. ((J
. ((B9
\
{.x.})
\/
{.x.})),(f
. x9))) by
A20,
A29,
A36,
XBOOLE_1: 43
.= (F
. ((J
. (B9
\/
{x})),(f
. x9))) by
XBOOLE_1: 39
.= (F
. ((J
. B9),(f
. x9))) by
A33,
ZFMISC_1: 40;
end;
end;
suppose
A39: not x
in B9;
then
A40: B9
c= B by
A29,
ZFMISC_1: 135;
A41: not ex C be
Element of (
Fin X) st C
<>
{} & C
c= B & B9
= (C
\/
{x}) by
A39,
ZFMISC_1: 136;
per cases ;
suppose
A42: x
<> x9;
then x9
in B by
A31,
ZFMISC_1: 136;
then
A43: x9
in (B
\ B9) by
A32,
XBOOLE_0:def 5;
not x
in (B9
\/
{x9}) by
A39,
A42,
ZFMISC_1: 136;
then not ex C be
Element of (
Fin X) st C
<>
{} & C
c= B & (B9
\/
{x9})
= (C
\/
{x}) by
ZFMISC_1: 136;
hence (J
. (B9
\/
{.x9.}))
= (G
. (B9
\/
{.x9.})) by
A20
.= (F
. ((G
. B9),(f
. x9))) by
A7,
A30,
A40,
A43
.= (F
. ((J
. B9),(f
. x9))) by
A20,
A41;
end;
suppose x
= x9;
hence (J
. (B9
\/
{.x9.}))
= (F
. ((G
. B9),(f
. x9))) by
A20,
A29,
A30,
A39,
ZFMISC_1: 135
.= (F
. ((J
. B9),(f
. x9))) by
A20,
A41;
end;
end;
end;
end;
A44:
X[(
{}. X)]
proof
consider e be
Element of Y such that
A45: (ex e be
Element of Y st e
is_a_unity_wrt F) implies e
= (
the_unity_wrt F);
defpred
X[
set,
set] means (for x9 be
Element of X st $1
=
{x9} holds $2
= (f
. x9)) & ( not (ex x9 be
Element of X st $1
=
{x9}) implies $2
= e);
A46:
now
let x be
Element of (
Fin X);
A47:
now
given x9 be
Element of X such that
A48: x
=
{x9};
take y = (f
. x9);
thus for x9 be
Element of X st x
=
{x9} holds y
= (f
. x9) by
A48,
ZFMISC_1: 3;
thus not (ex x9 be
Element of X st x
=
{x9}) implies y
= e by
A48;
end;
now
assume
A49: not ex x9 be
Element of X st x
=
{x9};
take y = e;
thus (for x9 be
Element of X st x
=
{x9} holds y
= (f
. x9)) & ( not (ex x9 be
Element of X st x
=
{x9}) implies y
= e) by
A49;
end;
hence ex y be
Element of Y st
X[x, y] by
A47;
end;
consider G9 be
Function of (
Fin X), Y such that
A50: for B9 be
Element of (
Fin X) holds
X[B9, (G9
. B9)] from
FUNCT_2:sch 3(
A46);
take G = G9;
thus for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e
proof
reconsider E =
{} as
Element of (
Fin X) by
FINSUB_1: 7;
let e9 be
Element of Y such that
A51: e9
is_a_unity_wrt F;
not ex x9 be
Element of X st E
=
{x9};
hence (G
.
{} )
= e by
A50
.= e9 by
A45,
A51,
BINOP_1:def 8;
end;
thus for x be
Element of X holds (G
.
{.x.})
= (f
. x) by
A50;
thus for B9 be
Element of (
Fin X) st B9
c= (
{}. X) & B9
<>
{} holds for x be
Element of X st x
in ((
{}. X)
\ B9) holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)));
end;
for B be
Element of (
Fin X) holds
X[B] from
FinSubInd1(
A44,
A4);
then
consider G be
Function of (
Fin X), Y such that
A52: ((for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e) & for x be
Element of X holds (G
.
{x})
= (f
. x)) & for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in (B
\ B9) holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)));
take (G
. B), G;
thus thesis by
A52;
end;
uniqueness
proof
let x,y be
Element of Y;
given G1 be
Function of (
Fin X), Y such that
A53: x
= (G1
. B) and
A54: for e be
Element of Y st e
is_a_unity_wrt F holds (G1
.
{} )
= e and
A55: for x be
Element of X holds (G1
.
{x})
= (f
. x) and
A56: for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in (B
\ B9) holds (G1
. (B9
\/
{x}))
= (F
. ((G1
. B9),(f
. x)));
given G2 be
Function of (
Fin X), Y such that
A57: y
= (G2
. B) and
A58: for e be
Element of Y st e
is_a_unity_wrt F holds (G2
.
{} )
= e and
A59: for x be
Element of X holds (G2
.
{x})
= (f
. x) and
A60: for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in (B
\ B9) holds (G2
. (B9
\/
{x}))
= (F
. ((G2
. B9),(f
. x)));
per cases ;
suppose
A61: B
=
{} ;
thus x
= (
the_unity_wrt F) by
A53,
A54,
A61,
A1,
Th11
.= y by
A57,
A58,
A61,
A1,
Th11;
end;
suppose
A62: B
<>
{} ;
defpred
X[
set] means $1
c= B & $1
<>
{} implies (G1
. $1)
= (G2
. $1);
A63: for B9 be
Element of (
Fin X), b be
Element of X holds
X[B9] & not b
in B9 implies
X[(B9
\/
{b})]
proof
let B9 be
Element of (
Fin X), x be
Element of X;
assume
A64: B9
c= B & B9
<>
{} implies (G1
. B9)
= (G2
. B9);
assume
A65: not x
in B9;
assume
A66: (B9
\/
{x})
c= B;
then
A67: B9
c= B by
ZFMISC_1: 137;
assume (B9
\/
{x})
<>
{} ;
x
in B by
A66,
ZFMISC_1: 137;
then
A68: x
in (B
\ B9) by
A65,
XBOOLE_0:def 5;
per cases ;
suppose
A69: B9
=
{} ;
hence (G1
. (B9
\/
{x}))
= (f
. x) by
A55
.= (G2
. (B9
\/
{x})) by
A59,
A69;
end;
suppose
A70: B9
<>
{} ;
hence (G1
. (B9
\/
{x}))
= (F
. ((G1
. B9),(f
. x))) by
A56,
A67,
A68
.= (G2
. (B9
\/
{x})) by
A60,
A64,
A67,
A68,
A70;
end;
end;
A71:
X[(
{}. X)];
for B9 be
Element of (
Fin X) holds
X[B9] from
FinSubInd1(
A71,
A63);
hence thesis by
A53,
A57,
A62;
end;
end;
end
theorem ::
SETWISEO:16
Th13: for X,Y be non
empty
set holds for F be
BinOp of Y holds for B be
Element of (
Fin X) holds for f be
Function of X, Y st (B
<>
{} or F is
having_a_unity) & F is
idempotent & F is
commutative & F is
associative holds for IT be
Element of Y holds IT
= (F
$$ (B,f)) iff ex G be
Function of (
Fin X), Y st IT
= (G
. B) & (for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e) & (for x be
Element of X holds (G
.
{x})
= (f
. x)) & for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in B holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)))
proof
let X,Y be non
empty
set;
let F be
BinOp of Y;
let B be
Element of (
Fin X);
let f be
Function of X, Y;
assume that
A1: B
<>
{} or F is
having_a_unity and
A2: F is
idempotent and
A3: F is
commutative and
A4: F is
associative;
let IT be
Element of Y;
thus IT
= (F
$$ (B,f)) implies ex G be
Function of (
Fin X), Y st IT
= (G
. B) & (for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e) & (for x be
Element of X holds (G
.
{x})
= (f
. x)) & for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in B holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)))
proof
assume IT
= (F
$$ (B,f));
then
consider G be
Function of (
Fin X), Y such that
A5: IT
= (G
. B) & for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e and
A6: for x be
Element of X holds (G
.
{x})
= (f
. x) and
A7: for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in (B
\ B9) holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x))) by
A1,
A3,
A4,
Def3;
for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in B holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)))
proof
let B9 be
Element of (
Fin X) such that
A8: B9
c= B and
A9: B9
<>
{} ;
let x be
Element of X such that
A10: x
in B;
per cases ;
suppose x
in B9;
then
A11: (B9
\/
{x})
= B9 by
ZFMISC_1: 40;
then
A12:
{x}
c= B9 by
XBOOLE_1: 7;
not x
in (B9
\
{x}) by
ZFMISC_1: 56;
then
A13: x
in (B
\ (B9
\
{x})) by
A10,
XBOOLE_0:def 5;
per cases ;
suppose
A14: B9
=
{x};
hence (G
. (B9
\/
{x}))
= (F
. ((f
. x),(f
. x))) by
A2,
A6
.= (F
. ((G
. B9),(f
. x))) by
A6,
A14;
end;
suppose B9
<>
{x};
then not B9
c=
{x} by
A12,
XBOOLE_0:def 10;
then (B9
\
{x})
<>
{} by
XBOOLE_1: 37;
then
A15: (G
. ((B9
\
{.x.})
\/
{.x.}))
= (F
. ((G
. (B9
\
{.x.})),(f
. x))) by
A7,
A8,
A13,
XBOOLE_1: 1;
thus (G
. (B9
\/
{x}))
= (F
. ((G
. (B9
\
{x})),(F
. ((f
. x),(f
. x))))) by
A2,
A15,
XBOOLE_1: 39
.= (F
. ((F
. ((G
. (B9
\
{.x.})),(f
. x))),(f
. x))) by
A4
.= (F
. ((G
. B9),(f
. x))) by
A11,
A15,
XBOOLE_1: 39;
end;
end;
suppose not x
in B9;
then x
in (B
\ B9) by
A10,
XBOOLE_0:def 5;
hence thesis by
A7,
A8,
A9;
end;
end;
hence thesis by
A5,
A6;
end;
given G be
Function of (
Fin X), Y such that
A16: (IT
= (G
. B) & for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e) & for x be
Element of X holds (G
.
{x})
= (f
. x) and
A17: for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in B holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)));
for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in (B
\ B9) holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x)))
proof
let B9 be
Element of (
Fin X) such that
A18: B9
c= B & B9
<>
{} ;
let x be
Element of X;
assume x
in (B
\ B9);
then x
in B by
XBOOLE_0:def 5;
hence thesis by
A17,
A18;
end;
hence thesis by
A1,
A3,
A4,
A16,
Def3;
end;
reserve X,Y for non
empty
set,
F for
BinOp of Y,
B for
Element of (
Fin X),
f for
Function of X, Y;
theorem ::
SETWISEO:17
Th14: F is
commutative & F is
associative implies for b be
Element of X holds (F
$$ (
{.b.},f))
= (f
. b)
proof
assume
A1: F is
commutative & F is
associative;
let b be
Element of X;
ex G be
Function of (
Fin X), Y st (F
$$ (
{.b.},f))
= (G
.
{b}) & (for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e) & (for x be
Element of X holds (G
.
{x})
= (f
. x)) & for B9 be
Element of (
Fin X) st B9
c=
{b} & B9
<>
{} holds for x be
Element of X st x
in (
{b}
\ B9) holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x))) by
A1,
Def3;
hence thesis;
end;
theorem ::
SETWISEO:18
Th15: F is
idempotent & F is
commutative & F is
associative implies for a,b be
Element of X holds (F
$$ (
{.a, b.},f))
= (F
. ((f
. a),(f
. b)))
proof
assume
A1: F is
idempotent & F is
commutative & F is
associative;
let a,b be
Element of X;
consider G be
Function of (
Fin X), Y such that
A2: (F
$$ (
{.a, b.},f))
= (G
.
{a, b}) and for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e and
A3: for x be
Element of X holds (G
.
{x})
= (f
. x) and
A4: for B9 be
Element of (
Fin X) st B9
c=
{a, b} & B9
<>
{} holds for x be
Element of X st x
in
{a, b} holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x))) by
A1,
Th13;
A5: b
in
{a, b} by
TARSKI:def 2;
thus (F
$$ (
{.a, b.},f))
= (G
. (
{.a.}
\/
{.b.})) by
A2,
ENUMSET1: 1
.= (F
. ((G
.
{.a.}),(f
. b))) by
A4,
A5,
ZFMISC_1: 7
.= (F
. ((f
. a),(f
. b))) by
A3;
end;
theorem ::
SETWISEO:19
Th16: F is
idempotent & F is
commutative & F is
associative implies for a,b,c be
Element of X holds (F
$$ (
{.a, b, c.},f))
= (F
. ((F
. ((f
. a),(f
. b))),(f
. c)))
proof
assume
A1: F is
idempotent & F is
commutative & F is
associative;
let a,b,c be
Element of X;
consider G be
Function of (
Fin X), Y such that
A2: (F
$$ (
{.a, b, c.},f))
= (G
.
{a, b, c}) and for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e and
A3: for x be
Element of X holds (G
.
{x})
= (f
. x) and
A4: for B9 be
Element of (
Fin X) st B9
c=
{a, b, c} & B9
<>
{} holds for x be
Element of X st x
in
{a, b, c} holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x))) by
A1,
Th13;
A5: b
in
{a, b, c} by
ENUMSET1:def 1;
A6: (G
.
{a, b})
= (G
. (
{a}
\/
{b})) by
ENUMSET1: 1
.= (F
. ((G
.
{.a.}),(f
. b))) by
A4,
A5,
Th1
.= (F
. ((f
. a),(f
. b))) by
A3;
A7: c
in
{a, b, c} by
ENUMSET1:def 1;
thus (F
$$ (
{.a, b, c.},f))
= (G
. (
{.a, b.}
\/
{.c.})) by
A2,
ENUMSET1: 3
.= (F
. ((F
. ((f
. a),(f
. b))),(f
. c))) by
A4,
A6,
A7,
Th2;
end;
theorem ::
SETWISEO:20
Th17: F is
idempotent & F is
commutative & F is
associative & B
<>
{} implies for x be
Element of X holds (F
$$ ((B
\/
{.x.}),f))
= (F
. ((F
$$ (B,f)),(f
. x)))
proof
assume
A1: F is
idempotent & F is
commutative & F is
associative;
assume
A2: B
<>
{} ;
then
consider G9 be
Function of (
Fin X), Y such that
A3: (F
$$ (B,f))
= (G9
. B) and for e be
Element of Y st e
is_a_unity_wrt F holds (G9
.
{} )
= e and
A4: for x be
Element of X holds (G9
.
{x})
= (f
. x) and
A5: for B9 be
Element of (
Fin X) st B9
c= B & B9
<>
{} holds for x be
Element of X st x
in B holds (G9
. (B9
\/
{x}))
= (F
. ((G9
. B9),(f
. x))) by
A1,
Th13;
let x be
Element of X;
consider G be
Function of (
Fin X), Y such that
A6: (F
$$ ((B
\/
{.x.}),f))
= (G
. (B
\/
{.x.})) and for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e and
A7: for x be
Element of X holds (G
.
{x})
= (f
. x) and
A8: for B9 be
Element of (
Fin X) st B9
c= (B
\/
{x}) & B9
<>
{} holds for x9 be
Element of X st x9
in (B
\/
{x}) holds (G
. (B9
\/
{x9}))
= (F
. ((G
. B9),(f
. x9))) by
A1,
Th13;
defpred
X[
set] means $1
<>
{} & $1
c= B implies (G
. $1)
= (G9
. $1);
A9: for B9 be
Element of (
Fin X), b be
Element of X holds
X[B9] implies
X[(B9
\/
{b})]
proof
A10: B
c= (B
\/
{x}) by
XBOOLE_1: 7;
let C be
Element of (
Fin X), y be
Element of X such that
A11: C
<>
{} & C
c= B implies (G
. C)
= (G9
. C);
assume that (C
\/
{y})
<>
{} and
A12: (C
\/
{y})
c= B;
A13: C
c= B & y
in B by
A12,
ZFMISC_1: 137;
per cases ;
suppose
A14: C
=
{} ;
hence (G
. (C
\/
{y}))
= (f
. y) by
A7
.= (G9
. (C
\/
{y})) by
A4,
A14;
end;
suppose
A15: C
<>
{} ;
hence (G
. (C
\/
{y}))
= (F
. ((G9
. C),(f
. y))) by
A8,
A11,
A13,
A10,
XBOOLE_1: 1
.= (G9
. (C
\/
{y})) by
A5,
A13,
A15;
end;
end;
A16:
X[(
{}. X)];
A17: for C be
Element of (
Fin X) holds
X[C] from
FinSubInd3(
A16,
A9);
x
in (B
\/
{x}) by
ZFMISC_1: 136;
hence (F
$$ ((B
\/
{.x.}),f))
= (F
. ((G
. B),(f
. x))) by
A2,
A6,
A8,
XBOOLE_1: 7
.= (F
. ((F
$$ (B,f)),(f
. x))) by
A2,
A3,
A17;
end;
theorem ::
SETWISEO:21
Th18: F is
idempotent & F is
commutative & F is
associative implies for B1,B2 be
Element of (
Fin X) st B1
<>
{} & B2
<>
{} holds (F
$$ ((B1
\/ B2),f))
= (F
. ((F
$$ (B1,f)),(F
$$ (B2,f))))
proof
assume that
A1: F is
idempotent and
A2: F is
commutative and
A3: F is
associative;
let B1,B2 be
Element of (
Fin X);
defpred
X[
Element of (
Fin X)] means $1
<>
{} implies (F
$$ ((B1
\/ $1),f))
= (F
. ((F
$$ (B1,f)),(F
$$ ($1,f))));
assume
A4: B1
<>
{} ;
A5: for B9 be
Element of (
Fin X), b be
Element of X holds
X[B9] implies
X[(B9
\/
{.b.})]
proof
let B be
Element of (
Fin X), x be
Element of X such that
A6: B
<>
{} implies (F
$$ ((B1
\/ B),f))
= (F
. ((F
$$ (B1,f)),(F
$$ (B,f)))) and (B
\/
{x})
<>
{} ;
per cases ;
suppose
A7: B
=
{} ;
hence (F
$$ ((B1
\/ (B
\/
{.x.})),f))
= (F
. ((F
$$ (B1,f)),(f
. x))) by
A1,
A2,
A3,
A4,
Th17
.= (F
. ((F
$$ (B1,f)),(F
$$ ((B
\/
{.x.}),f)))) by
A2,
A3,
A7,
Th14;
end;
suppose
A8: B
<>
{} ;
thus (F
$$ ((B1
\/ (B
\/
{.x.})),f))
= (F
$$ (((B1
\/ B)
\/
{.x.}),f)) by
XBOOLE_1: 4
.= (F
. ((F
. ((F
$$ (B1,f)),(F
$$ (B,f)))),(f
. x))) by
A1,
A2,
A3,
A6,
A8,
Th17
.= (F
. ((F
$$ (B1,f)),(F
. ((F
$$ (B,f)),(f
. x))))) by
A3
.= (F
. ((F
$$ (B1,f)),(F
$$ ((B
\/
{.x.}),f)))) by
A1,
A2,
A3,
A8,
Th17;
end;
end;
A9:
X[(
{}. X)];
for B2 be
Element of (
Fin X) holds
X[B2] from
FinSubInd3(
A9,
A5);
hence thesis;
end;
theorem ::
SETWISEO:22
F is
commutative & F is
associative & F is
idempotent implies for x be
Element of X st x
in B holds (F
. ((f
. x),(F
$$ (B,f))))
= (F
$$ (B,f))
proof
assume that
A1: F is
commutative & F is
associative and
A2: F is
idempotent;
let x be
Element of X;
assume
A3: x
in B;
thus (F
. ((f
. x),(F
$$ (B,f))))
= (F
. ((F
$$ (
{.x.},f)),(F
$$ (B,f)))) by
A1,
Th14
.= (F
$$ ((
{.x.}
\/ B),f)) by
A1,
A2,
A3,
Th18
.= (F
$$ (B,f)) by
A3,
ZFMISC_1: 40;
end;
theorem ::
SETWISEO:23
F is
commutative & F is
associative & F is
idempotent implies for B,C be
Element of (
Fin X) st B
<>
{} & B
c= C holds (F
. ((F
$$ (B,f)),(F
$$ (C,f))))
= (F
$$ (C,f))
proof
assume
A1: F is
commutative & F is
associative & F is
idempotent;
let B,C be
Element of (
Fin X) such that
A2: B
<>
{} and
A3: B
c= C;
C
<>
{} by
A2,
A3;
hence (F
. ((F
$$ (B,f)),(F
$$ (C,f))))
= (F
$$ ((B
\/ C),f)) by
A1,
A2,
Th18
.= (F
$$ (C,f)) by
A3,
XBOOLE_1: 12;
end;
theorem ::
SETWISEO:24
Th21: B
<>
{} & F is
commutative & F is
associative & F is
idempotent implies for a be
Element of Y st for b be
Element of X st b
in B holds (f
. b)
= a holds (F
$$ (B,f))
= a
proof
assume that
A1: B
<>
{} and
A2: F is
commutative & F is
associative and
A3: F is
idempotent;
let a be
Element of Y;
defpred
X[
Element of (
Fin X)] means (for b be
Element of X st b
in $1 holds (f
. b)
= a) implies (F
$$ ($1,f))
= a;
A4: for B1,B2 be non
empty
Element of (
Fin X) holds
X[B1] &
X[B2] implies
X[(B1
\/ B2)]
proof
let B1,B2 be non
empty
Element of (
Fin X);
assume that
A5: ((for b be
Element of X st b
in B1 holds (f
. b)
= a) implies (F
$$ (B1,f))
= a) & ((for b be
Element of X st b
in B2 holds (f
. b)
= a) implies (F
$$ (B2,f))
= a) and
A6: for b be
Element of X st b
in (B1
\/ B2) holds (f
. b)
= a;
A7:
now
let b be
Element of X;
assume b
in B2;
then b
in (B1
\/ B2) by
XBOOLE_0:def 3;
hence (f
. b)
= a by
A6;
end;
now
let b be
Element of X;
assume b
in B1;
then b
in (B1
\/ B2) by
XBOOLE_0:def 3;
hence (f
. b)
= a by
A6;
end;
hence (F
$$ ((B1
\/ B2),f))
= (F
. (a,a)) by
A2,
A3,
A5,
A7,
Th18
.= a by
A3;
end;
A8: for x be
Element of X holds
X[
{.x.}]
proof
let x be
Element of X such that
A9: for b be
Element of X st b
in
{x} holds (f
. b)
= a;
A10: x
in
{x} by
TARSKI:def 1;
thus (F
$$ (
{.x.},f))
= (f
. x) by
A2,
Th14
.= a by
A9,
A10;
end;
for B be non
empty
Element of (
Fin X) holds
X[B] from
FinSubInd2(
A8,
A4);
hence thesis by
A1;
end;
theorem ::
SETWISEO:25
Th22: F is
commutative & F is
associative & F is
idempotent implies for a be
Element of Y st (f
.: B)
=
{a} holds (F
$$ (B,f))
= a
proof
assume
A1: F is
commutative & F is
associative & F is
idempotent;
let a be
Element of Y;
assume
A2: (f
.: B)
=
{a};
A3: for b be
Element of X st b
in B holds (f
. b)
= a
proof
let b be
Element of X;
assume b
in B;
then (f
. b)
in
{a} by
A2,
FUNCT_2: 35;
hence thesis by
TARSKI:def 1;
end;
B
<>
{} by
A2;
hence thesis by
A1,
A3,
Th21;
end;
theorem ::
SETWISEO:26
Th23: F is
commutative & F is
associative & F is
idempotent implies for f,g be
Function of X, Y holds for A,B be
Element of (
Fin X) st A
<>
{} & (f
.: A)
= (g
.: B) holds (F
$$ (A,f))
= (F
$$ (B,g))
proof
assume that
A1: F is
commutative and
A2: F is
associative and
A3: F is
idempotent;
let f,g be
Function of X, Y;
defpred
X[
Element of (
Fin X)] means $1
<>
{} implies for B be
Element of (
Fin X) st (f
.: $1)
= (g
.: B) holds (F
$$ ($1,f))
= (F
$$ (B,g));
A4: for B9 be
Element of (
Fin X), b be
Element of X holds
X[B9] implies
X[(B9
\/
{.b.})]
proof
let A be
Element of (
Fin X), x be
Element of X such that
A5: A
<>
{} implies for B be
Element of (
Fin X) st (f
.: A)
= (g
.: B) holds (F
$$ (A,f))
= (F
$$ (B,g));
assume (A
\/
{x})
<>
{} ;
let B be
Element of (
Fin X) such that
A6: (f
.: (A
\/
{x}))
= (g
.: B);
per cases ;
suppose (f
. x)
in (f
.: A);
then
consider x9 be
Element of X such that
A7: x9
in A and
A8: (f
. x9)
= (f
. x) by
FUNCT_2: 65;
A9: (g
.: B)
= ((f
.: A)
\/ (
Im (f,x))) by
A6,
RELAT_1: 120
.= ((f
.: A)
\/
{(f
. x)}) by
Th5
.= (f
.: A) by
A7,
A8,
FUNCT_2: 35,
ZFMISC_1: 40;
thus (F
$$ ((A
\/
{.x.}),f))
= (F
. ((F
$$ (A,f)),(f
. x))) by
A1,
A2,
A3,
A7,
Th17
.= (F
. ((F
$$ ((A
\/
{.x9.}),f)),(f
. x))) by
A7,
ZFMISC_1: 40
.= (F
. ((F
. ((F
$$ (A,f)),(f
. x9))),(f
. x))) by
A1,
A2,
A3,
A7,
Th17
.= (F
. ((F
$$ (A,f)),(F
. ((f
. x9),(f
. x9))))) by
A2,
A8
.= (F
$$ ((A
\/
{.x9.}),f)) by
A1,
A2,
A3,
A7,
Th17
.= (F
$$ (A,f)) by
A7,
ZFMISC_1: 40
.= (F
$$ (B,g)) by
A5,
A7,
A9;
end;
suppose
A10: not (f
. x)
in (f
.: A);
per cases ;
suppose
A11: A
=
{} ;
then
A12: (g
.: B)
= (
Im (f,x)) by
A6
.=
{(f
. x)} by
Th5;
thus (F
$$ ((A
\/
{.x.}),f))
= (f
. x) by
A1,
A2,
A11,
Th14
.= (F
$$ (B,g)) by
A1,
A2,
A3,
A12,
Th22;
end;
suppose
A13: A
<>
{} ;
reconsider B1 = (B
\ (g
"
{(f
. x)})) as
Element of (
Fin X) by
Th8;
A14:
now
assume B1
=
{} ;
then
A15: (g
.: B)
c= (g
.: (g
"
{(f
. x)})) by
RELAT_1: 123,
XBOOLE_1: 37;
(g
.: (g
"
{(f
. x)}))
c=
{(f
. x)} by
FUNCT_1: 75;
then (f
.: (A
\/
{x}))
c=
{(f
. x)} by
A6,
A15;
then ((f
.: A)
\/ (f
.:
{x}))
c=
{(f
. x)} by
RELAT_1: 120;
then (f
.: A)
= ((f
.: A)
/\
{(f
. x)}) by
XBOOLE_1: 11,
XBOOLE_1: 28
.=
{} by
A10,
XBOOLE_0:def 7,
ZFMISC_1: 50;
hence contradiction by
A13,
Th10;
end;
reconsider B2 = (B
/\ (g
"
{(f
. x)})) as
Element of (
Fin X) by
Th8,
XBOOLE_1: 17;
A16: B
= (B1
\/ B2) by
XBOOLE_1: 51;
A17: for b be
Element of X st b
in B2 holds (g
. b)
= (f
. x)
proof
let b be
Element of X;
assume b
in B2;
then b
in (g
"
{(f
. x)}) by
XBOOLE_0:def 4;
then (g
. b)
in
{(f
. x)} by
FUNCT_1:def 7;
hence thesis by
TARSKI:def 1;
end;
A18: (f
.: A)
= ((f
.: A)
\
{(f
. x)}) by
A10,
ZFMISC_1: 57
.= ((f
.: A)
\ (
Im (f,x))) by
Th5
.= (((f
.: A)
\/ (f
.:
{x}))
\ (f
.:
{x})) by
XBOOLE_1: 40
.= ((f
.: (A
\/
{x}))
\ (
Im (f,x))) by
RELAT_1: 120
.= ((g
.: B)
\
{(f
. x)}) by
A6,
Th5
.= (g
.: B1) by
Th3;
x
in (A
\/
{x}) by
ZFMISC_1: 136;
then
consider x9 be
Element of X such that
A19: x9
in B and
A20: (g
. x9)
= (f
. x) by
A6,
FUNCT_2: 35,
FUNCT_2: 65;
x9
in (g
"
{(f
. x)}) by
A20,
Th4;
then
A21: B2
<>
{} by
A19,
XBOOLE_0:def 4;
thus (F
$$ ((A
\/
{.x.}),f))
= (F
. ((F
$$ (A,f)),(f
. x))) by
A1,
A2,
A3,
A13,
Th17
.= (F
. ((F
$$ (B1,g)),(f
. x))) by
A5,
A13,
A18
.= (F
. ((F
$$ (B1,g)),(F
$$ (B2,g)))) by
A1,
A2,
A3,
A21,
A17,
Th21
.= (F
$$ (B,g)) by
A1,
A2,
A3,
A16,
A14,
A21,
Th18;
end;
end;
end;
A22:
X[(
{}. X)];
A23: for A be
Element of (
Fin X) holds
X[A] from
FinSubInd3(
A22,
A4);
let A,B be
Element of (
Fin X);
assume A
<>
{} & (f
.: A)
= (g
.: B);
hence thesis by
A23;
end;
theorem ::
SETWISEO:27
for F,G be
BinOp of Y st F is
idempotent & F is
commutative & F is
associative & G
is_distributive_wrt F holds for B be
Element of (
Fin X) st B
<>
{} holds for f be
Function of X, Y holds for a be
Element of Y holds (G
. (a,(F
$$ (B,f))))
= (F
$$ (B,(G
[;] (a,f))))
proof
let F,G be
BinOp of Y such that
A1: F is
idempotent and
A2: F is
commutative & F is
associative and
A3: G
is_distributive_wrt F;
let B be
Element of (
Fin X) such that
A4: B
<>
{} ;
let f be
Function of X, Y;
let a be
Element of Y;
defpred
X[
Element of (
Fin X)] means (G
. (a,(F
$$ ($1,f))))
= (F
$$ ($1,(G
[;] (a,f))));
A5: for B1,B2 be non
empty
Element of (
Fin X) holds
X[B1] &
X[B2] implies
X[(B1
\/ B2)]
proof
let B1,B2 be non
empty
Element of (
Fin X);
assume
A6: (G
. (a,(F
$$ (B1,f))))
= (F
$$ (B1,(G
[;] (a,f)))) & (G
. (a,(F
$$ (B2,f))))
= (F
$$ (B2,(G
[;] (a,f))));
thus (G
. (a,(F
$$ ((B1
\/ B2),f))))
= (G
. (a,(F
. ((F
$$ (B1,f)),(F
$$ (B2,f)))))) by
A1,
A2,
Th18
.= (F
. ((F
$$ (B1,(G
[;] (a,f)))),(F
$$ (B2,(G
[;] (a,f)))))) by
A3,
A6,
BINOP_1: 11
.= (F
$$ ((B1
\/ B2),(G
[;] (a,f)))) by
A1,
A2,
Th18;
end;
A7: for x be
Element of X holds
X[
{.x.}]
proof
let x be
Element of X;
thus (G
. (a,(F
$$ (
{.x.},f))))
= (G
. (a,(f
. x))) by
A2,
Th14
.= ((G
[;] (a,f))
. x) by
FUNCOP_1: 53
.= (F
$$ (
{.x.},(G
[;] (a,f)))) by
A2,
Th14;
end;
for B be non
empty
Element of (
Fin X) holds
X[B] from
FinSubInd2(
A7,
A5);
hence thesis by
A4;
end;
theorem ::
SETWISEO:28
for F,G be
BinOp of Y st F is
idempotent & F is
commutative & F is
associative & G
is_distributive_wrt F holds for B be
Element of (
Fin X) st B
<>
{} holds for f be
Function of X, Y holds for a be
Element of Y holds (G
. ((F
$$ (B,f)),a))
= (F
$$ (B,(G
[:] (f,a))))
proof
let F,G be
BinOp of Y such that
A1: F is
idempotent and
A2: F is
commutative & F is
associative and
A3: G
is_distributive_wrt F;
let B be
Element of (
Fin X) such that
A4: B
<>
{} ;
let f be
Function of X, Y;
let a be
Element of Y;
defpred
X[
Element of (
Fin X)] means (G
. ((F
$$ ($1,f)),a))
= (F
$$ ($1,(G
[:] (f,a))));
A5: for B1,B2 be non
empty
Element of (
Fin X) holds
X[B1] &
X[B2] implies
X[(B1
\/ B2)]
proof
let B1,B2 be non
empty
Element of (
Fin X);
assume
A6: (G
. ((F
$$ (B1,f)),a))
= (F
$$ (B1,(G
[:] (f,a)))) & (G
. ((F
$$ (B2,f)),a))
= (F
$$ (B2,(G
[:] (f,a))));
thus (G
. ((F
$$ ((B1
\/ B2),f)),a))
= (G
. ((F
. ((F
$$ (B1,f)),(F
$$ (B2,f)))),a)) by
A1,
A2,
Th18
.= (F
. ((F
$$ (B1,(G
[:] (f,a)))),(F
$$ (B2,(G
[:] (f,a)))))) by
A3,
A6,
BINOP_1: 11
.= (F
$$ ((B1
\/ B2),(G
[:] (f,a)))) by
A1,
A2,
Th18;
end;
A7: for x be
Element of X holds
X[
{.x.}]
proof
let x be
Element of X;
thus (G
. ((F
$$ (
{.x.},f)),a))
= (G
. ((f
. x),a)) by
A2,
Th14
.= ((G
[:] (f,a))
. x) by
FUNCOP_1: 48
.= (F
$$ (
{.x.},(G
[:] (f,a)))) by
A2,
Th14;
end;
for B be non
empty
Element of (
Fin X) holds
X[B] from
FinSubInd2(
A7,
A5);
hence thesis by
A4;
end;
definition
let X,Y be non
empty
set;
let f be
Function of X, Y;
let A be
Element of (
Fin X);
:: original:
.:
redefine
func f
.: A ->
Element of (
Fin Y) ;
coherence by
Lm1;
end
theorem ::
SETWISEO:29
Th26: for A,X,Y be non
empty
set holds for F be
BinOp of A st F is
idempotent & F is
commutative & F is
associative holds for B be
Element of (
Fin X) st B
<>
{} holds for f be
Function of X, Y holds for g be
Function of Y, A holds (F
$$ ((f
.: B),g))
= (F
$$ (B,(g
* f)))
proof
let A,X,Y be non
empty
set, F be
BinOp of A such that
A1: F is
idempotent and
A2: F is
commutative & F is
associative;
let B be
Element of (
Fin X) such that
A3: B
<>
{} ;
let f be
Function of X, Y;
let g be
Function of Y, A;
defpred
X[
Element of (
Fin X)] means (F
$$ ((f
.: $1),g))
= (F
$$ ($1,(g
* f)));
A4: (
dom f)
= X by
FUNCT_2:def 1;
A5: for B1,B2 be non
empty
Element of (
Fin X) holds
X[B1] &
X[B2] implies
X[(B1
\/ B2)]
proof
let B1,B2 be non
empty
Element of (
Fin X);
assume
A6: (F
$$ ((f
.: B1),g))
= (F
$$ (B1,(g
* f))) & (F
$$ ((f
.: B2),g))
= (F
$$ (B2,(g
* f)));
A7: B1
c= X by
FINSUB_1:def 5;
A8: B2
c= X by
FINSUB_1:def 5;
thus (F
$$ ((f
.: (B1
\/ B2)),g))
= (F
$$ (((f
.: B1)
\/ (f
.: B2)),g)) by
RELAT_1: 120
.= (F
. ((F
$$ ((f
.: B1),g)),(F
$$ ((f
.: B2),g)))) by
A1,
A2,
A7,
A8,
Th18,
A4
.= (F
$$ ((B1
\/ B2),(g
* f))) by
A1,
A2,
A6,
Th18;
end;
A9: for x be
Element of X holds
X[
{.x.}]
proof
let x be
Element of X;
(f
.:
{.x.})
= (
Im (f,x));
hence (F
$$ ((f
.:
{.x.}),g))
= (F
$$ (
{.(f
. x).},g)) by
A4,
FUNCT_1: 59
.= (g
. (f
. x)) by
A2,
Th14
.= ((g
* f)
. x) by
FUNCT_2: 15
.= (F
$$ (
{.x.},(g
* f))) by
A2,
Th14;
end;
for B be non
empty
Element of (
Fin X) holds
X[B] from
FinSubInd2(
A9,
A5);
hence thesis by
A3;
end;
theorem ::
SETWISEO:30
Th27: F is
commutative & F is
associative & F is
idempotent implies for Z be non
empty
set holds for G be
BinOp of Z st G is
commutative & G is
associative & G is
idempotent holds for f be
Function of X, Y holds for g be
Function of Y, Z st for x,y be
Element of Y holds (g
. (F
. (x,y)))
= (G
. ((g
. x),(g
. y))) holds for B be
Element of (
Fin X) st B
<>
{} holds (g
. (F
$$ (B,f)))
= (G
$$ (B,(g
* f)))
proof
assume that
A1: F is
commutative & F is
associative and
A2: F is
idempotent;
let Z be non
empty
set, G be
BinOp of Z such that
A3: G is
commutative & G is
associative and
A4: G is
idempotent;
let f be
Function of X, Y;
let g be
Function of Y, Z such that
A5: for x,y be
Element of Y holds (g
. (F
. (x,y)))
= (G
. ((g
. x),(g
. y)));
defpred
X[
Element of (
Fin X)] means $1
<>
{} implies (g
. (F
$$ ($1,f)))
= (G
$$ ($1,(g
* f)));
A6: for B9 be
Element of (
Fin X), b be
Element of X holds
X[B9] implies
X[(B9
\/
{.b.})]
proof
let B be
Element of (
Fin X), x be
Element of X;
assume that
A7: B
<>
{} implies (g
. (F
$$ (B,f)))
= (G
$$ (B,(g
* f))) and (B
\/
{x})
<>
{} ;
per cases ;
suppose
A8: B
=
{} ;
hence (g
. (F
$$ ((B
\/
{.x.}),f)))
= (g
. (f
. x)) by
A1,
Th14
.= ((g
* f)
. x) by
FUNCT_2: 15
.= (G
$$ ((B
\/
{.x.}),(g
* f))) by
A3,
A8,
Th14;
end;
suppose
A9: B
<>
{} ;
hence (g
. (F
$$ ((B
\/
{.x.}),f)))
= (g
. (F
. ((F
$$ (B,f)),(f
. x)))) by
A1,
A2,
Th17
.= (G
. ((g
. (F
$$ (B,f))),(g
. (f
. x)))) by
A5
.= (G
. ((G
$$ (B,(g
* f))),((g
* f)
. x))) by
A7,
A9,
FUNCT_2: 15
.= (G
$$ ((B
\/
{.x.}),(g
* f))) by
A3,
A4,
A9,
Th17;
end;
end;
A10:
X[(
{}. X)];
thus for B be
Element of (
Fin X) holds
X[B] from
FinSubInd3(
A10,
A6);
end;
theorem ::
SETWISEO:31
Th28: F is
commutative & F is
associative & F is
having_a_unity implies for f holds (F
$$ ((
{}. X),f))
= (
the_unity_wrt F)
proof
assume
A1: F is
commutative & F is
associative & F is
having_a_unity;
let f;
(
the_unity_wrt F)
is_a_unity_wrt F & ex G be
Function of (
Fin X), Y st (F
$$ ((
{}. X),f))
= (G
. (
{}. X)) & (for e be
Element of Y st e
is_a_unity_wrt F holds (G
.
{} )
= e) & (for x be
Element of X holds (G
.
{x})
= (f
. x)) & for B9 be
Element of (
Fin X) st B9
c= (
{}. X) & B9
<>
{} holds for x be
Element of X st x
in ((
{}. X)
\ B9) holds (G
. (B9
\/
{x}))
= (F
. ((G
. B9),(f
. x))) by
A1,
Def3,
Th11;
hence thesis;
end;
theorem ::
SETWISEO:32
Th29: F is
idempotent & F is
commutative & F is
associative & F is
having_a_unity implies for x be
Element of X holds (F
$$ ((B
\/
{.x.}),f))
= (F
. ((F
$$ (B,f)),(f
. x)))
proof
assume that
A1: F is
idempotent and
A2: F is
commutative & F is
associative;
assume
A3: F is
having_a_unity;
let x be
Element of X;
A4:
{}
= (
{}. X);
now
assume
A5: B
=
{} ;
hence (F
$$ ((B
\/
{.x.}),f))
= (f
. x) by
A2,
Th14
.= (F
. ((
the_unity_wrt F),(f
. x))) by
A3,
Th12
.= (F
. ((F
$$ (B,f)),(f
. x))) by
A2,
A3,
A4,
A5,
Th28;
end;
hence thesis by
A1,
A2,
Th17;
end;
theorem ::
SETWISEO:33
F is
idempotent & F is
commutative & F is
associative & F is
having_a_unity implies for B1,B2 be
Element of (
Fin X) holds (F
$$ ((B1
\/ B2),f))
= (F
. ((F
$$ (B1,f)),(F
$$ (B2,f))))
proof
assume that
A1: F is
idempotent and
A2: F is
commutative & F is
associative and
A3: F is
having_a_unity;
let B1,B2 be
Element of (
Fin X);
now
A4:
{}
= (
{}. X);
assume
A5: B1
=
{} or B2
=
{} ;
per cases by
A5;
suppose
A6: B2
=
{} ;
hence (F
$$ ((B1
\/ B2),f))
= (F
. ((F
$$ (B1,f)),(
the_unity_wrt F))) by
A3,
Th12
.= (F
. ((F
$$ (B1,f)),(F
$$ (B2,f)))) by
A2,
A3,
A4,
A6,
Th28;
end;
suppose
A7: B1
=
{} ;
hence (F
$$ ((B1
\/ B2),f))
= (F
. ((
the_unity_wrt F),(F
$$ (B2,f)))) by
A3,
Th12
.= (F
. ((F
$$ (B1,f)),(F
$$ (B2,f)))) by
A2,
A3,
A4,
A7,
Th28;
end;
end;
hence thesis by
A1,
A2,
Th18;
end;
theorem ::
SETWISEO:34
F is
commutative & F is
associative & F is
idempotent & F is
having_a_unity implies for f,g be
Function of X, Y holds for A,B be
Element of (
Fin X) st (f
.: A)
= (g
.: B) holds (F
$$ (A,f))
= (F
$$ (B,g))
proof
assume that
A1: F is
commutative & F is
associative and
A2: F is
idempotent and
A3: F is
having_a_unity;
let f,g be
Function of X, Y;
let A,B be
Element of (
Fin X) such that
A4: (f
.: A)
= (g
.: B);
now
assume
A5: A
=
{} ;
then A
= (
{}. X);
then
A6: (F
$$ (A,f))
= (
the_unity_wrt F) by
A1,
A3,
Th28;
(f
.: A)
=
{} by
A5;
then B
= (
{}. X) by
A4,
Th10;
hence thesis by
A1,
A3,
A6,
Th28;
end;
hence thesis by
A1,
A2,
A4,
Th23;
end;
theorem ::
SETWISEO:35
Th32: for A,X,Y be non
empty
set holds for F be
BinOp of A st F is
idempotent & F is
commutative & F is
associative & F is
having_a_unity holds for B be
Element of (
Fin X) holds for f be
Function of X, Y holds for g be
Function of Y, A holds (F
$$ ((f
.: B),g))
= (F
$$ (B,(g
* f)))
proof
let A,X,Y be non
empty
set, F be
BinOp of A such that
A1: F is
idempotent and
A2: F is
commutative & F is
associative and
A3: F is
having_a_unity;
let B be
Element of (
Fin X);
let f be
Function of X, Y;
let g be
Function of Y, A;
now
assume
A4: B
=
{} ;
then (f
.: B)
= (
{}. Y);
then
A5: (F
$$ ((f
.: B),g))
= (
the_unity_wrt F) by
A2,
A3,
Th28;
B
= (
{}. X) by
A4;
hence thesis by
A2,
A3,
A5,
Th28;
end;
hence thesis by
A1,
A2,
Th26;
end;
theorem ::
SETWISEO:36
F is
commutative & F is
associative & F is
idempotent & F is
having_a_unity implies for Z be non
empty
set holds for G be
BinOp of Z st G is
commutative & G is
associative & G is
idempotent & G is
having_a_unity holds for f be
Function of X, Y holds for g be
Function of Y, Z st (g
. (
the_unity_wrt F))
= (
the_unity_wrt G) & for x,y be
Element of Y holds (g
. (F
. (x,y)))
= (G
. ((g
. x),(g
. y))) holds for B be
Element of (
Fin X) holds (g
. (F
$$ (B,f)))
= (G
$$ (B,(g
* f)))
proof
assume that
A1: F is
commutative & F is
associative and
A2: F is
idempotent and
A3: F is
having_a_unity;
let Z be non
empty
set;
let G be
BinOp of Z such that
A4: G is
commutative & G is
associative and
A5: G is
idempotent and
A6: G is
having_a_unity;
let f be
Function of X, Y;
let g be
Function of Y, Z such that
A7: (g
. (
the_unity_wrt F))
= (
the_unity_wrt G) and
A8: for x,y be
Element of Y holds (g
. (F
. (x,y)))
= (G
. ((g
. x),(g
. y)));
let B be
Element of (
Fin X);
per cases ;
suppose B
=
{} ;
then
A9: B
= (
{}. X);
hence (g
. (F
$$ (B,f)))
= (g
. (
the_unity_wrt F)) by
A1,
A3,
Th28
.= (G
$$ (B,(g
* f))) by
A4,
A6,
A7,
A9,
Th28;
end;
suppose B
<>
{} ;
hence thesis by
A1,
A2,
A4,
A5,
A8,
Th27;
end;
end;
definition
let A be
set;
::
SETWISEO:def4
func
FinUnion A ->
BinOp of (
Fin A) means
:
Def4: for x,y be
Element of (
Fin A) holds (it
. (x,y))
= (x
\/ y);
existence
proof
deffunc
U(
Element of (
Fin A),
Element of (
Fin A)) = ($1
\/ $2);
ex IT be
BinOp of (
Fin A) st for x,y be
Element of (
Fin A) holds (IT
. (x,y))
=
U(x,y) from
BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let IT,IT9 be
BinOp of (
Fin A) such that
A1: for x,y be
Element of (
Fin A) holds (IT
. (x,y))
= (x
\/ y) and
A2: for x,y be
Element of (
Fin A) holds (IT9
. (x,y))
= (x
\/ y);
now
let x,y be
Element of (
Fin A);
thus (IT
. (x,y))
= (x
\/ y) by
A1
.= (IT9
. (x,y)) by
A2;
end;
hence IT
= IT9;
end;
end
reserve A for
set,
x,y,z for
Element of (
Fin A);
theorem ::
SETWISEO:37
Th34: (
FinUnion A) is
idempotent
proof
let x;
thus ((
FinUnion A)
. (x,x))
= (x
\/ x) by
Def4
.= x;
end;
theorem ::
SETWISEO:38
Th35: (
FinUnion A) is
commutative
proof
let x, y;
thus ((
FinUnion A)
. (x,y))
= (y
\/ x) by
Def4
.= ((
FinUnion A)
. (y,x)) by
Def4;
end;
theorem ::
SETWISEO:39
Th36: (
FinUnion A) is
associative
proof
let x, y, z;
thus ((
FinUnion A)
. (((
FinUnion A)
. (x,y)),z))
= ((
FinUnion A)
. ((x
\/ y),z)) by
Def4
.= ((x
\/ y)
\/ z) by
Def4
.= (x
\/ (y
\/ z)) by
XBOOLE_1: 4
.= ((
FinUnion A)
. (x,(y
\/ z))) by
Def4
.= ((
FinUnion A)
. (x,((
FinUnion A)
. (y,z)))) by
Def4;
end;
theorem ::
SETWISEO:40
Th37: (
{}. A)
is_a_unity_wrt (
FinUnion A)
proof
thus for x holds ((
FinUnion A)
. ((
{}. A),x))
= x
proof
let x;
thus ((
FinUnion A)
. ((
{}. A),x))
= (
{}
\/ x) by
Def4
.= x;
end;
let x;
thus ((
FinUnion A)
. (x,(
{}. A)))
= (x
\/
{} ) by
Def4
.= x;
end;
theorem ::
SETWISEO:41
Th38: (
FinUnion A) is
having_a_unity
proof
(
{}. A)
is_a_unity_wrt (
FinUnion A) by
Th37;
hence thesis;
end;
theorem ::
SETWISEO:42
(
the_unity_wrt (
FinUnion A))
is_a_unity_wrt (
FinUnion A) by
Th11,
Th38;
theorem ::
SETWISEO:43
Th40: (
the_unity_wrt (
FinUnion A))
=
{}
proof
(
{}. A)
is_a_unity_wrt (
FinUnion A) by
Th37;
hence thesis by
BINOP_1:def 8;
end;
reserve X,Y for non
empty
set,
A for
set,
f for
Function of X, (
Fin A),
i,j,k for
Element of X;
definition
let X be non
empty
set, A be
set;
let B be
Element of (
Fin X);
let f be
Function of X, (
Fin A);
::
SETWISEO:def5
func
FinUnion (B,f) ->
Element of (
Fin A) equals ((
FinUnion A)
$$ (B,f));
coherence ;
end
theorem ::
SETWISEO:44
(
FinUnion (
{.i.},f))
= (f
. i)
proof
(
FinUnion A) is
commutative by
Th35;
hence thesis by
Th14,
Th36;
end;
theorem ::
SETWISEO:45
(
FinUnion (
{.i, j.},f))
= ((f
. i)
\/ (f
. j))
proof
(
FinUnion A) is
idempotent & (
FinUnion A) is
commutative by
Th34,
Th35;
hence (
FinUnion (
{.i, j.},f))
= ((
FinUnion A)
. ((f
. i),(f
. j))) by
Th15,
Th36
.= ((f
. i)
\/ (f
. j)) by
Def4;
end;
theorem ::
SETWISEO:46
(
FinUnion (
{.i, j, k.},f))
= (((f
. i)
\/ (f
. j))
\/ (f
. k))
proof
(
FinUnion A) is
idempotent & (
FinUnion A) is
commutative by
Th34,
Th35;
hence (
FinUnion (
{.i, j, k.},f))
= ((
FinUnion A)
. (((
FinUnion A)
. ((f
. i),(f
. j))),(f
. k))) by
Th16,
Th36
.= ((
FinUnion A)
. (((f
. i)
\/ (f
. j)),(f
. k))) by
Def4
.= (((f
. i)
\/ (f
. j))
\/ (f
. k)) by
Def4;
end;
theorem ::
SETWISEO:47
Th44: (
FinUnion ((
{}. X),f))
=
{}
proof
(
FinUnion A) is
commutative & (
FinUnion A) is
associative by
Th35,
Th36;
hence (
FinUnion ((
{}. X),f))
= (
the_unity_wrt (
FinUnion A)) by
Th28,
Th38
.=
{} by
Th40;
end;
theorem ::
SETWISEO:48
Th45: for B be
Element of (
Fin X) holds (
FinUnion ((B
\/
{.i.}),f))
= ((
FinUnion (B,f))
\/ (f
. i))
proof
let B be
Element of (
Fin X);
A1: (
FinUnion A) is
associative by
Th36;
(
FinUnion A) is
idempotent & (
FinUnion A) is
commutative by
Th34,
Th35;
hence (
FinUnion ((B
\/
{.i.}),f))
= ((
FinUnion A)
. ((
FinUnion (B,f)),(f
. i))) by
A1,
Th29,
Th38
.= ((
FinUnion (B,f))
\/ (f
. i)) by
Def4;
end;
theorem ::
SETWISEO:49
Th46: for B be
Element of (
Fin X) holds (
FinUnion (B,f))
= (
union (f
.: B))
proof
defpred
X[
Element of (
Fin X)] means (
FinUnion ($1,f))
= (
union (f
.: $1));
A1: for B be
Element of (
Fin X), i st
X[B] holds
X[(B
\/
{.i.})]
proof
let B be
Element of (
Fin X), i;
assume (
FinUnion (B,f))
= (
union (f
.: B));
hence (
FinUnion ((B
\/
{.i.}),f))
= ((
union (f
.: B))
\/ (
union
{(f
. i)})) by
Th45
.= (
union ((f
.: B)
\/
{(f
. i)})) by
ZFMISC_1: 78
.= (
union ((f
.: B)
\/ (
Im (f,i)))) by
Th5
.= (
union (f
.: (B
\/
{i}))) by
RELAT_1: 120;
end;
(
FinUnion ((
{}. X),f))
= (
union (f
.: (
{}. X))) by
Th44,
ZFMISC_1: 2;
then
A2:
X[(
{}. X)];
thus for B be
Element of (
Fin X) holds
X[B] from
FinSubInd3(
A2,
A1);
end;
theorem ::
SETWISEO:50
for B1,B2 be
Element of (
Fin X) holds (
FinUnion ((B1
\/ B2),f))
= ((
FinUnion (B1,f))
\/ (
FinUnion (B2,f)))
proof
let B1,B2 be
Element of (
Fin X);
thus (
FinUnion ((B1
\/ B2),f))
= (
union (f
.: (B1
\/ B2))) by
Th46
.= (
union ((f
.: B1)
\/ (f
.: B2))) by
RELAT_1: 120
.= ((
union (f
.: B1))
\/ (
union (f
.: B2))) by
ZFMISC_1: 78
.= ((
FinUnion (B1,f))
\/ (
union (f
.: B2))) by
Th46
.= ((
FinUnion (B1,f))
\/ (
FinUnion (B2,f))) by
Th46;
end;
theorem ::
SETWISEO:51
for B be
Element of (
Fin X) holds for f be
Function of X, Y holds for g be
Function of Y, (
Fin A) holds (
FinUnion ((f
.: B),g))
= (
FinUnion (B,(g
* f)))
proof
let B be
Element of (
Fin X);
let f be
Function of X, Y;
let g be
Function of Y, (
Fin A);
thus (
FinUnion ((f
.: B),g))
= (
union (g
.: (f
.: B))) by
Th46
.= (
union ((g
* f)
.: B)) by
RELAT_1: 126
.= (
FinUnion (B,(g
* f))) by
Th46;
end;
theorem ::
SETWISEO:52
Th49: for A,X be non
empty
set, Y be
set holds for G be
BinOp of A st G is
commutative & G is
associative & G is
idempotent holds for B be
Element of (
Fin X) st B
<>
{} holds for f be
Function of X, (
Fin Y), g be
Function of (
Fin Y), A st for x,y be
Element of (
Fin Y) holds (g
. (x
\/ y))
= (G
. ((g
. x),(g
. y))) holds (g
. (
FinUnion (B,f)))
= (G
$$ (B,(g
* f)))
proof
let A,X be non
empty
set, Y be
set, G be
BinOp of A such that
A1: G is
commutative & G is
associative & G is
idempotent;
let B be
Element of (
Fin X) such that
A2: B
<>
{} ;
let f be
Function of X, (
Fin Y), g be
Function of (
Fin Y), A such that
A3: for x,y be
Element of (
Fin Y) holds (g
. (x
\/ y))
= (G
. ((g
. x),(g
. y)));
A4:
now
let x,y be
Element of (
Fin Y);
thus (g
. ((
FinUnion Y)
. (x,y)))
= (g
. (x
\/ y)) by
Def4
.= (G
. ((g
. x),(g
. y))) by
A3;
end;
A5: (
FinUnion Y) is
idempotent by
Th34;
(
FinUnion Y) is
commutative & (
FinUnion Y) is
associative by
Th35,
Th36;
hence thesis by
A1,
A5,
A2,
A4,
Th27;
end;
theorem ::
SETWISEO:53
Th50: for Z be non
empty
set, Y be
set holds for G be
BinOp of Z st G is
commutative & G is
associative & G is
idempotent & G is
having_a_unity holds for f be
Function of X, (
Fin Y) holds for g be
Function of (
Fin Y), Z st (g
. (
{}. Y))
= (
the_unity_wrt G) & for x,y be
Element of (
Fin Y) holds (g
. (x
\/ y))
= (G
. ((g
. x),(g
. y))) holds for B be
Element of (
Fin X) holds (g
. (
FinUnion (B,f)))
= (G
$$ (B,(g
* f)))
proof
let Z be non
empty
set, Y be
set;
let G be
BinOp of Z such that
A1: G is
commutative & G is
associative and
A2: G is
idempotent and
A3: G is
having_a_unity;
let f be
Function of X, (
Fin Y);
let g be
Function of (
Fin Y), Z such that
A4: (g
. (
{}. Y))
= (
the_unity_wrt G) and
A5: for x,y be
Element of (
Fin Y) holds (g
. (x
\/ y))
= (G
. ((g
. x),(g
. y)));
let B be
Element of (
Fin X);
A6:
{}
= (
{}. X);
A7:
{}
= (
{}. (
Fin Y));
per cases ;
suppose
A8: B
=
{} ;
then
A9: (f
.: B)
=
{} ;
thus (g
. (
FinUnion (B,f)))
= (g
. (
{}. Y)) by
A6,
A8,
Th44
.= (G
$$ ((f
.: B),g)) by
A1,
A3,
A4,
A7,
A9,
Th28
.= (G
$$ (B,(g
* f))) by
A1,
A2,
A3,
Th32;
end;
suppose B
<>
{} ;
hence thesis by
A1,
A2,
A5,
Th49;
end;
end;
definition
let A be
set;
::
SETWISEO:def6
func
singleton A ->
Function of A, (
Fin A) means
:
Def6: for x be
object st x
in A holds (it
. x)
=
{x};
existence
proof
deffunc
U(
object) =
{$1};
A1:
now
let x be
object;
assume
A2: x
in A;
then
reconsider A9 = A as non
empty
set;
reconsider x9 = x as
Element of A9 by
A2;
{.x9.}
in (
Fin A9);
hence
U(x)
in (
Fin A);
end;
thus ex f be
Function of A, (
Fin A) st for x be
object st x
in A holds (f
. x)
=
U(x) from
FUNCT_2:sch 2(
A1);
end;
uniqueness
proof
let IT,IT9 be
Function of A, (
Fin A) such that
A3: for x be
object st x
in A holds (IT
. x)
=
{x} and
A4: for x be
object st x
in A holds (IT9
. x)
=
{x};
now
let x be
object;
assume
A5: x
in A;
then (IT
. x)
=
{x} by
A3;
hence (IT
. x)
= (IT9
. x) by
A4,
A5;
end;
hence thesis by
FUNCT_2: 12;
end;
end
theorem ::
SETWISEO:54
Th51: for A be non
empty
set holds for f be
Function of A, (
Fin A) holds f
= (
singleton A) iff for x be
Element of A holds (f
. x)
=
{x}
proof
let A be non
empty
set;
let f be
Function of A, (
Fin A);
thus f
= (
singleton A) implies for x be
Element of A holds (f
. x)
=
{x} by
Def6;
assume for x be
Element of A holds (f
. x)
=
{x};
then for x be
object holds x
in A implies (f
. x)
=
{x};
hence thesis by
Def6;
end;
theorem ::
SETWISEO:55
Th52: for x be
set, y be
Element of X holds x
in ((
singleton X)
. y) iff x
= y
proof
let x be
set, y be
Element of X;
((
singleton X)
. y)
=
{y} by
Th51;
hence thesis by
TARSKI:def 1;
end;
theorem ::
SETWISEO:56
for x,y,z be
Element of X st x
in ((
singleton X)
. z) & y
in ((
singleton X)
. z) holds x
= y
proof
let x,y,z be
Element of X;
assume that
A1: x
in ((
singleton X)
. z) and
A2: y
in ((
singleton X)
. z);
x
= z by
A1,
Th52;
hence thesis by
A2,
Th52;
end;
Lm2: for D be non
empty
set, X,P be
set holds for f be
Function of X, D holds (f
.: P)
c= D;
theorem ::
SETWISEO:57
Th54: for B be
Element of (
Fin X), x be
set holds x
in (
FinUnion (B,f)) iff ex i be
Element of X st i
in B & x
in (f
. i)
proof
let B be
Element of (
Fin X), x be
set;
A1:
now
assume x
in (
union (f
.: B));
then
consider Z be
set such that
A2: x
in Z and
A3: Z
in (f
.: B) by
TARSKI:def 4;
(f
.: B) is
Subset of (
Fin A) by
Lm2;
then
reconsider Z as
Element of (
Fin A) by
A3;
consider i be
Element of X such that
A4: i
in B & Z
= (f
. i) by
A3,
FUNCT_2: 65;
take i9 = i;
thus i9
in B & x
in (f
. i9) by
A2,
A4;
end;
now
given i be
Element of X such that
A5: i
in B and
A6: x
in (f
. i);
(f
. i)
in (f
.: B) by
A5,
FUNCT_2: 35;
hence x
in (
union (f
.: B)) by
A6,
TARSKI:def 4;
end;
hence thesis by
A1,
Th46;
end;
theorem ::
SETWISEO:58
for B be
Element of (
Fin X) holds (
FinUnion (B,(
singleton X)))
= B
proof
let B be
Element of (
Fin X);
now
let x be
object;
thus x
in (
FinUnion (B,(
singleton X))) implies x
in B
proof
assume x
in (
FinUnion (B,(
singleton X)));
then ex i be
Element of X st i
in B & x
in ((
singleton X)
. i) by
Th54;
hence thesis by
Th52;
end;
assume
A1: x
in B;
then
reconsider x9 = x as
Element of X by
Th6;
x
in ((
singleton X)
. x9) by
Th52;
hence x
in (
FinUnion (B,(
singleton X))) by
A1,
Th54;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
SETWISEO:59
for Y,Z be
set holds for f be
Function of X, (
Fin Y) holds for g be
Function of (
Fin Y), (
Fin Z) st (g
. (
{}. Y))
= (
{}. Z) & for x,y be
Element of (
Fin Y) holds (g
. (x
\/ y))
= ((g
. x)
\/ (g
. y)) holds for B be
Element of (
Fin X) holds (g
. (
FinUnion (B,f)))
= (
FinUnion (B,(g
* f)))
proof
let Y,Z be
set;
let f be
Function of X, (
Fin Y);
let g be
Function of (
Fin Y), (
Fin Z);
assume that
A1: (g
. (
{}. Y))
= (
{}. Z) and
A2: for x,y be
Element of (
Fin Y) holds (g
. (x
\/ y))
= ((g
. x)
\/ (g
. y));
A3: (g
. (
{}. Y))
= (
the_unity_wrt (
FinUnion Z)) by
A1,
Th40;
A4:
now
let x,y be
Element of (
Fin Y);
thus (g
. (x
\/ y))
= ((g
. x)
\/ (g
. y)) by
A2
.= ((
FinUnion Z)
. ((g
. x),(g
. y))) by
Def4;
end;
let B be
Element of (
Fin X);
A5: (
FinUnion Z) is
idempotent by
Th34;
(
FinUnion Z) is
associative & (
FinUnion Z) is
commutative by
Th35,
Th36;
hence thesis by
A5,
A3,
A4,
Th38,
Th50;
end;