funct_1.miz
begin
reserve X,X1,X2,Y,Y1,Y2 for
set,
p,x,x1,x2,y,y1,y2,z,z1,z2 for
object;
definition
let X be
set;
::
FUNCT_1:def1
attr X is
Function-like means
:
Def1: for x, y1, y2 st
[x, y1]
in X &
[x, y2]
in X holds y1
= y2;
end
registration
cluster
empty ->
Function-like for
set;
coherence ;
end
registration
cluster
Function-like for
Relation;
existence
proof
take
{} ;
thus thesis;
end;
end
definition
mode
Function is
Function-like
Relation;
end
registration
let a,b be
object;
cluster
{
[a, b]} ->
Function-like;
coherence
proof
set X =
{
[a, b]};
A1:
[:
{a},
{b}:]
= X by
ZFMISC_1: 29;
for x,y1,y2 be
object st
[x, y1]
in X &
[x, y2]
in X holds y1
= y2
proof
let x,y1,y2 be
object such that
A2:
[x, y1]
in X and
A3:
[x, y2]
in X;
y1
= b by
A1,
A2,
ZFMISC_1: 28;
hence thesis by
A1,
A3,
ZFMISC_1: 28;
end;
hence thesis;
end;
end
reserve f,g,g1,g2,h for
Function,
R,S for
Relation;
scheme ::
FUNCT_1:sch1
GraphFunc { A() ->
set , P[
object,
object] } :
ex f st for x,y be
object holds
[x, y]
in f iff x
in A() & P[x, y]
provided
A1: for x,y1,y2 be
object st P[x, y1] & P[x, y2] holds y1
= y2;
consider Y such that
A2: for y be
object holds y
in Y iff ex x be
object st x
in A() & P[x, y] from
TARSKI:sch 1(
A1);
defpred
R[
object] means ex x, y st
[x, y]
= $1 & P[x, y];
consider F be
set such that
A3: for p be
object holds p
in F iff p
in
[:A(), Y:] &
R[p] from
XBOOLE_0:sch 1;
now
thus for p be
object holds p
in F implies ex x,y be
object st
[x, y]
= p
proof
let p be
object;
p
in F implies ex x, y st
[x, y]
= p & P[x, y] by
A3;
hence thesis;
end;
let x, y1, y2;
assume
[x, y1]
in F;
then
consider x1, z1 such that
A4:
[x1, z1]
=
[x, y1] and
A5: P[x1, z1] by
A3;
A6: x
= x1 & z1
= y1 by
A4,
XTUPLE_0: 1;
assume
[x, y2]
in F;
then
consider x2, z2 such that
A7:
[x2, z2]
=
[x, y2] and
A8: P[x2, z2] by
A3;
x
= x2 & z2
= y2 by
A7,
XTUPLE_0: 1;
hence y1
= y2 by
A1,
A5,
A8,
A6;
end;
then
reconsider f = F as
Function by
Def1,
RELAT_1:def 1;
take f;
let x,y be
object;
thus
[x, y]
in f implies x
in A() & P[x, y]
proof
assume
A9:
[x, y]
in f;
then
consider x1, y1 such that
A10:
[x1, y1]
=
[x, y] and
A11: P[x1, y1] by
A3;
[x, y]
in
[:A(), Y:] by
A3,
A9;
hence x
in A() by
ZFMISC_1: 87;
x1
= x by
A10,
XTUPLE_0: 1;
hence thesis by
A10,
A11,
XTUPLE_0: 1;
end;
assume that
A12: x
in A() and
A13: P[x, y];
y
in Y by
A2,
A12,
A13;
then
[x, y]
in
[:A(), Y:] by
A12,
ZFMISC_1: 87;
hence thesis by
A3,
A13;
end;
definition
let f;
let x be
object;
::
FUNCT_1:def2
func f
. x ->
set means
:
Def2:
[x, it ]
in f if x
in (
dom f)
otherwise it
=
{} ;
existence
proof
hereby
assume x
in (
dom f);
then
consider y be
object such that
A1:
[x, y]
in f by
XTUPLE_0:def 12;
reconsider y as
set by
TARSKI: 1;
take y;
thus
[x, y]
in f by
A1;
end;
thus thesis;
end;
uniqueness by
Def1;
consistency ;
end
theorem ::
FUNCT_1:1
Th1:
[x, y]
in f iff x
in (
dom f) & y
= (f
. x)
proof
thus
[x, y]
in f implies x
in (
dom f) & y
= (f
. x)
proof
assume
A1:
[x, y]
in f;
hence
A2: x
in (
dom f) by
XTUPLE_0:def 12;
reconsider y as
set by
TARSKI: 1;
y
= (f
. x) by
A1,
Def2,
A2;
hence thesis;
end;
thus thesis by
Def2;
end;
theorem ::
FUNCT_1:2
Th2: (
dom f)
= (
dom g) & (for x st x
in (
dom f) holds (f
. x)
= (g
. x)) implies f
= g
proof
assume that
A1: (
dom f)
= (
dom g) and
A2: for x st x
in (
dom f) holds (f
. x)
= (g
. x);
let x,y be
object;
thus
[x, y]
in f implies
[x, y]
in g
proof
assume
A3:
[x, y]
in f;
then
A4: x
in (
dom f) by
XTUPLE_0:def 12;
reconsider y as
set by
TARSKI: 1;
(f
. x)
= y by
A3,
Def2,
A4;
then (g
. x)
= y by
A2,
A4;
hence thesis by
A1,
A4,
Def2;
end;
assume
A5:
[x, y]
in g;
then
A6: x
in (
dom g) by
XTUPLE_0:def 12;
reconsider y as
set by
TARSKI: 1;
(g
. x)
= y by
A5,
Def2,
A6;
then (f
. x)
= y by
A1,
A2,
A6;
hence thesis by
A1,
A6,
Def2;
end;
definition
let f;
:: original:
rng
redefine
::
FUNCT_1:def3
func
rng f means
:
Def3: for y be
object holds y
in it iff ex x be
object st x
in (
dom f) & y
= (f
. x);
compatibility
proof
let Y;
hereby
assume
A1: Y
= (
rng f);
let y be
object;
hereby
assume y
in Y;
then
consider x be
object such that
A2:
[x, y]
in f by
A1,
XTUPLE_0:def 13;
take x;
thus x
in (
dom f) & y
= (f
. x) by
A2,
Th1;
end;
given x be
object such that
A3: x
in (
dom f) & y
= (f
. x);
[x, y]
in f by
A3,
Def2;
hence y
in Y by
A1,
XTUPLE_0:def 13;
end;
assume
A4: for y be
object holds y
in Y iff ex x be
object st x
in (
dom f) & y
= (f
. x);
hereby
let y be
object;
assume y
in Y;
then
consider x be
object such that
A5: x
in (
dom f) & y
= (f
. x) by
A4;
[x, y]
in f by
A5,
Def2;
hence y
in (
rng f) by
XTUPLE_0:def 13;
end;
let y be
object;
assume y
in (
rng f);
then
consider x be
object such that
A6:
[x, y]
in f by
XTUPLE_0:def 13;
x
in (
dom f) & y
= (f
. x) by
A6,
Th1;
hence thesis by
A4;
end;
end
theorem ::
FUNCT_1:3
x
in (
dom f) implies (f
. x)
in (
rng f) by
Def3;
theorem ::
FUNCT_1:4
Th4: (
dom f)
=
{x} implies (
rng f)
=
{(f
. x)}
proof
assume
A1: (
dom f)
=
{x};
for y be
object holds y
in (
rng f) iff y
in
{(f
. x)}
proof
let y be
object;
thus y
in (
rng f) implies y
in
{(f
. x)}
proof
assume y
in (
rng f);
then
consider z be
object such that
A2: z
in (
dom f) and
A3: y
= (f
. z) by
Def3;
z
= x by
A1,
A2,
TARSKI:def 1;
hence thesis by
A3,
TARSKI:def 1;
end;
assume y
in
{(f
. x)};
then
A4: y
= (f
. x) by
TARSKI:def 1;
x
in (
dom f) by
A1,
TARSKI:def 1;
hence thesis by
A4,
Def3;
end;
hence thesis by
TARSKI: 2;
end;
scheme ::
FUNCT_1:sch2
FuncEx { A() ->
set , P[
object,
object] } :
ex f st (
dom f)
= A() & for x st x
in A() holds P[x, (f
. x)]
provided
A1: for x, y1, y2 st x
in A() & P[x, y1] & P[x, y2] holds y1
= y2
and
A2: for x st x
in A() holds ex y st P[x, y];
defpred
R[
object,
object] means $1
in A() & P[$1, $2];
A3: for x,y1,y2 be
object st
R[x, y1] &
R[x, y2] holds y1
= y2 by
A1;
consider f be
Function such that
A4: for x,y be
object holds
[x, y]
in f iff x
in A() &
R[x, y] from
GraphFunc(
A3);
take f;
for x be
object holds x
in (
dom f) iff x
in A()
proof
let x be
object;
thus x
in (
dom f) implies x
in A()
proof
assume x
in (
dom f);
then ex y be
object st
[x, y]
in f by
XTUPLE_0:def 12;
hence thesis by
A4;
end;
assume
A5: x
in A();
then
consider y such that
A6: P[x, y] by
A2;
[x, y]
in f by
A4,
A5,
A6;
hence thesis by
XTUPLE_0:def 12;
end;
hence
A7: (
dom f)
= A() by
TARSKI: 2;
let x;
assume
A8: x
in A();
then
consider y such that
A9: P[x, y] by
A2;
reconsider y as
set by
TARSKI: 1;
[x, y]
in f by
A4,
A8,
A9;
hence thesis by
A7,
A8,
A9,
Def2;
end;
scheme ::
FUNCT_1:sch3
Lambda { A() ->
set , F(
object) ->
object } :
ex f be
Function st (
dom f)
= A() & for x st x
in A() holds (f
. x)
= F(x);
defpred
P[
object,
object] means $2
= F($1);
A1: for x st x
in A() holds ex y st
P[x, y];
A2: for x, y1, y2 st x
in A() &
P[x, y1] &
P[x, y2] holds y1
= y2;
thus ex f be
Function st (
dom f)
= A() & for x st x
in A() holds
P[x, (f
. x)] from
FuncEx(
A2,
A1);
end;
theorem ::
FUNCT_1:5
Th5: X
<>
{} implies for y holds ex f st (
dom f)
= X & (
rng f)
=
{y}
proof
assume
A1: X
<>
{} ;
let y;
deffunc
F(
object) = y;
consider f such that
A2: (
dom f)
= X and
A3: for x st x
in X holds (f
. x)
=
F(x) from
Lambda;
take f;
thus (
dom f)
= X by
A2;
for y1 be
object holds y1
in (
rng f) iff y1
= y
proof
let y1 be
object;
A4:
now
set x = the
Element of X;
assume
A5: y1
= y;
(f
. x)
= y by
A1,
A3;
hence y1
in (
rng f) by
A1,
A2,
A5,
Def3;
end;
now
assume y1
in (
rng f);
then ex x be
object st x
in (
dom f) & y1
= (f
. x) by
Def3;
hence y1
= y by
A2,
A3;
end;
hence thesis by
A4;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
FUNCT_1:6
(for f, g st (
dom f)
= X & (
dom g)
= X holds f
= g) implies X
=
{}
proof
deffunc
F(
object) =
{} ;
assume
A1: for f, g st (
dom f)
= X & (
dom g)
= X holds f
= g;
set x = the
Element of X;
consider f be
Function such that
A2: (
dom f)
= X and
A3: for x st x
in X holds (f
. x)
=
F(x) from
Lambda;
assume
A4: not thesis;
then
A5: (f
. x)
=
{} by
A3;
deffunc
F(
object) =
{
{} };
consider g be
Function such that
A6: (
dom g)
= X and
A7: for x st x
in X holds (g
. x)
=
F(x) from
Lambda;
(g
. x)
=
{
{} } by
A4,
A7;
hence contradiction by
A1,
A2,
A6,
A5;
end;
theorem ::
FUNCT_1:7
(
dom f)
= (
dom g) & (
rng f)
=
{y} & (
rng g)
=
{y} implies f
= g
proof
assume that
A1: (
dom f)
= (
dom g) and
A2: (
rng f)
=
{y} and
A3: (
rng g)
=
{y};
x
in (
dom f) implies (f
. x)
= (g
. x)
proof
assume
A4: x
in (
dom f);
then (f
. x)
in (
rng f) by
Def3;
then
A5: (f
. x)
= y by
A2,
TARSKI:def 1;
(g
. x)
in (
rng g) by
A1,
A4,
Def3;
hence thesis by
A3,
A5,
TARSKI:def 1;
end;
hence thesis by
A1,
Th2;
end;
theorem ::
FUNCT_1:8
Y
<>
{} or X
=
{} implies ex f st X
= (
dom f) & (
rng f)
c= Y
proof
assume
A1: Y
<>
{} or X
=
{} ;
A2:
now
set y = the
Element of Y;
deffunc
F(
object) = y;
consider f such that
A3: (
dom f)
= X and
A4: for x st x
in X holds (f
. x)
=
F(x) from
Lambda;
assume X
<>
{} ;
then
A5: y
in Y by
A1;
take f;
thus (
dom f)
= X by
A3;
for z be
object holds z
in (
rng f) implies z
in Y
proof
let z be
object;
assume z
in (
rng f);
then ex x be
object st x
in (
dom f) & z
= (f
. x) by
Def3;
hence thesis by
A5,
A3,
A4;
end;
hence (
rng f)
c= Y;
end;
now
assume
A6: X
=
{} ;
take f =
{} ;
thus (
dom f)
= X by
A6;
thus (
rng f)
c= Y;
end;
hence thesis by
A2;
end;
theorem ::
FUNCT_1:9
(for y st y
in Y holds ex x st x
in (
dom f) & y
= (f
. x)) implies Y
c= (
rng f)
proof
assume
A1: for y st y
in Y holds ex x st x
in (
dom f) & y
= (f
. x);
let y be
object;
assume y
in Y;
then ex x st x
in (
dom f) & y
= (f
. x) by
A1;
hence thesis by
Def3;
end;
notation
let f, g;
synonym g
* f for f
* g;
end
registration
let f, g;
cluster (g
* f) ->
Function-like;
coherence
proof
let x, y1, y2;
assume
[x, y1]
in (g
* f);
then
consider z1 be
object such that
A1:
[x, z1]
in f and
A2:
[z1, y1]
in g by
RELAT_1:def 8;
assume
[x, y2]
in (g
* f);
then
consider z2 be
object such that
A3:
[x, z2]
in f and
A4:
[z2, y2]
in g by
RELAT_1:def 8;
z1
= z2 by
A1,
A3,
Def1;
hence thesis by
A2,
A4,
Def1;
end;
end
theorem ::
FUNCT_1:10
for h st (for x holds x
in (
dom h) iff x
in (
dom f) & (f
. x)
in (
dom g)) & (for x st x
in (
dom h) holds (h
. x)
= (g
. (f
. x))) holds h
= (g
* f)
proof
let h;
assume that
A1: for x holds x
in (
dom h) iff x
in (
dom f) & (f
. x)
in (
dom g) and
A2: for x st x
in (
dom h) holds (h
. x)
= (g
. (f
. x));
now
let x,y be
object;
hereby
assume
A3:
[x, y]
in h;
then
A4: x
in (
dom h) by
XTUPLE_0:def 12;
then
A5: (f
. x)
in (
dom g) by
A1;
reconsider y1 = (f
. x) as
object;
take y1;
x
in (
dom f) by
A1,
A4;
hence
[x, y1]
in f by
Def2;
reconsider yy = y as
set by
TARSKI: 1;
yy
= (h
. x) by
A3,
A4,
Def2
.= (g
. (f
. x)) by
A2,
A4;
hence
[y1, y]
in g by
A5,
Def2;
end;
given z be
object such that
A6:
[x, z]
in f and
A7:
[z, y]
in g;
A8: x
in (
dom f) by
A6,
XTUPLE_0:def 12;
reconsider z as
set by
TARSKI: 1;
A9: z
= (f
. x) by
A6,
Def2,
A8;
A10: z
in (
dom g) by
A7,
XTUPLE_0:def 12;
then
A11: x
in (
dom h) by
A1,
A8,
A9;
reconsider yy = y as
set by
TARSKI: 1;
yy
= (g
. z) by
A7,
A10,
Def2;
then y
= (h
. x) by
A2,
A9,
A11;
hence
[x, y]
in h by
A11,
Def2;
end;
hence thesis by
RELAT_1:def 8;
end;
theorem ::
FUNCT_1:11
Th11: x
in (
dom (g
* f)) iff x
in (
dom f) & (f
. x)
in (
dom g)
proof
set h = (g
* f);
hereby
assume x
in (
dom h);
then
consider y be
object such that
A1:
[x, y]
in h by
XTUPLE_0:def 12;
consider z be
object such that
A2:
[x, z]
in f and
A3:
[z, y]
in g by
A1,
RELAT_1:def 8;
reconsider z as
set by
TARSKI: 1;
thus x
in (
dom f) by
A2,
XTUPLE_0:def 12;
then z
= (f
. x) by
A2,
Def2;
hence (f
. x)
in (
dom g) by
A3,
XTUPLE_0:def 12;
end;
assume
A4: x
in (
dom f);
then
consider z be
object such that
A5:
[x, z]
in f by
XTUPLE_0:def 12;
assume (f
. x)
in (
dom g);
then
consider y be
object such that
A6:
[(f
. x), y]
in g by
XTUPLE_0:def 12;
reconsider z as
set by
TARSKI: 1;
z
= (f
. x) by
A4,
A5,
Def2;
then
[x, y]
in h by
A5,
A6,
RELAT_1:def 8;
hence thesis by
XTUPLE_0:def 12;
end;
theorem ::
FUNCT_1:12
Th12: x
in (
dom (g
* f)) implies ((g
* f)
. x)
= (g
. (f
. x))
proof
set h = (g
* f);
assume
A1: x
in (
dom h);
then
consider y be
object such that
A2:
[x, y]
in h by
XTUPLE_0:def 12;
consider z be
object such that
A3:
[x, z]
in f and
A4:
[z, y]
in g by
A2,
RELAT_1:def 8;
reconsider z, y as
set by
TARSKI: 1;
x
in (
dom f) by
A3,
XTUPLE_0:def 12;
then
A5: z
= (f
. x) by
A3,
Def2;
then (f
. x)
in (
dom g) by
A4,
XTUPLE_0:def 12;
then y
= (g
. (f
. x)) by
A4,
A5,
Def2;
hence thesis by
A1,
A2,
Def2;
end;
theorem ::
FUNCT_1:13
Th13: x
in (
dom f) implies ((g
* f)
. x)
= (g
. (f
. x))
proof
assume
A1: x
in (
dom f);
per cases ;
suppose (f
. x)
in (
dom g);
then x
in (
dom (g
* f)) by
A1,
Th11;
hence thesis by
Th12;
end;
suppose
A2: not (f
. x)
in (
dom g);
then not x
in (
dom (g
* f)) by
Th11;
hence ((g
* f)
. x)
=
{} by
Def2
.= (g
. (f
. x)) by
A2,
Def2;
end;
end;
theorem ::
FUNCT_1:14
z
in (
rng (g
* f)) implies z
in (
rng g)
proof
assume z
in (
rng (g
* f));
then
consider x be
object such that
A1: x
in (
dom (g
* f)) and
A2: z
= ((g
* f)
. x) by
Def3;
(f
. x)
in (
dom g) & ((g
* f)
. x)
= (g
. (f
. x)) by
A1,
Th11,
Th12;
hence thesis by
A2,
Def3;
end;
theorem ::
FUNCT_1:15
Th15: (
dom (g
* f))
= (
dom f) implies (
rng f)
c= (
dom g)
proof
assume
A1: (
dom (g
* f))
= (
dom f);
let y be
object;
assume y
in (
rng f);
then ex x be
object st x
in (
dom f) & y
= (f
. x) by
Def3;
hence thesis by
A1,
Th11;
end;
theorem ::
FUNCT_1:16
(
rng f)
c= Y & (for g, h st (
dom g)
= Y & (
dom h)
= Y & (g
* f)
= (h
* f) holds g
= h) implies Y
= (
rng f)
proof
assume that
A1: (
rng f)
c= Y and
A2: for g, h st (
dom g)
= Y & (
dom h)
= Y & (g
* f)
= (h
* f) holds g
= h;
Y
c= (
rng f)
proof
deffunc
F(
object) =
{} ;
let y be
object;
assume that
A3: y
in Y and
A4: not y
in (
rng f);
defpred
P[
object,
object] means ($1
= y implies $2
=
{
{} }) & ($1
<> y implies $2
=
{} );
A5: x
in Y implies ex y1 st
P[x, y1]
proof
assume x
in Y;
x
= y implies thesis;
hence thesis;
end;
A6: for x, y1, y2 st x
in Y &
P[x, y1] &
P[x, y2] holds y1
= y2;
consider h be
Function such that
A7: (
dom h)
= Y and
A8: for x st x
in Y holds
P[x, (h
. x)] from
FuncEx(
A6,
A5);
A9: (
dom (h
* f))
= (
dom f) by
A1,
A7,
RELAT_1: 27;
consider g be
Function such that
A10: (
dom g)
= Y and
A11: x
in Y implies (g
. x)
=
F(x) from
Lambda;
A12: (
dom (g
* f))
= (
dom f) by
A1,
A10,
RELAT_1: 27;
x
in (
dom f) implies ((g
* f)
. x)
= ((h
* f)
. x)
proof
assume
A13: x
in (
dom f);
then (f
. x)
in (
rng f) by
Def3;
then
A14: (g
. (f
. x))
=
{} & (h
. (f
. x))
=
{} by
A1,
A4,
A11,
A8;
((g
* f)
. x)
= (g
. (f
. x)) by
A12,
A13,
Th12;
hence thesis by
A9,
A13,
A14,
Th12;
end;
then
A15: g
= h by
A2,
A10,
A7,
A12,
A9,
Th2;
(g
. y)
=
{} by
A3,
A11;
hence contradiction by
A3,
A8,
A15;
end;
hence thesis by
A1;
end;
registration
let X;
cluster (
id X) ->
Function-like;
coherence
proof
let x, y1, y2;
assume that
A1:
[x, y1]
in (
id X) and
A2:
[x, y2]
in (
id X);
x
= y1 by
A1,
RELAT_1:def 10;
hence thesis by
A2,
RELAT_1:def 10;
end;
end
theorem ::
FUNCT_1:17
Th17: f
= (
id X) iff (
dom f)
= X & for x st x
in X holds (f
. x)
= x
proof
hereby
assume
A1: f
= (
id X);
hence
A2: (
dom f)
= X;
let x;
assume
A3: x
in X;
then
[x, x]
in f by
A1,
RELAT_1:def 10;
hence (f
. x)
= x by
A2,
A3,
Def2;
end;
assume that
A4: (
dom f)
= X and
A5: for x st x
in X holds (f
. x)
= x;
now
let x,y be
object;
hereby
assume
A6:
[x, y]
in f;
hence
A7: x
in X by
A4,
Th1;
y
= (f
. x) by
A6,
Th1;
hence x
= y by
A5,
A7;
end;
assume
A8: x
in X;
then (f
. x)
= x by
A5;
hence x
= y implies
[x, y]
in f by
A4,
A8,
Th1;
end;
hence thesis by
RELAT_1:def 10;
end;
theorem ::
FUNCT_1:18
Th18: x
in X implies ((
id X)
. x)
= x by
Th17;
theorem ::
FUNCT_1:19
Th19: (
dom (f
* (
id X)))
= ((
dom f)
/\ X)
proof
for x be
object holds x
in (
dom (f
* (
id X))) iff x
in ((
dom f)
/\ X)
proof
let x be
object;
x
in (
dom (f
* (
id X))) iff x
in (
dom f) & x
in X
proof
thus x
in (
dom (f
* (
id X))) implies x
in (
dom f) & x
in X
proof
assume x
in (
dom (f
* (
id X)));
then
A1: x
in (
dom (
id X)) & ((
id X)
. x)
in (
dom f) by
Th11;
thus thesis by
A1,
Th17;
end;
assume
A2: x
in (
dom f);
A3: (
dom (
id X))
= X;
assume
A4: x
in X;
then ((
id X)
. x)
in (
dom f) by
A2,
Th17;
hence thesis by
A4,
A3,
Th11;
end;
hence thesis by
XBOOLE_0:def 4;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
FUNCT_1:20
x
in ((
dom f)
/\ X) implies (f
. x)
= ((f
* (
id X))
. x)
proof
assume x
in ((
dom f)
/\ X);
then x
in X by
XBOOLE_0:def 4;
then ((
id X)
. x)
= x & x
in (
dom (
id X)) by
Th17;
hence thesis by
Th13;
end;
theorem ::
FUNCT_1:21
x
in (
dom ((
id Y)
* f)) iff x
in (
dom f) & (f
. x)
in Y
proof
(
dom (
id Y))
= Y;
hence thesis by
Th11;
end;
theorem ::
FUNCT_1:22
((
id X)
* (
id Y))
= (
id (X
/\ Y))
proof
A1: (
dom ((
id X)
* (
id Y)))
= ((
dom (
id X))
/\ Y) by
Th19
.= (X
/\ Y);
A2: z
in (X
/\ Y) implies (((
id X)
* (
id Y))
. z)
= ((
id (X
/\ Y))
. z)
proof
assume
A3: z
in (X
/\ Y);
then
A4: z
in X by
XBOOLE_0:def 4;
A5: z
in Y by
A3,
XBOOLE_0:def 4;
thus (((
id X)
* (
id Y))
. z)
= ((
id X)
. ((
id Y)
. z)) by
A1,
A3,
Th12
.= ((
id X)
. z) by
A5,
Th17
.= z by
A4,
Th17
.= ((
id (X
/\ Y))
. z) by
A3,
Th17;
end;
(X
/\ Y)
= (
dom (
id (X
/\ Y)));
hence thesis by
A1,
A2,
Th2;
end;
theorem ::
FUNCT_1:23
Th23: (
rng f)
= (
dom g) & (g
* f)
= f implies g
= (
id (
dom g))
proof
assume that
A1: (
rng f)
= (
dom g) and
A2: (g
* f)
= f;
set X = (
dom g);
x
in X implies (g
. x)
= x
proof
assume x
in X;
then ex y be
object st y
in (
dom f) & (f
. y)
= x by
A1,
Def3;
hence thesis by
A2,
Th13;
end;
hence thesis by
Th17;
end;
definition
let f;
::
FUNCT_1:def4
attr f is
one-to-one means
:
Def4: for x1, x2 st x1
in (
dom f) & x2
in (
dom f) & (f
. x1)
= (f
. x2) holds x1
= x2;
end
theorem ::
FUNCT_1:24
Th24: f is
one-to-one & g is
one-to-one implies (g
* f) is
one-to-one
proof
assume that
A1: f is
one-to-one and
A2: g is
one-to-one;
now
let x1, x2;
assume
A3: x1
in (
dom (g
* f)) & x2
in (
dom (g
* f));
then
A4: ((g
* f)
. x1)
= (g
. (f
. x1)) & ((g
* f)
. x2)
= (g
. (f
. x2)) by
Th12;
A5: x1
in (
dom f) & x2
in (
dom f) by
A3,
Th11;
assume
A6: ((g
* f)
. x1)
= ((g
* f)
. x2);
(f
. x1)
in (
dom g) & (f
. x2)
in (
dom g) by
A3,
Th11;
then (f
. x1)
= (f
. x2) by
A2,
A4,
A6;
hence x1
= x2 by
A1,
A5;
end;
hence thesis;
end;
theorem ::
FUNCT_1:25
Th25: (g
* f) is
one-to-one & (
rng f)
c= (
dom g) implies f is
one-to-one
proof
assume that
A1: (g
* f) is
one-to-one and
A2: (
rng f)
c= (
dom g);
now
let x1, x2;
assume that
A3: x1
in (
dom f) & x2
in (
dom f) and
A4: (f
. x1)
= (f
. x2);
A5: x1
in (
dom (g
* f)) & x2
in (
dom (g
* f)) by
A2,
A3,
RELAT_1: 27;
((g
* f)
. x1)
= (g
. (f
. x1)) & ((g
* f)
. x2)
= (g
. (f
. x2)) by
A3,
Th13;
hence x1
= x2 by
A1,
A4,
A5;
end;
hence thesis;
end;
theorem ::
FUNCT_1:26
(g
* f) is
one-to-one & (
rng f)
= (
dom g) implies f is
one-to-one & g is
one-to-one
proof
assume that
A1: (g
* f) is
one-to-one and
A2: (
rng f)
= (
dom g);
A3: (
dom (g
* f))
= (
dom f) by
A2,
RELAT_1: 27;
thus f is
one-to-one by
A1,
A2,
Th25;
assume not g is
one-to-one;
then
consider y1, y2 such that
A4: y1
in (
dom g) and
A5: y2
in (
dom g) and
A6: (g
. y1)
= (g
. y2) & y1
<> y2;
consider x2 be
object such that
A7: x2
in (
dom f) and
A8: (f
. x2)
= y2 by
A2,
A5,
Def3;
A9: ((g
* f)
. x2)
= (g
. (f
. x2)) by
A7,
Th13;
consider x1 be
object such that
A10: x1
in (
dom f) and
A11: (f
. x1)
= y1 by
A2,
A4,
Def3;
((g
* f)
. x1)
= (g
. (f
. x1)) by
A10,
Th13;
hence contradiction by
A1,
A6,
A10,
A11,
A7,
A8,
A3,
A9;
end;
theorem ::
FUNCT_1:27
f is
one-to-one iff for g, h st (
rng g)
c= (
dom f) & (
rng h)
c= (
dom f) & (
dom g)
= (
dom h) & (f
* g)
= (f
* h) holds g
= h
proof
thus f is
one-to-one implies for g, h st (
rng g)
c= (
dom f) & (
rng h)
c= (
dom f) & (
dom g)
= (
dom h) & (f
* g)
= (f
* h) holds g
= h
proof
assume
A1: f is
one-to-one;
let g, h such that
A2: (
rng g)
c= (
dom f) & (
rng h)
c= (
dom f) and
A3: (
dom g)
= (
dom h) and
A4: (f
* g)
= (f
* h);
x
in (
dom g) implies (g
. x)
= (h
. x)
proof
assume
A5: x
in (
dom g);
then
A6: (g
. x)
in (
rng g) & (h
. x)
in (
rng h) by
A3,
Def3;
((f
* g)
. x)
= (f
. (g
. x)) & ((f
* h)
. x)
= (f
. (h
. x)) by
A3,
A5,
Th13;
hence thesis by
A1,
A2,
A4,
A6;
end;
hence thesis by
A3,
Th2;
end;
assume
A7: for g, h st (
rng g)
c= (
dom f) & (
rng h)
c= (
dom f) & (
dom g)
= (
dom h) & (f
* g)
= (f
* h) holds g
= h;
x1
in (
dom f) & x2
in (
dom f) & (f
. x1)
= (f
. x2) implies x1
= x2
proof
assume that
A8: x1
in (
dom f) and
A9: x2
in (
dom f) and
A10: (f
. x1)
= (f
. x2);
deffunc
F(
object) = x1;
consider g be
Function such that
A11: (
dom g)
=
{
{} } and
A12: for x st x
in
{
{} } holds (g
. x)
=
F(x) from
Lambda;
A13:
{}
in
{
{} } by
TARSKI:def 1;
then
A14: (g
.
{} )
= x1 by
A12;
then (
rng g)
=
{x1} by
A11,
Th4;
then
A15: (
rng g)
c= (
dom f) by
A8,
ZFMISC_1: 31;
then
A16: (
dom (f
* g))
= (
dom g) by
RELAT_1: 27;
deffunc
F(
object) = x2;
consider h be
Function such that
A17: (
dom h)
=
{
{} } and
A18: for x st x
in
{
{} } holds (h
. x)
=
F(x) from
Lambda;
A19: (h
.
{} )
= x2 by
A18,
A13;
then (
rng h)
=
{x2} by
A17,
Th4;
then
A20: (
rng h)
c= (
dom f) by
A9,
ZFMISC_1: 31;
then
A21: (
dom (f
* h))
= (
dom h) by
RELAT_1: 27;
x
in (
dom (f
* g)) implies ((f
* g)
. x)
= ((f
* h)
. x)
proof
assume
A22: x
in (
dom (f
* g));
then
A23: (g
. x)
= x1 by
A11,
A12,
A16;
((f
* g)
. x)
= (f
. (g
. x)) & ((f
* h)
. x)
= (f
. (h
. x)) by
A11,
A17,
A16,
A21,
A22,
Th12;
hence thesis by
A10,
A11,
A18,
A16,
A22,
A23;
end;
hence thesis by
A7,
A11,
A17,
A14,
A19,
A15,
A20,
A16,
A21,
Th2;
end;
hence thesis;
end;
theorem ::
FUNCT_1:28
(
dom f)
= X & (
dom g)
= X & (
rng g)
c= X & f is
one-to-one & (f
* g)
= f implies g
= (
id X)
proof
assume that
A1: (
dom f)
= X and
A2: (
dom g)
= X and
A3: (
rng g)
c= X & f is
one-to-one and
A4: (f
* g)
= f;
x
in X implies (g
. x)
= x
proof
assume
A5: x
in X;
then (g
. x)
in (
rng g) & (f
. x)
= (f
. (g
. x)) by
A2,
A4,
Def3,
Th13;
hence thesis by
A1,
A3,
A5;
end;
hence thesis by
A2,
Th17;
end;
theorem ::
FUNCT_1:29
(
rng (g
* f))
= (
rng g) & g is
one-to-one implies (
dom g)
c= (
rng f)
proof
assume that
A1: (
rng (g
* f))
= (
rng g) and
A2: g is
one-to-one;
let y be
object;
assume
A3: y
in (
dom g);
then (g
. y)
in (
rng (g
* f)) by
A1,
Def3;
then
consider x be
object such that
A4: x
in (
dom (g
* f)) and
A5: (g
. y)
= ((g
* f)
. x) by
Def3;
((g
* f)
. x)
= (g
. (f
. x)) & (f
. x)
in (
dom g) by
A4,
Th11,
Th12;
then
A6: y
= (f
. x) by
A2,
A3,
A5;
x
in (
dom f) by
A4,
Th11;
hence thesis by
A6,
Def3;
end;
registration
let X be
set;
cluster (
id X) ->
one-to-one;
coherence
proof
let x1, x2;
assume that
A1: x1
in (
dom (
id X)) and
A2: x2
in (
dom (
id X));
x1
in X by
A1;
then
A3: ((
id X)
. x1)
= x1 by
Th17;
x2
in X by
A2;
hence thesis by
A3,
Th17;
end;
end
::$Canceled
theorem ::
FUNCT_1:31
(ex g st (g
* f)
= (
id (
dom f))) implies f is
one-to-one
proof
given g such that
A1: (g
* f)
= (
id (
dom f));
(
dom (g
* f))
= (
dom f) by
A1;
then (
rng f)
c= (
dom g) by
Th15;
hence thesis by
A1,
Th25;
end;
registration
cluster
empty ->
one-to-one for
Function;
coherence ;
end
registration
cluster
one-to-one for
Function;
existence
proof
take
{} ;
thus thesis;
end;
end
registration
let f be
one-to-one
Function;
cluster (f
~ ) ->
Function-like;
coherence
proof
let x, y1, y2;
assume that
A1:
[x, y1]
in (f
~ ) and
A2:
[x, y2]
in (f
~ );
A3:
[y2, x]
in f by
A2,
RELAT_1:def 7;
then
A4: y2
in (
dom f) by
XTUPLE_0:def 12;
reconsider x as
set by
TARSKI: 1;
A5: x
= (f
. y2) by
A3,
Def2,
A4;
A6:
[y1, x]
in f by
A1,
RELAT_1:def 7;
then
A7: y1
in (
dom f) by
XTUPLE_0:def 12;
then x
= (f
. y1) by
A6,
Def2;
hence thesis by
A7,
A4,
A5,
Def4;
end;
end
definition
let f;
assume
A1: f is
one-to-one;
::
FUNCT_1:def5
func f
" ->
Function equals
:
Def5: (f
~ );
coherence by
A1;
end
theorem ::
FUNCT_1:32
Th31: f is
one-to-one implies for g be
Function holds g
= (f
" ) iff (
dom g)
= (
rng f) & for y, x holds y
in (
rng f) & x
= (g
. y) iff x
in (
dom f) & y
= (f
. x)
proof
assume
A1: f is
one-to-one;
let g be
Function;
thus g
= (f
" ) implies (
dom g)
= (
rng f) & for y, x holds y
in (
rng f) & x
= (g
. y) iff x
in (
dom f) & y
= (f
. x)
proof
assume g
= (f
" );
then
A2: g
= (f
~ ) by
A1,
Def5;
hence (
dom g)
= (
rng f) by
RELAT_1: 20;
let y, x;
thus y
in (
rng f) & x
= (g
. y) implies x
in (
dom f) & y
= (f
. x)
proof
assume that
A3: y
in (
rng f) and
A4: x
= (g
. y);
reconsider y as
set by
TARSKI: 1;
y
in (
dom g) by
A2,
A3,
RELAT_1: 20;
then
[y, x]
in g by
A4,
Def2;
then
A5:
[x, y]
in f by
A2,
RELAT_1:def 7;
hence x
in (
dom f) by
XTUPLE_0:def 12;
hence thesis by
A5,
Def2;
end;
assume x
in (
dom f) & y
= (f
. x);
then
A6:
[x, y]
in f by
Def2;
hence y
in (
rng f) by
XTUPLE_0:def 13;
then
A7: y
in (
dom g) by
A2,
RELAT_1: 20;
reconsider x as
set by
TARSKI: 1;
[y, x]
in g by
A2,
A6,
RELAT_1:def 7;
hence thesis by
A7,
Def2;
end;
assume that
A8: (
dom g)
= (
rng f) and
A9: for y, x holds y
in (
rng f) & x
= (g
. y) iff x
in (
dom f) & y
= (f
. x);
let a,b be
object;
thus
[a, b]
in g implies
[a, b]
in (f
" )
proof
assume
A10:
[a, b]
in g;
reconsider b as
set by
TARSKI: 1;
A11: a
in (
dom g) by
XTUPLE_0:def 12,
A10;
then b
= (g
. a) by
A10,
Def2;
then b
in (
dom f) & a
= (f
. b) by
A8,
A9,
A11;
then
[b, a]
in f by
Def2;
then
[a, b]
in (f
~ ) by
RELAT_1:def 7;
hence thesis by
A1,
Def5;
end;
assume
[a, b]
in (f
" );
then
[a, b]
in (f
~ ) by
A1,
Def5;
then
A12:
[b, a]
in f by
RELAT_1:def 7;
then
A13: b
in (
dom f) by
XTUPLE_0:def 12;
reconsider a as
set by
TARSKI: 1;
a
= (f
. b) by
A12,
Def2,
A13;
then a
in (
rng f) & b
= (g
. a) by
A9,
A13;
hence thesis by
A8,
Def2;
end;
theorem ::
FUNCT_1:33
Th32: f is
one-to-one implies (
rng f)
= (
dom (f
" )) & (
dom f)
= (
rng (f
" ))
proof
assume f is
one-to-one;
then (f
" )
= (f
~ ) by
Def5;
hence thesis by
RELAT_1: 20;
end;
theorem ::
FUNCT_1:34
Th33: f is
one-to-one & x
in (
dom f) implies x
= ((f
" )
. (f
. x)) & x
= (((f
" )
* f)
. x)
proof
assume
A1: f is
one-to-one;
assume
A2: x
in (
dom f);
hence x
= ((f
" )
. (f
. x)) by
A1,
Th31;
hence thesis by
A2,
Th13;
end;
theorem ::
FUNCT_1:35
Th34: f is
one-to-one & y
in (
rng f) implies y
= (f
. ((f
" )
. y)) & y
= ((f
* (f
" ))
. y)
proof
assume
A1: f is
one-to-one;
assume
A2: y
in (
rng f);
hence
A3: y
= (f
. ((f
" )
. y)) by
A1,
Th31;
(
rng f)
= (
dom (f
" )) by
A1,
Th32;
hence thesis by
A2,
A3,
Th13;
end;
theorem ::
FUNCT_1:36
Th35: f is
one-to-one implies (
dom ((f
" )
* f))
= (
dom f) & (
rng ((f
" )
* f))
= (
dom f)
proof
assume
A1: f is
one-to-one;
then
A2: (
rng f)
= (
dom (f
" )) by
Th32;
then (
rng ((f
" )
* f))
= (
rng (f
" )) by
RELAT_1: 28;
hence thesis by
A1,
A2,
Th32,
RELAT_1: 27;
end;
theorem ::
FUNCT_1:37
Th36: f is
one-to-one implies (
dom (f
* (f
" )))
= (
rng f) & (
rng (f
* (f
" )))
= (
rng f)
proof
assume
A1: f is
one-to-one;
then
A2: (
rng (f
" ))
= (
dom f) by
Th32;
then (
dom (f
* (f
" )))
= (
dom (f
" )) by
RELAT_1: 27;
hence thesis by
A1,
A2,
Th32,
RELAT_1: 28;
end;
theorem ::
FUNCT_1:38
f is
one-to-one & (
dom f)
= (
rng g) & (
rng f)
= (
dom g) & (for x, y st x
in (
dom f) & y
in (
dom g) holds (f
. x)
= y iff (g
. y)
= x) implies g
= (f
" )
proof
assume that
A1: f is
one-to-one and
A2: (
dom f)
= (
rng g) and
A3: (
rng f)
= (
dom g) and
A4: for x, y st x
in (
dom f) & y
in (
dom g) holds (f
. x)
= y iff (g
. y)
= x;
A5: y
in (
dom g) implies (g
. y)
= ((f
" )
. y)
proof
assume
A6: y
in (
dom g);
then
A7: (g
. y)
in (
dom f) by
A2,
Def3;
then (f
. (g
. y))
= y by
A4,
A6;
hence thesis by
A1,
A7,
Th31;
end;
(
rng f)
= (
dom (f
" )) by
A1,
Th31;
hence thesis by
A3,
A5,
Th2;
end;
theorem ::
FUNCT_1:39
Th38: f is
one-to-one implies ((f
" )
* f)
= (
id (
dom f)) & (f
* (f
" ))
= (
id (
rng f))
proof
assume
A1: f is
one-to-one;
A2: x
in (
dom ((f
" )
* f)) implies (((f
" )
* f)
. x)
= x
proof
assume x
in (
dom ((f
" )
* f));
then x
in (
dom f) by
A1,
Th35;
hence thesis by
A1,
Th33;
end;
A3: x
in (
dom (f
* (f
" ))) implies ((f
* (f
" ))
. x)
= x
proof
assume x
in (
dom (f
* (f
" )));
then x
in (
rng f) by
A1,
Th36;
hence thesis by
A1,
Th34;
end;
(
dom ((f
" )
* f))
= (
dom f) by
A1,
Th35;
hence ((f
" )
* f)
= (
id (
dom f)) by
A2,
Th17;
(
dom (f
* (f
" )))
= (
rng f) by
A1,
Th36;
hence thesis by
A3,
Th17;
end;
theorem ::
FUNCT_1:40
Th39: f is
one-to-one implies (f
" ) is
one-to-one
proof
assume
A1: f is
one-to-one;
let y1, y2;
assume that
A2: y1
in (
dom (f
" )) and
A3: y2
in (
dom (f
" ));
y1
in (
rng f) by
A1,
A2,
Th31;
then
A4: y1
= (f
. ((f
" )
. y1)) by
A1,
Th34;
y2
in (
rng f) by
A1,
A3,
Th31;
hence thesis by
A1,
A4,
Th34;
end;
registration
let f be
one-to-one
Function;
cluster (f
" ) ->
one-to-one;
coherence by
Th39;
let g be
one-to-one
Function;
cluster (g
* f) ->
one-to-one;
coherence by
Th24;
end
Lm1: (
rng g2)
= X & (f
* g2)
= (
id (
dom g1)) & (g1
* f)
= (
id X) implies g1
= g2
proof
A1: (g1
* (f
* g2))
= ((g1
* f)
* g2) & (g1
* (
id (
dom g1)))
= g1 by
RELAT_1: 36,
RELAT_1: 51;
assume (
rng g2)
= X & (f
* g2)
= (
id (
dom g1)) & (g1
* f)
= (
id X);
hence thesis by
A1,
RELAT_1: 53;
end;
theorem ::
FUNCT_1:41
Th40: f is
one-to-one & (
rng f)
= (
dom g) & (g
* f)
= (
id (
dom f)) implies g
= (f
" )
proof
assume that
A1: f is
one-to-one and
A2: (
rng f)
= (
dom g) & (g
* f)
= (
id (
dom f));
(f
* (f
" ))
= (
id (
rng f)) & (
rng (f
" ))
= (
dom f) by
A1,
Th32,
Th38;
hence thesis by
A2,
Lm1;
end;
theorem ::
FUNCT_1:42
f is
one-to-one & (
rng g)
= (
dom f) & (f
* g)
= (
id (
rng f)) implies g
= (f
" )
proof
assume that
A1: f is
one-to-one and
A2: (
rng g)
= (
dom f) & (f
* g)
= (
id (
rng f));
((f
" )
* f)
= (
id (
dom f)) & (
dom (f
" ))
= (
rng f) by
A1,
Th32,
Th38;
hence thesis by
A2,
Lm1;
end;
theorem ::
FUNCT_1:43
f is
one-to-one implies ((f
" )
" )
= f
proof
assume
A1: f is
one-to-one;
then (
rng f)
= (
dom (f
" )) by
Th32;
then
A2: (f
* (f
" ))
= (
id (
dom (f
" ))) by
A1,
Th38;
(
dom f)
= (
rng (f
" )) by
A1,
Th32;
hence thesis by
A1,
A2,
Th40;
end;
theorem ::
FUNCT_1:44
f is
one-to-one & g is
one-to-one implies ((g
* f)
" )
= ((f
" )
* (g
" ))
proof
assume that
A1: f is
one-to-one and
A2: g is
one-to-one;
for y be
object holds y
in (
rng (g
* f)) iff y
in (
dom ((f
" )
* (g
" )))
proof
let y be
object;
thus y
in (
rng (g
* f)) implies y
in (
dom ((f
" )
* (g
" )))
proof
assume y
in (
rng (g
* f));
then
consider x be
object such that
A3: x
in (
dom (g
* f)) and
A4: y
= ((g
* f)
. x) by
Def3;
A5: (f
. x)
in (
dom g) by
A3,
Th11;
A6: y
= (g
. (f
. x)) by
A3,
A4,
Th12;
then y
in (
rng g) by
A5,
Def3;
then
A7: y
in (
dom (g
" )) by
A2,
Th31;
A8: x
in (
dom f) by
A3,
Th11;
((g
" )
. (g
. (f
. x)))
= (((g
" )
* g)
. (f
. x)) by
A5,
Th13
.= ((
id (
dom g))
. (f
. x)) by
A2,
Th38
.= (f
. x) by
A5,
Th17;
then ((g
" )
. y)
in (
rng f) by
A8,
A6,
Def3;
then ((g
" )
. y)
in (
dom (f
" )) by
A1,
Th31;
hence thesis by
A7,
Th11;
end;
assume
A9: y
in (
dom ((f
" )
* (g
" )));
then y
in (
dom (g
" )) by
Th11;
then y
in (
rng g) by
A2,
Th31;
then
consider z be
object such that
A10: z
in (
dom g) and
A11: y
= (g
. z) by
Def3;
((g
" )
. y)
in (
dom (f
" )) by
A9,
Th11;
then ((g
" )
. (g
. z))
in (
rng f) by
A1,
A11,
Th31;
then (((g
" )
* g)
. z)
in (
rng f) by
A10,
Th13;
then ((
id (
dom g))
. z)
in (
rng f) by
A2,
Th38;
then z
in (
rng f) by
A10,
Th17;
then
consider x be
object such that
A12: x
in (
dom f) & z
= (f
. x) by
Def3;
x
in (
dom (g
* f)) & y
= ((g
* f)
. x) by
A10,
A11,
A12,
Th11,
Th13;
hence thesis by
Def3;
end;
then
A13: (
rng (g
* f))
= (
dom ((f
" )
* (g
" ))) by
TARSKI: 2;
for x be
object holds x
in (
dom (((f
" )
* (g
" ))
* (g
* f))) iff x
in (
dom (g
* f))
proof
let x be
object;
thus x
in (
dom (((f
" )
* (g
" ))
* (g
* f))) implies x
in (
dom (g
* f)) by
Th11;
assume
A14: x
in (
dom (g
* f));
then ((g
* f)
. x)
in (
rng (g
* f)) by
Def3;
hence thesis by
A13,
A14,
Th11;
end;
then
A15: (
dom (((f
" )
* (g
" ))
* (g
* f)))
= (
dom (g
* f)) by
TARSKI: 2;
x
in (
dom (g
* f)) implies ((((f
" )
* (g
" ))
* (g
* f))
. x)
= x
proof
assume
A16: x
in (
dom (g
* f));
then
A17: (f
. x)
in (
dom g) by
Th11;
((g
* f)
. x)
in (
rng (g
* f)) by
A16,
Def3;
then
A18: (g
. (f
. x))
in (
dom ((f
" )
* (g
" ))) by
A13,
A16,
Th12;
A19: x
in (
dom f) by
A16,
Th11;
thus ((((f
" )
* (g
" ))
* (g
* f))
. x)
= (((f
" )
* (g
" ))
. ((g
* f)
. x)) by
A15,
A16,
Th12
.= (((f
" )
* (g
" ))
. (g
. (f
. x))) by
A16,
Th12
.= ((f
" )
. ((g
" )
. (g
. (f
. x)))) by
A18,
Th12
.= ((f
" )
. (((g
" )
* g)
. (f
. x))) by
A17,
Th13
.= ((f
" )
. ((
id (
dom g))
. (f
. x))) by
A2,
Th38
.= ((f
" )
. (f
. x)) by
A17,
Th17
.= x by
A1,
A19,
Th33;
end;
then (((f
" )
* (g
" ))
* (g
* f))
= (
id (
dom (g
* f))) by
A15,
Th17;
hence thesis by
A1,
A2,
A13,
Th40;
end;
theorem ::
FUNCT_1:45
((
id X)
" )
= (
id X)
proof
(
dom (
id X))
= X;
then
A1: (((
id X)
" )
* (
id X))
= (
id X) by
Th38;
(
dom ((
id X)
" ))
= (
rng (
id X)) & (
rng (
id X))
= X by
Th32;
hence thesis by
A1,
Th23;
end;
registration
let f, X;
cluster (f
| X) ->
Function-like;
coherence
proof
let x, y1, y2;
assume
[x, y1]
in (f
| X) &
[x, y2]
in (f
| X);
then
[x, y1]
in f &
[x, y2]
in f by
RELAT_1:def 11;
hence thesis by
Def1;
end;
end
theorem ::
FUNCT_1:46
(
dom g)
= ((
dom f)
/\ X) & (for x st x
in (
dom g) holds (g
. x)
= (f
. x)) implies g
= (f
| X)
proof
assume that
A1: (
dom g)
= ((
dom f)
/\ X) and
A2: for x st x
in (
dom g) holds (g
. x)
= (f
. x);
now
let x,y be
object;
hereby
assume
A3:
[x, y]
in g;
then
A4: x
in (
dom g) by
XTUPLE_0:def 12;
hence x
in X by
A1,
XBOOLE_0:def 4;
A5: x
in (
dom f) by
A1,
A4,
XBOOLE_0:def 4;
reconsider yy = y as
set by
TARSKI: 1;
yy
= (g
. x) by
A3,
A4,
Def2
.= (f
. x) by
A2,
A4;
hence
[x, y]
in f by
A5,
Def2;
end;
assume
A6: x
in X;
assume
A7:
[x, y]
in f;
then
A8: x
in (
dom f) by
XTUPLE_0:def 12;
then
A9: x
in (
dom g) by
A1,
A6,
XBOOLE_0:def 4;
reconsider yy = y as
set by
TARSKI: 1;
yy
= (f
. x) by
A7,
A8,
Def2
.= (g
. x) by
A2,
A9;
hence
[x, y]
in g by
A9,
Def2;
end;
hence thesis by
RELAT_1:def 11;
end;
theorem ::
FUNCT_1:47
Th46: x
in (
dom (f
| X)) implies ((f
| X)
. x)
= (f
. x)
proof
set g = (f
| X);
assume
A1: x
in (
dom g);
(
dom g)
= ((
dom f)
/\ X) by
RELAT_1: 61;
then
A2: x
in (
dom f) by
A1,
XBOOLE_0:def 4;
g
c= f &
[x, (g
. x)]
in g by
A1,
Def2,
RELAT_1: 59;
hence (g
. x)
= (f
. x) by
A2,
Def2;
end;
theorem ::
FUNCT_1:48
Th47: x
in ((
dom f)
/\ X) implies ((f
| X)
. x)
= (f
. x)
proof
assume x
in ((
dom f)
/\ X);
then x
in (
dom (f
| X)) by
RELAT_1: 61;
hence thesis by
Th46;
end;
theorem ::
FUNCT_1:49
Th48: x
in X implies ((f
| X)
. x)
= (f
. x)
proof
assume
A1: x
in X;
per cases ;
suppose x
in (
dom f);
then x
in (
dom (f
| X)) by
A1,
RELAT_1: 57;
hence thesis by
Th46;
end;
suppose
A2: not x
in (
dom f);
then not x
in (
dom (f
| X)) by
RELAT_1: 57;
hence ((f
| X)
. x)
=
{} by
Def2
.= (f
. x) by
A2,
Def2;
end;
end;
theorem ::
FUNCT_1:50
x
in (
dom f) & x
in X implies (f
. x)
in (
rng (f
| X))
proof
assume that
A1: x
in (
dom f) and
A2: x
in X;
x
in ((
dom f)
/\ X) by
A1,
A2,
XBOOLE_0:def 4;
then
A3: x
in (
dom (f
| X)) by
RELAT_1: 61;
((f
| X)
. x)
= (f
. x) by
A2,
Th48;
hence thesis by
A3,
Def3;
end;
theorem ::
FUNCT_1:51
X
c= Y implies ((f
| X)
| Y)
= (f
| X) & ((f
| Y)
| X)
= (f
| X) by
RELAT_1: 73,
RELAT_1: 74;
theorem ::
FUNCT_1:52
f is
one-to-one implies (f
| X) is
one-to-one
proof
assume
A1: f is
one-to-one;
let x1, x2;
assume that
A2: x1
in (
dom (f
| X)) and
A3: x2
in (
dom (f
| X));
x1
in ((
dom f)
/\ X) by
A2,
RELAT_1: 61;
then
A4: x1
in (
dom f) by
XBOOLE_0:def 4;
x2
in ((
dom f)
/\ X) by
A3,
RELAT_1: 61;
then
A5: x2
in (
dom f) by
XBOOLE_0:def 4;
((f
| X)
. x1)
= (f
. x1) & ((f
| X)
. x2)
= (f
. x2) by
A2,
A3,
Th46;
hence thesis by
A1,
A4,
A5;
end;
registration
let Y, f;
cluster (Y
|` f) ->
Function-like;
coherence
proof
let x, y1, y2;
assume
[x, y1]
in (Y
|` f) &
[x, y2]
in (Y
|` f);
then
[x, y1]
in f &
[x, y2]
in f by
RELAT_1:def 12;
hence thesis by
Def1;
end;
end
theorem ::
FUNCT_1:53
Th52: g
= (Y
|` f) iff (for x holds x
in (
dom g) iff x
in (
dom f) & (f
. x)
in Y) & for x st x
in (
dom g) holds (g
. x)
= (f
. x)
proof
hereby
assume
A1: g
= (Y
|` f);
hereby
let x;
hereby
assume x
in (
dom g);
then
A2:
[x, (g
. x)]
in g by
Def2;
then
A3:
[x, (g
. x)]
in f by
A1,
RELAT_1:def 12;
hence x
in (
dom f) by
XTUPLE_0:def 12;
then (f
. x)
= (g
. x) by
A3,
Def2;
hence (f
. x)
in Y by
A1,
A2,
RELAT_1:def 12;
end;
assume x
in (
dom f);
then
A4:
[x, (f
. x)]
in f by
Def2;
assume (f
. x)
in Y;
then
[x, (f
. x)]
in g by
A1,
A4,
RELAT_1:def 12;
hence x
in (
dom g) by
XTUPLE_0:def 12;
end;
let x;
assume x
in (
dom g);
then
[x, (g
. x)]
in g by
Def2;
then
A5:
[x, (g
. x)]
in f by
A1,
RELAT_1:def 12;
then x
in (
dom f) by
XTUPLE_0:def 12;
hence (f
. x)
= (g
. x) by
A5,
Def2;
end;
assume that
A6: for x holds x
in (
dom g) iff x
in (
dom f) & (f
. x)
in Y and
A7: for x st x
in (
dom g) holds (g
. x)
= (f
. x);
now
let x,y be
object;
hereby
assume
A8:
[x, y]
in g;
then
A9: x
in (
dom g) by
XTUPLE_0:def 12;
reconsider yy = y as
set by
TARSKI: 1;
A10: yy
= (g
. x) by
A8,
Def2,
A9
.= (f
. x) by
A7,
A9;
hence y
in Y by
A6,
A9;
x
in (
dom f) by
A6,
A9;
hence
[x, y]
in f by
A10,
Def2;
end;
assume
A11: y
in Y;
assume
A12:
[x, y]
in f;
then
A13: y
= (f
. x) by
Th1;
x
in (
dom f) by
A12,
XTUPLE_0:def 12;
then
A14: x
in (
dom g) by
A6,
A11,
A13;
then y
= (g
. x) by
A7,
A13;
hence
[x, y]
in g by
A14,
Def2;
end;
hence thesis by
RELAT_1:def 12;
end;
theorem ::
FUNCT_1:54
x
in (
dom (Y
|` f)) iff x
in (
dom f) & (f
. x)
in Y by
Th52;
theorem ::
FUNCT_1:55
x
in (
dom (Y
|` f)) implies ((Y
|` f)
. x)
= (f
. x) by
Th52;
theorem ::
FUNCT_1:56
(
dom (Y
|` f))
c= (
dom f) by
Th52;
theorem ::
FUNCT_1:57
X
c= Y implies (Y
|` (X
|` f))
= (X
|` f) & (X
|` (Y
|` f))
= (X
|` f) by
RELAT_1: 98,
RELAT_1: 99;
theorem ::
FUNCT_1:58
f is
one-to-one implies (Y
|` f) is
one-to-one
proof
assume
A1: f is
one-to-one;
let x1, x2 such that
A2: x1
in (
dom (Y
|` f)) & x2
in (
dom (Y
|` f)) and
A3: ((Y
|` f)
. x1)
= ((Y
|` f)
. x2);
A4: x1
in (
dom f) & x2
in (
dom f) by
A2,
Th52;
((Y
|` f)
. x1)
= (f
. x1) & ((Y
|` f)
. x2)
= (f
. x2) by
A2,
Th52;
hence thesis by
A1,
A3,
A4;
end;
definition
let f, X;
:: original:
.:
redefine
::
FUNCT_1:def6
func f
.: X means
:
Def6: for y be
object holds y
in it iff ex x be
object st x
in (
dom f) & x
in X & y
= (f
. x);
compatibility
proof
let Y;
hereby
assume
A1: Y
= (f
.: X);
let y be
object;
hereby
assume y
in Y;
then
consider x be
object such that
A2:
[x, y]
in f and
A3: x
in X by
A1,
RELAT_1:def 13;
reconsider x as
object;
take x;
thus
A4: x
in (
dom f) by
A2,
XTUPLE_0:def 12;
reconsider yy = y as
set by
TARSKI: 1;
thus x
in X by
A3;
yy
= (f
. x) by
A2,
A4,
Def2;
hence y
= (f
. x);
end;
given x be
object such that
A5: x
in (
dom f) and
A6: x
in X and
A7: y
= (f
. x);
[x, y]
in f by
A5,
A7,
Def2;
hence y
in Y by
A1,
A6,
RELAT_1:def 13;
end;
assume
A8: for y be
object holds y
in Y iff ex x be
object st x
in (
dom f) & x
in X & y
= (f
. x);
now
let y be
object;
hereby
assume y
in Y;
then
consider x be
object such that
A9: x
in (
dom f) and
A10: x
in X and
A11: y
= (f
. x) by
A8;
reconsider x as
object;
take x;
thus
[x, y]
in f by
A9,
A11,
Def2;
thus x
in X by
A10;
end;
given x be
object such that
A12:
[x, y]
in f and
A13: x
in X;
x
in (
dom f) & y
= (f
. x) by
A12,
Th1;
hence y
in Y by
A8,
A13;
end;
hence thesis by
RELAT_1:def 13;
end;
end
theorem ::
FUNCT_1:59
Th58: x
in (
dom f) implies (
Im (f,x))
=
{(f
. x)}
proof
assume
A1: x
in (
dom f);
for y be
object holds y
in (f
.:
{x}) iff y
in
{(f
. x)}
proof
let y be
object;
thus y
in (f
.:
{x}) implies y
in
{(f
. x)}
proof
assume y
in (f
.:
{x});
then
consider z be
object such that z
in (
dom f) and
A2: z
in
{x} and
A3: y
= (f
. z) by
Def6;
z
= x by
A2,
TARSKI:def 1;
hence thesis by
A3,
TARSKI:def 1;
end;
assume y
in
{(f
. x)};
then
A4: y
= (f
. x) by
TARSKI:def 1;
x
in
{x} by
TARSKI:def 1;
hence thesis by
A1,
A4,
Def6;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
FUNCT_1:60
x1
in (
dom f) & x2
in (
dom f) implies (f
.:
{x1, x2})
=
{(f
. x1), (f
. x2)}
proof
assume
A1: x1
in (
dom f) & x2
in (
dom f);
for y be
object holds y
in (f
.:
{x1, x2}) iff y
= (f
. x1) or y
= (f
. x2)
proof
let y be
object;
A2: x1
in
{x1, x2} & x2
in
{x1, x2} by
TARSKI:def 2;
thus y
in (f
.:
{x1, x2}) implies y
= (f
. x1) or y
= (f
. x2)
proof
assume y
in (f
.:
{x1, x2});
then ex x be
object st x
in (
dom f) & x
in
{x1, x2} & y
= (f
. x) by
Def6;
hence thesis by
TARSKI:def 2;
end;
assume y
= (f
. x1) or y
= (f
. x2);
hence thesis by
A1,
A2,
Def6;
end;
hence thesis by
TARSKI:def 2;
end;
theorem ::
FUNCT_1:61
((Y
|` f)
.: X)
c= (f
.: X)
proof
let y be
object;
assume y
in ((Y
|` f)
.: X);
then
consider x be
object such that
A1: x
in (
dom (Y
|` f)) and
A2: x
in X and
A3: y
= ((Y
|` f)
. x) by
Def6;
y
= (f
. x) & x
in (
dom f) by
A1,
A3,
Th52;
hence thesis by
A2,
Def6;
end;
theorem ::
FUNCT_1:62
Th61: f is
one-to-one implies (f
.: (X1
/\ X2))
= ((f
.: X1)
/\ (f
.: X2))
proof
assume
A1: f is
one-to-one;
A2: ((f
.: X1)
/\ (f
.: X2))
c= (f
.: (X1
/\ X2))
proof
let y be
object;
assume
A3: y
in ((f
.: X1)
/\ (f
.: X2));
then y
in (f
.: X1) by
XBOOLE_0:def 4;
then
consider x1 be
object such that
A4: x1
in (
dom f) and
A5: x1
in X1 and
A6: y
= (f
. x1) by
Def6;
y
in (f
.: X2) by
A3,
XBOOLE_0:def 4;
then
consider x2 be
object such that
A7: x2
in (
dom f) and
A8: x2
in X2 and
A9: y
= (f
. x2) by
Def6;
x1
= x2 by
A1,
A4,
A6,
A7,
A9;
then x1
in (X1
/\ X2) by
A5,
A8,
XBOOLE_0:def 4;
hence thesis by
A4,
A6,
Def6;
end;
(f
.: (X1
/\ X2))
c= ((f
.: X1)
/\ (f
.: X2)) by
RELAT_1: 121;
hence thesis by
A2;
end;
theorem ::
FUNCT_1:63
(for X1, X2 holds (f
.: (X1
/\ X2))
= ((f
.: X1)
/\ (f
.: X2))) implies f is
one-to-one
proof
assume
A1: for X1, X2 holds (f
.: (X1
/\ X2))
= ((f
.: X1)
/\ (f
.: X2));
given x1, x2 such that
A2: x1
in (
dom f) & x2
in (
dom f) and
A3: (f
. x1)
= (f
. x2) and
A4: x1
<> x2;
A5: (f
.: (
{x1}
/\
{x2}))
= ((f
.:
{x1})
/\ (f
.:
{x2})) by
A1;
{x1}
misses
{x2} by
A4,
ZFMISC_1: 11;
then
A6: (
{x1}
/\
{x2})
=
{} ;
(
Im (f,x1))
=
{(f
. x1)} & (
Im (f,x2))
=
{(f
. x2)} by
A2,
Th58;
hence contradiction by
A3,
A6,
A5;
end;
theorem ::
FUNCT_1:64
f is
one-to-one implies (f
.: (X1
\ X2))
= ((f
.: X1)
\ (f
.: X2))
proof
assume
A1: f is
one-to-one;
A2: (f
.: (X1
\ X2))
c= ((f
.: X1)
\ (f
.: X2))
proof
let y be
object;
assume y
in (f
.: (X1
\ X2));
then
consider x be
object such that
A3: x
in (
dom f) and
A4: x
in (X1
\ X2) and
A5: y
= (f
. x) by
Def6;
A6: not x
in X2 by
A4,
XBOOLE_0:def 5;
A7:
now
assume y
in (f
.: X2);
then ex z be
object st z
in (
dom f) & z
in X2 & y
= (f
. z) by
Def6;
hence contradiction by
A1,
A3,
A5,
A6;
end;
y
in (f
.: X1) by
A3,
A4,
A5,
Def6;
hence thesis by
A7,
XBOOLE_0:def 5;
end;
((f
.: X1)
\ (f
.: X2))
c= (f
.: (X1
\ X2)) by
RELAT_1: 122;
hence thesis by
A2;
end;
theorem ::
FUNCT_1:65
(for X1, X2 holds (f
.: (X1
\ X2))
= ((f
.: X1)
\ (f
.: X2))) implies f is
one-to-one
proof
assume
A1: for X1, X2 holds (f
.: (X1
\ X2))
= ((f
.: X1)
\ (f
.: X2));
given x1, x2 such that
A2: x1
in (
dom f) & x2
in (
dom f) and
A3: (f
. x1)
= (f
. x2) and
A4: x1
<> x2;
A5: (f
.: (
{x1}
\
{x2}))
= (f
.:
{x1}) by
A4,
ZFMISC_1: 14;
A6: (f
.: (
{x1}
\
{x2}))
= ((f
.:
{x1})
\ (f
.:
{x2})) by
A1;
(
Im (f,x1))
=
{(f
. x1)} & (
Im (f,x2))
=
{(f
. x2)} by
A2,
Th58;
hence contradiction by
A3,
A5,
A6,
XBOOLE_1: 37;
end;
theorem ::
FUNCT_1:66
X
misses Y & f is
one-to-one implies (f
.: X)
misses (f
.: Y)
proof
assume (X
/\ Y)
=
{} & f is
one-to-one;
then (f
.: (X
/\ Y))
=
{} & (f
.: (X
/\ Y))
= ((f
.: X)
/\ (f
.: Y)) by
Th61;
hence thesis;
end;
theorem ::
FUNCT_1:67
((Y
|` f)
.: X)
= (Y
/\ (f
.: X))
proof
for y be
object holds y
in ((Y
|` f)
.: X) iff y
in (Y
/\ (f
.: X))
proof
let y be
object;
thus y
in ((Y
|` f)
.: X) implies y
in (Y
/\ (f
.: X))
proof
assume y
in ((Y
|` f)
.: X);
then
consider x be
object such that
A1: x
in (
dom (Y
|` f)) and
A2: x
in X and
A3: y
= ((Y
|` f)
. x) by
Def6;
A4: y
= (f
. x) by
A1,
A3,
Th52;
then
A5: y
in Y by
A1,
Th52;
x
in (
dom f) by
A1,
Th52;
then y
in (f
.: X) by
A2,
A4,
Def6;
hence thesis by
A5,
XBOOLE_0:def 4;
end;
assume
A6: y
in (Y
/\ (f
.: X));
then y
in (f
.: X) by
XBOOLE_0:def 4;
then
consider x be
object such that
A7: x
in (
dom f) and
A8: x
in X and
A9: y
= (f
. x) by
Def6;
y
in Y by
A6,
XBOOLE_0:def 4;
then
A10: x
in (
dom (Y
|` f)) by
A7,
A9,
Th52;
then ((Y
|` f)
. x)
= (f
. x) by
Th52;
hence thesis by
A8,
A9,
A10,
Def6;
end;
hence thesis by
TARSKI: 2;
end;
definition
let f, Y;
:: original:
"
redefine
::
FUNCT_1:def7
func f
" Y means
:
Def7: for x holds x
in it iff x
in (
dom f) & (f
. x)
in Y;
compatibility
proof
let X;
hereby
assume
A1: X
= (f
" Y);
let x;
hereby
assume x
in X;
then
A2: ex y be
object st
[x, y]
in f & y
in Y by
A1,
RELAT_1:def 14;
hence x
in (
dom f) by
XTUPLE_0:def 12;
thus (f
. x)
in Y by
A2,
Th1;
end;
assume that
A3: x
in (
dom f) and
A4: (f
. x)
in Y;
[x, (f
. x)]
in f by
A3,
Th1;
hence x
in X by
A1,
A4,
RELAT_1:def 14;
end;
assume
A5: for x holds x
in X iff x
in (
dom f) & (f
. x)
in Y;
now
let x be
object;
hereby
assume
A6: x
in X;
reconsider y = (f
. x) as
object;
take y;
x
in (
dom f) by
A5,
A6;
hence
[x, y]
in f by
Def2;
thus y
in Y by
A5,
A6;
end;
given y be
object such that
A7:
[x, y]
in f and
A8: y
in Y;
x
in (
dom f) & y
= (f
. x) by
A7,
Th1;
hence x
in X by
A5,
A8;
end;
hence thesis by
RELAT_1:def 14;
end;
end
theorem ::
FUNCT_1:68
Th67: (f
" (Y1
/\ Y2))
= ((f
" Y1)
/\ (f
" Y2))
proof
for x be
object holds x
in (f
" (Y1
/\ Y2)) iff x
in ((f
" Y1)
/\ (f
" Y2))
proof
let x be
object;
reconsider x as
set by
TARSKI: 1;
A1: x
in (f
" Y2) iff (f
. x)
in Y2 & x
in (
dom f) by
Def7;
A2: x
in (f
" (Y1
/\ Y2)) iff (f
. x)
in (Y1
/\ Y2) & x
in (
dom f) by
Def7;
x
in (f
" Y1) iff (f
. x)
in Y1 & x
in (
dom f) by
Def7;
then x
in (f
" (Y1
/\ Y2)) iff x
in ((f
" Y1)
/\ (f
" Y2)) by
A1,
A2,
XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
FUNCT_1:69
(f
" (Y1
\ Y2))
= ((f
" Y1)
\ (f
" Y2))
proof
for x be
object holds x
in (f
" (Y1
\ Y2)) iff x
in ((f
" Y1)
\ (f
" Y2))
proof
let x be
object;
A1: x
in (f
" Y2) iff (f
. x)
in Y2 & x
in (
dom f) by
Def7;
A2: x
in (f
" (Y1
\ Y2)) iff (f
. x)
in (Y1
\ Y2) & x
in (
dom f) by
Def7;
x
in (f
" Y1) iff (f
. x)
in Y1 & x
in (
dom f) by
Def7;
hence thesis by
A1,
A2,
XBOOLE_0:def 5;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
FUNCT_1:70
((R
| X)
" Y)
= (X
/\ (R
" Y))
proof
hereby
let x be
object;
assume x
in ((R
| X)
" Y);
then
A1: ex y be
object st
[x, y]
in (R
| X) & y
in Y by
RELAT_1:def 14;
then
A2: x
in X by
RELAT_1:def 11;
(R
| X)
c= R by
RELAT_1: 59;
then x
in (R
" Y) by
A1,
RELAT_1:def 14;
hence x
in (X
/\ (R
" Y)) by
A2,
XBOOLE_0:def 4;
end;
let x be
object;
assume
A3: x
in (X
/\ (R
" Y));
then x
in (R
" Y) by
XBOOLE_0:def 4;
then
consider y be
object such that
A4:
[x, y]
in R and
A5: y
in Y by
RELAT_1:def 14;
x
in X by
A3,
XBOOLE_0:def 4;
then
[x, y]
in (R
| X) by
A4,
RELAT_1:def 11;
hence thesis by
A5,
RELAT_1:def 14;
end;
theorem ::
FUNCT_1:71
for f be
Function, A,B be
set st A
misses B holds (f
" A)
misses (f
" B)
proof
let f be
Function, A,B be
set;
assume A
misses B;
then (A
/\ B)
=
{} ;
then
{}
= (f
" (A
/\ B))
.= ((f
" A)
/\ (f
" B)) by
Th67;
hence thesis;
end;
theorem ::
FUNCT_1:72
Th71: y
in (
rng R) iff (R
"
{y})
<>
{}
proof
thus y
in (
rng R) implies (R
"
{y})
<>
{}
proof
assume y
in (
rng R);
then
A1: ex x be
object st
[x, y]
in R by
XTUPLE_0:def 13;
y
in
{y} by
TARSKI:def 1;
hence thesis by
A1,
RELAT_1:def 14;
end;
assume (R
"
{y})
<>
{} ;
then
consider x be
object such that
A2: x
in (R
"
{y}) by
XBOOLE_0:def 1;
consider z be
object such that
A3:
[x, z]
in R and
A4: z
in
{y} by
A2,
RELAT_1:def 14;
z
= y by
A4,
TARSKI:def 1;
hence thesis by
A3,
XTUPLE_0:def 13;
end;
theorem ::
FUNCT_1:73
(for y st y
in Y holds (R
"
{y})
<>
{} ) implies Y
c= (
rng R)
proof
assume
A1: for y st y
in Y holds (R
"
{y})
<>
{} ;
let y be
object;
assume y
in Y;
then (R
"
{y})
<>
{} by
A1;
hence thesis by
Th71;
end;
theorem ::
FUNCT_1:74
Th73: (for y st y
in (
rng f) holds ex x st (f
"
{y})
=
{x}) iff f is
one-to-one
proof
thus (for y st y
in (
rng f) holds ex x st (f
"
{y})
=
{x}) implies f is
one-to-one
proof
assume
A1: for y st y
in (
rng f) holds ex x st (f
"
{y})
=
{x};
let x1, x2;
assume that
A2: x1
in (
dom f) and
A3: x2
in (
dom f);
(f
. x1)
in (
rng f) by
A2,
Def3;
then
consider y1 such that
A4: (f
"
{(f
. x1)})
=
{y1} by
A1;
(f
. x2)
in (
rng f) by
A3,
Def3;
then
consider y2 such that
A5: (f
"
{(f
. x2)})
=
{y2} by
A1;
(f
. x1)
in
{(f
. x1)} by
TARSKI:def 1;
then x1
in
{y1} by
A2,
A4,
Def7;
then
A6: y1
= x1 by
TARSKI:def 1;
(f
. x2)
in
{(f
. x2)} by
TARSKI:def 1;
then x2
in
{y2} by
A3,
A5,
Def7;
hence thesis by
A4,
A5,
A6,
TARSKI:def 1;
end;
assume
A7: f is
one-to-one;
let y;
assume y
in (
rng f);
then
consider x be
object such that
A8: x
in (
dom f) & y
= (f
. x) by
Def3;
take x;
for z be
object holds z
in (f
"
{y}) iff z
= x
proof
let z be
object;
thus z
in (f
"
{y}) implies z
= x
proof
assume
A9: z
in (f
"
{y});
then (f
. z)
in
{y} by
Def7;
then
A10: (f
. z)
= y by
TARSKI:def 1;
z
in (
dom f) by
A9,
Def7;
hence thesis by
A7,
A8,
A10;
end;
y
in
{y} by
TARSKI:def 1;
hence thesis by
A8,
Def7;
end;
hence thesis by
TARSKI:def 1;
end;
theorem ::
FUNCT_1:75
Th74: (f
.: (f
" Y))
c= Y
proof
let y be
object;
assume y
in (f
.: (f
" Y));
then ex x be
object st x
in (
dom f) & x
in (f
" Y) & y
= (f
. x) by
Def6;
hence thesis by
Def7;
end;
theorem ::
FUNCT_1:76
Th75: X
c= (
dom R) implies X
c= (R
" (R
.: X))
proof
assume
A1: X
c= (
dom R);
let x be
object;
assume
A2: x
in X;
then
consider Rx be
object such that
A3:
[x, Rx]
in R by
A1,
XTUPLE_0:def 12;
Rx
in (R
.: X) by
A2,
A3,
RELAT_1:def 13;
hence thesis by
A3,
RELAT_1:def 14;
end;
theorem ::
FUNCT_1:77
Y
c= (
rng f) implies (f
.: (f
" Y))
= Y
proof
assume
A1: Y
c= (
rng f);
thus (f
.: (f
" Y))
c= Y by
Th74;
let y be
object;
assume
A2: y
in Y;
then
consider x be
object such that
A3: x
in (
dom f) & y
= (f
. x) by
A1,
Def3;
x
in (f
" Y) by
A2,
A3,
Def7;
hence thesis by
A3,
Def6;
end;
theorem ::
FUNCT_1:78
(f
.: (f
" Y))
= (Y
/\ (f
.: (
dom f)))
proof
(f
.: (f
" Y))
c= Y & (f
.: (f
" Y))
c= (f
.: (
dom f)) by
Th74,
RELAT_1: 114;
hence (f
.: (f
" Y))
c= (Y
/\ (f
.: (
dom f))) by
XBOOLE_1: 19;
let y be
object;
assume
A1: y
in (Y
/\ (f
.: (
dom f)));
then y
in (f
.: (
dom f)) by
XBOOLE_0:def 4;
then
consider x be
object such that
A2: x
in (
dom f) and x
in (
dom f) and
A3: y
= (f
. x) by
Def6;
y
in Y by
A1,
XBOOLE_0:def 4;
then x
in (f
" Y) by
A2,
A3,
Def7;
hence thesis by
A2,
A3,
Def6;
end;
theorem ::
FUNCT_1:79
Th78: (f
.: (X
/\ (f
" Y)))
c= ((f
.: X)
/\ Y)
proof
let y be
object;
assume y
in (f
.: (X
/\ (f
" Y)));
then
consider x be
object such that
A1: x
in (
dom f) and
A2: x
in (X
/\ (f
" Y)) and
A3: y
= (f
. x) by
Def6;
x
in (f
" Y) by
A2,
XBOOLE_0:def 4;
then
A4: y
in Y by
A3,
Def7;
x
in X by
A2,
XBOOLE_0:def 4;
then y
in (f
.: X) by
A1,
A3,
Def6;
hence thesis by
A4,
XBOOLE_0:def 4;
end;
theorem ::
FUNCT_1:80
(f
.: (X
/\ (f
" Y)))
= ((f
.: X)
/\ Y)
proof
thus (f
.: (X
/\ (f
" Y)))
c= ((f
.: X)
/\ Y) by
Th78;
let y be
object;
assume
A1: y
in ((f
.: X)
/\ Y);
then y
in (f
.: X) by
XBOOLE_0:def 4;
then
consider x be
object such that
A2: x
in (
dom f) and
A3: x
in X and
A4: y
= (f
. x) by
Def6;
y
in Y by
A1,
XBOOLE_0:def 4;
then x
in (f
" Y) by
A2,
A4,
Def7;
then x
in (X
/\ (f
" Y)) by
A3,
XBOOLE_0:def 4;
hence thesis by
A2,
A4,
Def6;
end;
theorem ::
FUNCT_1:81
(X
/\ (R
" Y))
c= (R
" ((R
.: X)
/\ Y))
proof
let x be
object;
assume
A1: x
in (X
/\ (R
" Y));
then x
in (R
" Y) by
XBOOLE_0:def 4;
then
consider Rx be
object such that
A2:
[x, Rx]
in R and
A3: Rx
in Y by
RELAT_1:def 14;
x
in X by
A1,
XBOOLE_0:def 4;
then Rx
in (R
.: X) by
A2,
RELAT_1:def 13;
then Rx
in ((R
.: X)
/\ Y) by
A3,
XBOOLE_0:def 4;
hence thesis by
A2,
RELAT_1:def 14;
end;
theorem ::
FUNCT_1:82
Th81: f is
one-to-one implies (f
" (f
.: X))
c= X
proof
assume
A1: f is
one-to-one;
let x be
object;
assume
A2: x
in (f
" (f
.: X));
then (f
. x)
in (f
.: X) by
Def7;
then
A3: ex z be
object st z
in (
dom f) & z
in X & (f
. x)
= (f
. z) by
Def6;
x
in (
dom f) by
A2,
Def7;
hence thesis by
A1,
A3;
end;
theorem ::
FUNCT_1:83
(for X holds (f
" (f
.: X))
c= X) implies f is
one-to-one
proof
assume
A1: for X holds (f
" (f
.: X))
c= X;
given x1, x2 such that
A2: x1
in (
dom f) and
A3: x2
in (
dom f) and
A4: (f
. x1)
= (f
. x2) & x1
<> x2;
A5: (f
" (f
.:
{x1}))
c=
{x1} by
A1;
A6: (
Im (f,x2))
=
{(f
. x2)} by
A3,
Th58;
A7: (
Im (f,x1))
=
{(f
. x1)} by
A2,
Th58;
(f
. x1)
in (
rng f) by
A2,
Def3;
then (f
" (f
.:
{x1}))
<>
{} by
A7,
Th71;
then (f
" (f
.:
{x1}))
=
{x1} by
A5,
ZFMISC_1: 33;
hence contradiction by
A1,
A4,
A7,
A6,
ZFMISC_1: 3;
end;
theorem ::
FUNCT_1:84
f is
one-to-one implies (f
.: X)
= ((f
" )
" X)
proof
assume
A1: f is
one-to-one;
for y be
object holds y
in (f
.: X) iff y
in ((f
" )
" X)
proof
let y be
object;
thus y
in (f
.: X) implies y
in ((f
" )
" X)
proof
assume y
in (f
.: X);
then
consider x be
object such that
A2: x
in (
dom f) and
A3: x
in X and
A4: y
= (f
. x) by
Def6;
y
in (
rng f) by
A2,
A4,
Def3;
then
A5: y
in (
dom (f
" )) by
A1,
Th31;
((f
" )
. (f
. x))
= x by
A1,
A2,
Th31;
hence thesis by
A3,
A4,
A5,
Def7;
end;
assume
A6: y
in ((f
" )
" X);
then
A7: ((f
" )
. y)
in X by
Def7;
y
in (
dom (f
" )) by
A6,
Def7;
then y
in (
rng f) by
A1,
Th31;
then
consider x be
object such that
A8: x
in (
dom f) & y
= (f
. x) by
Def3;
((f
" )
. y)
= x by
A1,
A8,
Th33;
hence thesis by
A7,
A8,
Def6;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
FUNCT_1:85
f is
one-to-one implies (f
" Y)
= ((f
" )
.: Y)
proof
assume
A1: f is
one-to-one;
for x be
object holds x
in (f
" Y) iff x
in ((f
" )
.: Y)
proof
let x be
object;
thus x
in (f
" Y) implies x
in ((f
" )
.: Y)
proof
assume
A2: x
in (f
" Y);
then
A3: (f
. x)
in Y by
Def7;
A4: x
in (
dom f) by
A2,
Def7;
then (f
. x)
in (
rng f) by
Def3;
then
A5: (f
. x)
in (
dom (f
" )) by
A1,
Th31;
((f
" )
. (f
. x))
= x by
A1,
A4,
Th31;
hence thesis by
A3,
A5,
Def6;
end;
assume x
in ((f
" )
.: Y);
then
consider y be
object such that
A6: y
in (
dom (f
" )) and
A7: y
in Y and
A8: x
= ((f
" )
. y) by
Def6;
(
dom (f
" ))
= (
rng f) by
A1,
Th31;
then y
= (f
. x) & x
in (
dom f) by
A1,
A6,
A8,
Th31;
hence thesis by
A7,
Def7;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
FUNCT_1:86
Y
= (
rng f) & (
dom g)
= Y & (
dom h)
= Y & (g
* f)
= (h
* f) implies g
= h
proof
assume that
A1: Y
= (
rng f) and
A2: (
dom g)
= Y & (
dom h)
= Y and
A3: (g
* f)
= (h
* f);
y
in Y implies (g
. y)
= (h
. y)
proof
assume y
in Y;
then
consider x be
object such that
A4: x
in (
dom f) & y
= (f
. x) by
A1,
Def3;
((g
* f)
. x)
= (g
. y) by
A4,
Th13;
hence thesis by
A3,
A4,
Th13;
end;
hence thesis by
A2,
Th2;
end;
theorem ::
FUNCT_1:87
(f
.: X1)
c= (f
.: X2) & X1
c= (
dom f) & f is
one-to-one implies X1
c= X2
proof
assume that
A1: (f
.: X1)
c= (f
.: X2) and
A2: X1
c= (
dom f) and
A3: f is
one-to-one;
let x be
object;
assume
A4: x
in X1;
then (f
. x)
in (f
.: X1) by
A2,
Def6;
then ex x2 be
object st x2
in (
dom f) & x2
in X2 & (f
. x)
= (f
. x2) by
A1,
Def6;
hence thesis by
A2,
A3,
A4;
end;
theorem ::
FUNCT_1:88
Th87: (f
" Y1)
c= (f
" Y2) & Y1
c= (
rng f) implies Y1
c= Y2
proof
assume that
A1: (f
" Y1)
c= (f
" Y2) and
A2: Y1
c= (
rng f);
let y be
object;
assume
A3: y
in Y1;
then
consider x be
object such that
A4: x
in (
dom f) and
A5: y
= (f
. x) by
A2,
Def3;
x
in (f
" Y1) by
A3,
A4,
A5,
Def7;
hence thesis by
A1,
A5,
Def7;
end;
theorem ::
FUNCT_1:89
f is
one-to-one iff for y holds ex x st (f
"
{y})
c=
{x}
proof
(for y holds ex x st (f
"
{y})
c=
{x}) iff for y st y
in (
rng f) holds ex x st (f
"
{y})
=
{x}
proof
thus (for y holds ex x st (f
"
{y})
c=
{x}) implies for y st y
in (
rng f) holds ex x st (f
"
{y})
=
{x}
proof
assume
A1: for y holds ex x st (f
"
{y})
c=
{x};
let y;
consider x such that
A2: (f
"
{y})
c=
{x} by
A1;
assume y
in (
rng f);
then
consider x1 be
object such that
A3: x1
in (
dom f) and
A4: y
= (f
. x1) by
Def3;
take x;
(f
. x1)
in
{y} by
A4,
TARSKI:def 1;
then (f
"
{y})
<>
{} by
A3,
Def7;
hence thesis by
A2,
ZFMISC_1: 33;
end;
assume
A5: for y st y
in (
rng f) holds ex x st (f
"
{y})
=
{x};
let y;
A6:
now
set x = the
set;
assume
A7: not y
in (
rng f);
take x;
(
rng f)
misses
{y} by
A7,
ZFMISC_1: 50;
then (f
"
{y})
=
{} by
RELAT_1: 138;
hence (f
"
{y})
c=
{x};
end;
now
assume y
in (
rng f);
then
consider x such that
A8: (f
"
{y})
=
{x} by
A5;
take x;
thus (f
"
{y})
c=
{x} by
A8;
end;
hence thesis by
A6;
end;
hence thesis by
Th73;
end;
theorem ::
FUNCT_1:90
(
rng R)
c= (
dom S) implies (R
" X)
c= ((R
* S)
" (S
.: X))
proof
assume
A1: (
rng R)
c= (
dom S);
let x be
object;
assume x
in (R
" X);
then
consider Rx be
object such that
A2:
[x, Rx]
in R and
A3: Rx
in X by
RELAT_1:def 14;
Rx
in (
rng R) by
A2,
XTUPLE_0:def 13;
then
consider SRx be
object such that
A4:
[Rx, SRx]
in S by
A1,
XTUPLE_0:def 12;
SRx
in (S
.: X) &
[x, SRx]
in (R
* S) by
A2,
A3,
A4,
RELAT_1:def 8,
RELAT_1:def 13;
hence thesis by
RELAT_1:def 14;
end;
theorem ::
FUNCT_1:91
for f be
Function st (f
" X)
= (f
" Y) & X
c= (
rng f) & Y
c= (
rng f) holds X
= Y by
Th87;
begin
reserve e,u for
object,
A for
Subset of X;
theorem ::
FUNCT_1:92
((
id X)
.: A)
= A
proof
now
let e be
object;
thus e
in A implies ex u be
object st u
in (
dom (
id X)) & u
in A & e
= ((
id X)
. u)
proof
assume
A1: e
in A;
take e;
thus e
in (
dom (
id X)) by
A1;
thus e
in A by
A1;
thus thesis by
A1,
Th17;
end;
assume ex u be
object st u
in (
dom (
id X)) & u
in A & e
= ((
id X)
. u);
hence e
in A by
Th17;
end;
hence thesis by
Def6;
end;
definition
let f be
Function;
:: original:
empty-yielding
redefine
::
FUNCT_1:def8
attr f is
empty-yielding means
:
Def8: for x st x
in (
dom f) holds (f
. x) is
empty;
compatibility
proof
hereby
assume
A1: f is
empty-yielding;
let x;
assume x
in (
dom f);
then (f
. x)
in (
rng f) by
Def3;
hence (f
. x) is
empty by
A1,
RELAT_1: 149;
end;
assume
A2: for x st x
in (
dom f) holds (f
. x) is
empty;
let s be
object;
assume s
in (
rng f);
then ex e be
object st e
in (
dom f) & s
= (f
. e) by
Def3;
then s
=
{} by
A2;
hence thesis by
TARSKI:def 1;
end;
end
definition
let F be
Function;
:: original:
non-empty
redefine
::
FUNCT_1:def9
attr F is
non-empty means
:
Def9: for n be
object st n
in (
dom F) holds (F
. n) is non
empty;
compatibility
proof
thus F is
non-empty implies for n be
object st n
in (
dom F) holds (F
. n) is non
empty by
Def3;
assume
A1: for n be
object st n
in (
dom F) holds (F
. n) is non
empty;
assume
{}
in (
rng F);
then ex i be
object st i
in (
dom F) & (F
. i)
=
{} by
Def3;
hence contradiction by
A1;
end;
end
registration
cluster
non-empty for
Function;
existence
proof
take
{} ;
let x be
object;
thus thesis;
end;
end
scheme ::
FUNCT_1:sch4
LambdaB { D() -> non
empty
set , F(
object) ->
object } :
ex f be
Function st (
dom f)
= D() & for d be
Element of D() holds (f
. d)
= F(d);
consider f be
Function such that
A1: (
dom f)
= D() & for d be
object st d
in D() holds (f
. d)
= F(d) from
Lambda;
take f;
thus thesis by
A1;
end;
registration
let f be
non-empty
Function;
cluster (
rng f) ->
with_non-empty_elements;
coherence
proof
assume
{}
in (
rng f);
then ex x be
object st x
in (
dom f) &
{}
= (f
. x) by
Def3;
hence thesis by
Def9;
end;
end
definition
let f be
Function;
::
FUNCT_1:def10
attr f is
constant means
:
Def10: x
in (
dom f) & y
in (
dom f) implies (f
. x)
= (f
. y);
end
theorem ::
FUNCT_1:93
for A,B be
set, f be
Function st A
c= (
dom f) & (f
.: A)
c= B holds A
c= (f
" B)
proof
let A,B be
set, f be
Function;
assume A
c= (
dom f);
then
A1: A
c= (f
" (f
.: A)) by
Th75;
assume (f
.: A)
c= B;
then (f
" (f
.: A))
c= (f
" B) by
RELAT_1: 143;
hence thesis by
A1;
end;
theorem ::
FUNCT_1:94
for f be
Function st X
c= (
dom f) & f is
one-to-one holds (f
" (f
.: X))
= X
proof
let f be
Function such that
A1: X
c= (
dom f) and
A2: f is
one-to-one;
thus (f
" (f
.: X))
c= X by
A2,
Th81;
let x be
object;
assume
A3: x
in X;
then (f
. x)
in (f
.: X) by
A1,
Def6;
hence thesis by
A1,
A3,
Def7;
end;
definition
let f, g;
:: original:
=
redefine
::
FUNCT_1:def11
pred f
= g means (
dom f)
= (
dom g) & for x st x
in (
dom f) holds (f
. x)
= (g
. x);
compatibility by
Th2;
end
registration
cluster
non-empty non
empty for
Function;
existence
proof
consider f such that
A1: (
dom f)
=
{
{} } and
A2: (
rng f)
=
{
{
{} }} by
Th5;
take f;
not
{}
in (
rng f) by
A2,
TARSKI:def 1;
hence f is
non-empty;
thus thesis by
A1;
end;
end
registration
let a be
non-empty non
empty
Function;
let i be
Element of (
dom a);
cluster (a
. i) -> non
empty;
coherence
proof
(a
. i)
in (
rng a) by
Def3;
hence thesis by
RELAT_1:def 9;
end;
end
registration
let f be
Function;
cluster ->
Function-like for
Subset of f;
coherence by
Def1;
end
theorem ::
FUNCT_1:95
for f,g be
Function, D be
set st D
c= (
dom f) & D
c= (
dom g) holds (f
| D)
= (g
| D) iff for x be
set st x
in D holds (f
. x)
= (g
. x)
proof
let f,g be
Function;
let D be
set;
assume that
A1: D
c= (
dom f) and
A2: D
c= (
dom g);
A3: (
dom (g
| D))
= ((
dom g)
/\ D) by
RELAT_1: 61
.= D by
A2,
XBOOLE_1: 28;
hereby
assume
A4: (f
| D)
= (g
| D);
hereby
let x be
set;
assume
A5: x
in D;
hence (f
. x)
= ((g
| D)
. x) by
A4,
Th48
.= (g
. x) by
A5,
Th48;
end;
end;
assume
A6: for x be
set st x
in D holds (f
. x)
= (g
. x);
A7:
now
let x be
object;
assume
A8: x
in D;
hence ((f
| D)
. x)
= (f
. x) by
Th48
.= (g
. x) by
A6,
A8
.= ((g
| D)
. x) by
A8,
Th48;
end;
(
dom (f
| D))
= ((
dom f)
/\ D) by
RELAT_1: 61
.= D by
A1,
XBOOLE_1: 28;
hence thesis by
A3,
A7;
end;
theorem ::
FUNCT_1:96
for f,g be
Function, X be
set st (
dom f)
= (
dom g) & (for x be
set st x
in X holds (f
. x)
= (g
. x)) holds (f
| X)
= (g
| X)
proof
let f,g be
Function, X be
set such that
A1: (
dom f)
= (
dom g) and
A2: for x be
set st x
in X holds (f
. x)
= (g
. x);
A3: (
dom (f
| X))
= ((
dom f)
/\ X) by
RELAT_1: 61;
then
A4: (
dom (f
| X))
= (
dom (g
| X)) by
A1,
RELAT_1: 61;
now
let x be
object;
assume
A5: x
in (
dom (f
| X));
then
A6: x
in X by
A3,
XBOOLE_0:def 4;
((f
| X)
. x)
= (f
. x) & ((g
| X)
. x)
= (g
. x) by
A4,
A5,
Th46;
hence ((f
| X)
. x)
= ((g
| X)
. x) by
A2,
A6;
end;
hence thesis by
A4;
end;
theorem ::
FUNCT_1:97
Th96: (
rng (f
|
{X}))
c=
{(f
. X)}
proof
let x be
object;
assume x
in (
rng (f
|
{X}));
then
consider y be
object such that
A1: y
in (
dom (f
|
{X})) and
A2: x
= ((f
|
{X})
. y) by
Def3;
(
dom (f
|
{X}))
c=
{X} by
RELAT_1: 58;
then y
= X by
A1,
TARSKI:def 1;
then x
= (f
. X) by
A1,
A2,
Th46;
hence thesis by
TARSKI:def 1;
end;
theorem ::
FUNCT_1:98
X
in (
dom f) implies (
rng (f
|
{X}))
=
{(f
. X)}
proof
A1: X
in
{X} by
TARSKI:def 1;
assume X
in (
dom f);
then
A2: X
in (
dom (f
|
{X})) by
A1,
RELAT_1: 57;
thus (
rng (f
|
{X}))
c=
{(f
. X)} by
Th96;
let x be
object;
assume x
in
{(f
. X)};
then x
= (f
. X) by
TARSKI:def 1;
then x
= ((f
|
{X})
. X) by
A2,
Th46;
hence thesis by
A2,
Def3;
end;
registration
cluster
empty ->
constant for
Function;
coherence ;
end
registration
let f be
constant
Function;
cluster (
rng f) ->
trivial;
coherence
proof
per cases ;
suppose f is
empty;
then
reconsider g = f as
empty
Function;
(
rng g) is
empty;
hence thesis;
end;
suppose f
<>
{} ;
then
consider x be
object such that
A1: x
in (
dom f) by
XBOOLE_0:def 1;
for y be
object holds y
in
{(f
. x)} iff ex z be
object st z
in (
dom f) & y
= (f
. z)
proof
let y be
object;
hereby
assume
A2: y
in
{(f
. x)};
reconsider x as
object;
take x;
thus x
in (
dom f) & y
= (f
. x) by
A1,
A2,
TARSKI:def 1;
end;
given z be
object such that
A3: z
in (
dom f) & y
= (f
. z);
y
= (f
. x) by
A1,
A3,
Def10;
hence thesis by
TARSKI:def 1;
end;
hence thesis by
Def3;
end;
end;
end
registration
cluster non
constant for
Function;
existence
proof
set f =
{
[
{} ,
{} ],
[
{
{} },
{
{} }]};
f is
Function-like
proof
let x,y,z be
object;
assume that
A1:
[x, y]
in f and
A2:
[x, z]
in f;
[x, y]
=
[
{} ,
{} ] or
[x, y]
=
[
{
{} },
{
{} }] by
A1,
TARSKI:def 2;
then
A3: x
=
{} & y
=
{} or x
=
{
{} } & y
=
{
{} } by
XTUPLE_0: 1;
[x, z]
=
[
{} ,
{} ] or
[x, z]
=
[
{
{} },
{
{} }] by
A2,
TARSKI:def 2;
hence thesis by
A3,
XTUPLE_0: 1;
end;
then
reconsider f as
Function;
take f,
{} ,
{
{} };
A4:
[
{
{} },
{
{} }]
in f by
TARSKI:def 2;
A5:
[
{} ,
{} ]
in f by
TARSKI:def 2;
hence
A6:
{}
in (
dom f) &
{
{} }
in (
dom f) by
A4,
XTUPLE_0:def 12;
then (f
.
{} )
=
{} by
A5,
Def2;
hence thesis by
A4,
A6,
Def2;
end;
end
registration
let f be non
constant
Function;
cluster (
rng f) -> non
trivial;
coherence
proof
assume
A1: (
rng f) is
trivial;
per cases ;
suppose (
rng f) is
empty;
then
reconsider f as
empty
Function;
f is
trivial;
hence thesis;
end;
suppose (
rng f) is non
empty;
then
consider x be
object such that
A2: x
in (
rng f);
f is
constant
proof
let y,z be
object;
assume that
A3: y
in (
dom f) and
A4: z
in (
dom f);
A5: (f
. z)
in (
rng f) by
A4,
Def3;
(f
. y)
in (
rng f) by
A3,
Def3;
hence (f
. y)
= x by
A1,
A2
.= (f
. z) by
A1,
A2,
A5;
end;
hence thesis;
end;
end;
end
registration
cluster non
constant -> non
trivial for
Function;
coherence
proof
let f be
Function;
assume f is non
constant;
then
consider n1,n2 be
object such that
A1: n1
in (
dom f) and
A2: n2
in (
dom f) and
A3: (f
. n1)
<> (f
. n2);
reconsider f as non
empty
Function by
A1;
f is non
trivial
proof
reconsider x =
[n1, (f
. n1)], y =
[n2, (f
. n2)] as
Element of f by
A1,
A2,
Th1;
take x, y;
thus x
in f & y
in f;
thus thesis by
A3,
XTUPLE_0: 1;
end;
hence thesis;
end;
end
registration
cluster
trivial ->
constant for
Function;
coherence ;
end
theorem ::
FUNCT_1:99
for F,G be
Function, X holds ((G
| (F
.: X))
* (F
| X))
= ((G
* F)
| X)
proof
let F,G be
Function, X;
set Y = (
dom ((G
* F)
| X));
now
let x be
object;
thus x
in (
dom ((G
| (F
.: X))
* (F
| X))) implies x
in Y
proof
assume
A1: x
in (
dom ((G
| (F
.: X))
* (F
| X)));
then
A2: x
in (
dom (F
| X)) by
Th11;
then
A3: x
in ((
dom F)
/\ X) by
RELAT_1: 61;
then
A4: x
in X by
XBOOLE_0:def 4;
((F
| X)
. x)
in (
dom (G
| (F
.: X))) by
A1,
Th11;
then (F
. x)
in (
dom (G
| (F
.: X))) by
A2,
Th46;
then (F
. x)
in ((
dom G)
/\ (F
.: X)) by
RELAT_1: 61;
then
A5: (F
. x)
in (
dom G) by
XBOOLE_0:def 4;
x
in (
dom F) by
A3,
XBOOLE_0:def 4;
then x
in (
dom (G
* F)) by
A5,
Th11;
then x
in ((
dom (G
* F))
/\ X) by
A4,
XBOOLE_0:def 4;
hence thesis by
RELAT_1: 61;
end;
assume x
in Y;
then
A6: x
in ((
dom (G
* F))
/\ X) by
RELAT_1: 61;
then
A7: x
in (
dom (G
* F)) by
XBOOLE_0:def 4;
then
A8: (F
. x)
in (
dom G) by
Th11;
A9: x
in X by
A6,
XBOOLE_0:def 4;
x
in (
dom F) by
A7,
Th11;
then x
in ((
dom F)
/\ X) by
A9,
XBOOLE_0:def 4;
then
A10: x
in (
dom (F
| X)) by
RELAT_1: 61;
x
in (
dom F) by
A7,
Th11;
then (F
. x)
in (F
.: X) by
A9,
Def6;
then (F
. x)
in ((
dom G)
/\ (F
.: X)) by
A8,
XBOOLE_0:def 4;
then (F
. x)
in (
dom (G
| (F
.: X))) by
RELAT_1: 61;
then ((F
| X)
. x)
in (
dom (G
| (F
.: X))) by
A10,
Th46;
hence x
in (
dom ((G
| (F
.: X))
* (F
| X))) by
A10,
Th11;
end;
then
A11: Y
= (
dom ((G
| (F
.: X))
* (F
| X))) by
TARSKI: 2;
now
let x;
assume
A12: x
in Y;
then
A13: x
in ((
dom (G
* F))
/\ X) by
RELAT_1: 61;
then x
in (
dom (G
* F)) by
XBOOLE_0:def 4;
then
A14: x
in (
dom F) by
Th11;
A15: x
in X by
A13,
XBOOLE_0:def 4;
then
A16: (F
. x)
in (F
.: X) by
A14,
Def6;
thus (((G
| (F
.: X))
* (F
| X))
. x)
= ((G
| (F
.: X))
. ((F
| X)
. x)) by
A11,
A12,
Th12
.= ((G
| (F
.: X))
. (F
. x)) by
A15,
Th48
.= (G
. (F
. x)) by
A16,
Th48
.= ((G
* F)
. x) by
A14,
Th13
.= (((G
* F)
| X)
. x) by
A13,
Th47;
end;
hence thesis by
A11;
end;
theorem ::
FUNCT_1:100
for F,G be
Function, X, X1 holds ((G
| X1)
* (F
| X))
= ((G
* F)
| (X
/\ (F
" X1)))
proof
let F,G be
Function, X, X1;
set Y = (
dom ((G
| X1)
* (F
| X)));
now
let x be
object;
thus x
in (
dom ((G
* F)
| (X
/\ (F
" X1)))) implies x
in Y
proof
assume x
in (
dom ((G
* F)
| (X
/\ (F
" X1))));
then
A1: x
in ((
dom (G
* F))
/\ (X
/\ (F
" X1))) by
RELAT_1: 61;
then
A2: x
in (
dom (G
* F)) by
XBOOLE_0:def 4;
A3: x
in (X
/\ (F
" X1)) by
A1,
XBOOLE_0:def 4;
then
A4: x
in X by
XBOOLE_0:def 4;
x
in (
dom F) by
A2,
Th11;
then x
in ((
dom F)
/\ X) by
A4,
XBOOLE_0:def 4;
then
A5: x
in (
dom (F
| X)) by
RELAT_1: 61;
x
in (F
" X1) by
A3,
XBOOLE_0:def 4;
then
A6: (F
. x)
in X1 by
Def7;
(F
. x)
in (
dom G) by
A2,
Th11;
then (F
. x)
in ((
dom G)
/\ X1) by
A6,
XBOOLE_0:def 4;
then (F
. x)
in (
dom (G
| X1)) by
RELAT_1: 61;
then ((F
| X)
. x)
in (
dom (G
| X1)) by
A5,
Th46;
hence thesis by
A5,
Th11;
end;
assume
A7: x
in Y;
then
A8: x
in (
dom (F
| X)) by
Th11;
then
A9: x
in ((
dom F)
/\ X) by
RELAT_1: 61;
then
A10: x
in (
dom F) by
XBOOLE_0:def 4;
A11: x
in X by
A9,
XBOOLE_0:def 4;
((F
| X)
. x)
in (
dom (G
| X1)) by
A7,
Th11;
then (F
. x)
in (
dom (G
| X1)) by
A8,
Th46;
then
A12: (F
. x)
in ((
dom G)
/\ X1) by
RELAT_1: 61;
then (F
. x)
in X1 by
XBOOLE_0:def 4;
then x
in (F
" X1) by
A10,
Def7;
then
A13: x
in (X
/\ (F
" X1)) by
A11,
XBOOLE_0:def 4;
(F
. x)
in (
dom G) by
A12,
XBOOLE_0:def 4;
then x
in (
dom (G
* F)) by
A10,
Th11;
then x
in ((
dom (G
* F))
/\ (X
/\ (F
" X1))) by
A13,
XBOOLE_0:def 4;
hence x
in (
dom ((G
* F)
| (X
/\ (F
" X1)))) by
RELAT_1: 61;
end;
then
A14: Y
= (
dom ((G
* F)
| (X
/\ (F
" X1)))) by
TARSKI: 2;
now
let x;
assume
A15: x
in Y;
then
A16: x
in (
dom (F
| X)) by
Th11;
then
A17: x
in ((
dom F)
/\ X) by
RELAT_1: 61;
then
A18: x
in (
dom F) by
XBOOLE_0:def 4;
A19: ((F
| X)
. x)
in (
dom (G
| X1)) by
A15,
Th11;
then
A20: (F
. x)
in (
dom (G
| X1)) by
A16,
Th46;
A21: x
in X by
A17,
XBOOLE_0:def 4;
(F
. x)
in (
dom (G
| X1)) by
A16,
A19,
Th46;
then (F
. x)
in ((
dom G)
/\ X1) by
RELAT_1: 61;
then (F
. x)
in X1 by
XBOOLE_0:def 4;
then x
in (F
" X1) by
A18,
Def7;
then
A22: x
in (X
/\ (F
" X1)) by
A21,
XBOOLE_0:def 4;
thus (((G
| X1)
* (F
| X))
. x)
= ((G
| X1)
. ((F
| X)
. x)) by
A15,
Th12
.= ((G
| X1)
. (F
. x)) by
A16,
Th46
.= (G
. (F
. x)) by
A20,
Th46
.= ((G
* F)
. x) by
A18,
Th13
.= (((G
* F)
| (X
/\ (F
" X1)))
. x) by
A22,
Th48;
end;
hence thesis by
A14;
end;
theorem ::
FUNCT_1:101
for F,G be
Function, X holds X
c= (
dom (G
* F)) iff X
c= (
dom F) & (F
.: X)
c= (
dom G)
proof
let F,G be
Function, X;
thus X
c= (
dom (G
* F)) implies X
c= (
dom F) & (F
.: X)
c= (
dom G)
proof
assume
A1: X
c= (
dom (G
* F));
then for x be
object st x
in X holds x
in (
dom F) by
Th11;
hence X
c= (
dom F);
let x be
object;
assume x
in (F
.: X);
then ex y be
object st y
in (
dom F) & y
in X & x
= (F
. y) by
Def6;
hence thesis by
A1,
Th11;
end;
assume that
A2: X
c= (
dom F) and
A3: (F
.: X)
c= (
dom G);
let x be
object;
assume
A4: x
in X;
then (F
. x)
in (F
.: X) by
A2,
Def6;
hence thesis by
A2,
A3,
A4,
Th11;
end;
definition
let f be
Function;
assume
A1: f is non
empty
constant;
::
FUNCT_1:def12
func
the_value_of f ->
object means ex x be
set st x
in (
dom f) & it
= (f
. x);
existence
proof
consider x1 be
object such that
A2: x1
in (
dom f) by
A1,
XBOOLE_0:def 1;
take (f
. x1);
thus thesis by
A2;
end;
uniqueness by
A1;
end
registration
let X, Y;
cluster X
-definedY
-valued for
Function;
existence
proof
take
{} ;
thus (
dom
{} )
c= X & (
rng
{} )
c= Y;
end;
end
theorem ::
FUNCT_1:102
for X be
set, f be X
-valued
Function holds for x be
set st x
in (
dom f) holds (f
. x)
in X
proof
let X be
set, f be X
-valued
Function;
let x be
set;
assume x
in (
dom f);
then
A1: (f
. x)
in (
rng f) by
Def3;
(
rng f)
c= X by
RELAT_1:def 19;
hence thesis by
A1;
end;
definition
let IT be
set;
::
FUNCT_1:def13
attr IT is
functional means
:
Def13: for x be
object st x
in IT holds x is
Function;
end
registration
cluster
empty ->
functional for
set;
coherence ;
let f be
Function;
cluster
{f} ->
functional;
coherence by
TARSKI:def 1;
let g be
Function;
cluster
{f, g} ->
functional;
coherence by
TARSKI:def 2;
end
registration
cluster non
empty
functional for
set;
existence
proof
take
{
{} };
thus thesis;
end;
end
registration
let P be
functional
set;
cluster ->
Function-like
Relation-like for
Element of P;
coherence
proof
let x be
Element of P;
per cases ;
suppose P is
empty;
hence thesis by
SUBSET_1:def 1;
end;
suppose P is non
empty;
hence thesis by
Def13;
end;
end;
end
registration
let A be
functional
set;
cluster ->
functional for
Subset of A;
coherence ;
end
definition
let g,f be
Function;
::
FUNCT_1:def14
attr f is g
-compatible means
:
Def14: x
in (
dom f) implies (f
. x)
in (g
. x);
end
theorem ::
FUNCT_1:103
f is g
-compatible & (
dom f)
= (
dom g) implies g is
non-empty;
theorem ::
FUNCT_1:104
{} is f
-compatible;
registration
let I be
set, f be
Function;
cluster
emptyI
-definedf
-compatible for
Function;
existence
proof
take
{} ;
thus thesis by
RELAT_1: 171;
end;
end
registration
let X be
set;
let f be
Function, g be f
-compatible
Function;
cluster (g
| X) -> f
-compatible;
coherence
proof
let x;
A1: (
dom (g
| X))
c= (
dom g) by
RELAT_1: 60;
assume
A2: x
in (
dom (g
| X));
then (g
. x)
in (f
. x) by
A1,
Def14;
hence ((g
| X)
. x)
in (f
. x) by
A2,
Th46;
end;
end
registration
let I be
set;
cluster
non-emptyI
-defined for
Function;
existence
proof
take
{} ;
thus
{} is
non-empty;
thus (
dom
{} )
c= I;
end;
end
theorem ::
FUNCT_1:105
Th104: for g be f
-compatible
Function holds (
dom g)
c= (
dom f)
proof
let g be f
-compatible
Function;
let x be
object;
assume x
in (
dom g);
then (g
. x)
in (f
. x) by
Def14;
hence x
in (
dom f) by
Def2;
end;
registration
let X;
let f be X
-defined
Function;
cluster f
-compatible -> X
-defined for
Function;
coherence
proof
let g be
Function;
assume g is f
-compatible;
then
A1: (
dom g)
c= (
dom f) by
Th104;
(
dom f)
c= X by
RELAT_1:def 18;
hence (
dom g)
c= X by
A1;
end;
end
theorem ::
FUNCT_1:106
for f be X
-valued
Function st x
in (
dom f) holds (f
. x) is
Element of X
proof
let f be X
-valued
Function;
assume x
in (
dom f);
then
A1: (f
. x)
in (
rng f) by
Def3;
(
rng f)
c= X by
RELAT_1:def 19;
hence (f
. x) is
Element of X by
A1;
end;
theorem ::
FUNCT_1:107
for f be
Function, A be
set st f is
one-to-one & A
c= (
dom f) holds ((f
" )
.: (f
.: A))
= A
proof
let f be
Function, A be
set;
set B = (f
.: A);
assume that
A1: f is
one-to-one and
A2: A
c= (
dom f);
A3: ((f
" )
.: B)
c= A
proof
let y be
object;
assume y
in ((f
" )
.: B);
then
consider x be
object such that x
in (
dom (f
" )) and
A4: x
in B and
A5: y
= ((f
" )
. x) by
Def6;
ex y2 be
object st (y2
in (
dom f)) & (y2
in A) & (x
= (f
. y2)) by
A4,
Def6;
hence thesis by
A1,
A5,
Th31;
end;
A
c= ((f
" )
.: B)
proof
let x be
object;
assume
A6: x
in A;
set y0 = (f
. x);
A7: ((f
" )
. y0)
= x by
A1,
A2,
A6,
Th33;
y0
in (
rng f) by
A2,
A6,
Def3;
then
A8: y0
in (
dom (f
" )) by
A1,
Th32;
y0
in B by
A2,
A6,
Def6;
hence thesis by
A7,
A8,
Def6;
end;
hence thesis by
A3;
end;
registration
let A be
functional
set, x be
object;
let F be A
-valued
Function;
cluster (F
. x) ->
Function-like
Relation-like;
coherence
proof
per cases ;
suppose x
in (
dom F);
then
A1: (F
. x)
in (
rng F) by
Def3;
(
rng F)
c= A by
RELAT_1:def 19;
hence thesis by
A1;
end;
suppose not x
in (
dom F);
hence thesis by
Def2;
end;
end;
end
theorem ::
FUNCT_1:108
Th107: x
in X & x
in (
dom f) implies (f
. x)
in (f
.: X)
proof
assume that
A1: x
in X and
A2: x
in (
dom f);
x
in (X
/\ (
dom f)) by
A1,
A2,
XBOOLE_0:def 4;
then x
in (
dom (f
| X)) by
RELAT_1: 61;
then
A3: ((f
| X)
. x)
in (
rng (f
| X)) by
Def3;
((f
| X)
. x)
= (f
. x) by
A1,
Th48;
hence (f
. x)
in (f
.: X) by
A3,
RELAT_1: 115;
end;
theorem ::
FUNCT_1:109
X
<>
{} & X
c= (
dom f) implies (f
.: X)
<>
{}
proof
assume X
<>
{} ;
then ex x be
object st x
in X by
XBOOLE_0:def 1;
hence thesis by
Th107;
end;
registration
let f be non
trivial
Function;
cluster (
dom f) -> non
trivial;
coherence
proof
consider u,w be
object such that
A1: u
in f and
A2: w
in f and
A3: u
<> w by
ZFMISC_1:def 10;
consider u1,u2 be
object such that
A4: u
=
[u1, u2] by
A1,
RELAT_1:def 1;
consider w1,w2 be
object such that
A5: w
=
[w1, w2] by
A2,
RELAT_1:def 1;
take u1, w1;
thus u1
in (
dom f) & w1
in (
dom f) by
A4,
A5,
A1,
A2,
XTUPLE_0:def 12;
thus u1
<> w1 by
A1,
A2,
A3,
A4,
A5,
Def1;
end;
end
theorem ::
FUNCT_1:110
for B be non
empty
functional
set, f be
Function st f
= (
union B) holds (
dom f)
= (
union the set of all (
dom g) where g be
Element of B) & (
rng f)
= (
union the set of all (
rng g) where g be
Element of B)
proof
let B be non
empty
functional
set, f be
Function such that
A1: f
= (
union B);
set X = the set of all (
dom g) where g be
Element of B;
now
let x be
object;
hereby
assume x
in (
dom f);
then
[x, (f
. x)]
in f by
Th1;
then
consider g be
set such that
A2:
[x, (f
. x)]
in g and
A3: g
in B by
A1,
TARSKI:def 4;
reconsider g as
Function by
A3;
take Z = (
dom g);
thus x
in Z & Z
in X by
A2,
A3,
Th1;
end;
given Z be
set such that
A4: x
in Z and
A5: Z
in X;
consider g be
Element of B such that
A6: Z
= (
dom g) by
A5;
[x, (g
. x)]
in g by
A4,
A6,
Th1;
then
[x, (g
. x)]
in f by
A1,
TARSKI:def 4;
hence x
in (
dom f) by
Th1;
end;
hence (
dom f)
= (
union X) by
TARSKI:def 4;
set X = the set of all (
rng g) where g be
Element of B;
now
let y be
object;
hereby
assume y
in (
rng f);
then
consider x be
object such that
A7: x
in (
dom f) & y
= (f
. x) by
Def3;
[x, y]
in f by
A7,
Th1;
then
consider g be
set such that
A8:
[x, y]
in g and
A9: g
in B by
A1,
TARSKI:def 4;
reconsider g as
Function by
A9;
take Z = (
rng g);
x
in (
dom g) & y
= (g
. x) by
A8,
Th1;
hence y
in Z & Z
in X by
A9,
Def3;
end;
given Z be
set such that
A10: y
in Z and
A11: Z
in X;
consider g be
Element of B such that
A12: Z
= (
rng g) by
A11;
consider x be
object such that
A13: x
in (
dom g) & y
= (g
. x) by
A10,
A12,
Def3;
[x, y]
in g by
A13,
Th1;
then
[x, y]
in f by
A1,
TARSKI:def 4;
hence y
in (
rng f) by
XTUPLE_0:def 13;
end;
hence thesis by
TARSKI:def 4;
end;
scheme ::
FUNCT_1:sch5
LambdaS { A() ->
set , F(
object) ->
object } :
ex f be
Function st (
dom f)
= A() & for X st X
in A() holds (f
. X)
= F(X);
defpred
P[
object,
object] means $2
= F($1);
A1: for x st x
in A() holds ex y st
P[x, y];
A2: for x, y1, y2 st x
in A() &
P[x, y1] &
P[x, y2] holds y1
= y2;
consider f be
Function such that
A3: (
dom f)
= A() and
A4: for x st x
in A() holds
P[x, (f
. x)] from
FuncEx(
A2,
A1);
take f;
thus (
dom f)
= A() by
A3;
thus thesis by
A4;
end;
theorem ::
FUNCT_1:111
Th110: for M be
set st for X st X
in M holds X
<>
{} holds ex f be
Function st (
dom f)
= M & for X st X
in M holds (f
. X)
in X
proof
let M be
set;
assume
A1: for X st X
in M holds X
<>
{} ;
deffunc
F(
set) = the
Element of $1;
consider f be
Function such that
A2: (
dom f)
= M and
A3: for X st X
in M holds (f
. X)
=
F(X) from
LambdaS;
take f;
thus (
dom f)
= M by
A2;
let X;
assume
A4: X
in M;
then
A5: (f
. X)
= the
Element of X by
A3;
X
<>
{} by
A1,
A4;
hence (f
. X)
in X by
A5;
end;
scheme ::
FUNCT_1:sch6
NonUniqBoundFuncEx { X() ->
set , Y() ->
set , P[
object,
object] } :
ex f be
Function st (
dom f)
= X() & (
rng f)
c= Y() & for x be
object st x
in X() holds P[x, (f
. x)]
provided
A1: for x be
object st x
in X() holds ex y be
object st y
in Y() & P[x, y];
per cases ;
suppose
A2: X()
=
{} ;
take
{} ;
thus thesis by
A2;
end;
suppose
A3: X()
<>
{} ;
defpred
Q[
object,
object] means ex D2 be
set st D2
= $2 & for y holds y
in D2 iff y
in Y() & P[$1, y];
A4: for e,u1,u2 be
object st e
in X() &
Q[e, u1] &
Q[e, u2] holds u1
= u2
proof
let e,u1,u2 be
object such that e
in X();
given U1 be
set such that
A5: U1
= u1 and
A6: for y holds y
in U1 iff y
in Y() & P[e, y];
defpred
A[
object] means $1
in Y() & P[e, $1];
A7: for x be
object holds x
in U1 iff
A[x] by
A6;
given U2 be
set such that
A8: U2
= u2 and
A9: for y holds y
in U2 iff y
in Y() & P[e, y];
A10: for x be
object holds x
in U2 iff
A[x] by
A9;
U1
= U2 from
XBOOLE_0:sch 2(
A7,
A10);
hence thesis by
A5,
A8;
end;
A11: for x st x
in X() holds ex y st
Q[x, y]
proof
let x such that x
in X();
defpred
R[
object] means P[x, $1];
consider X such that
A12: for y be
object holds y
in X iff y
in Y() &
R[y] from
XBOOLE_0:sch 1;
take X;
thus thesis by
A12;
end;
consider G be
Function such that
A13: (
dom G)
= X() & for x st x
in X() holds
Q[x, (G
. x)] from
FuncEx(
A4,
A11);
reconsider D = (
rng G) as non
empty
set by
A13,
A3,
RELAT_1: 42;
now
let X;
assume X
in D;
then
consider x be
object such that
A14: x
in (
dom G) & X
= (G
. x) by
Def3;
consider y be
object such that
A15: y
in Y() & P[x, y] by
A1,
A13,
A14;
Q[x, (G
. x)] by
A13,
A14;
then y
in X by
A15,
A14;
hence X
<>
{} ;
end;
then
consider F be
Function such that
A16: (
dom F)
= D and
A17: for X st X
in D holds (F
. X)
in X by
Th110;
A18: (
dom (F
* G))
= X() by
A13,
A16,
RELAT_1: 27;
take f = (F
* G);
thus (
dom f)
= X() by
A13,
A16,
RELAT_1: 27;
(
rng F)
c= Y()
proof
let x be
object;
assume x
in (
rng F);
then
consider y be
object such that
A19: y
in (
dom F) and
A20: x
= (F
. y) by
Def3;
consider z be
object such that
A21: z
in (
dom G) & y
= (G
. z) by
A16,
A19,
Def3;
reconsider y as
set by
TARSKI: 1;
A22: x
in y by
A16,
A17,
A19,
A20;
Q[z, (G
. z)] by
A13,
A21;
hence thesis by
A21,
A22;
end;
hence (
rng f)
c= Y() by
A16,
RELAT_1: 28;
let x be
object;
assume
A23: x
in X();
then (f
. x)
= (F
. (G
. x)) & (G
. x)
in D by
A13,
A18,
Th12,
Def3;
then
A24: (f
. x)
in (G
. x) by
A17;
Q[x, (G
. x)] by
A13,
A23;
hence thesis by
A24;
end;
end;
registration
let f be
empty-yielding
Function;
let x;
cluster (f
. x) ->
empty;
coherence
proof
x
in (
dom f) or not x
in (
dom f);
hence thesis by
Def2,
Def8;
end;
end
theorem ::
FUNCT_1:112
for f,g,h be
Function st f
c= h & g
c= h & f
misses g holds (
dom f)
misses (
dom g)
proof
let f,g,h be
Function such that
A1: f
c= h and
A2: g
c= h and
A3: f
misses g;
for x be
object st x
in (
dom f) holds not x
in (
dom g)
proof
let x be
object;
assume x
in (
dom f);
then
A4:
[x, (f
. x)]
in f by
Def2;
now
assume x
in (
dom g);
then
A5:
[x, (g
. x)]
in g by
Def2;
then (f
. x)
= (g
. x) by
A1,
A2,
A4,
Def1;
hence contradiction by
A3,
A4,
A5,
XBOOLE_0: 3;
end;
hence thesis;
end;
hence thesis by
XBOOLE_0: 3;
end;
theorem ::
FUNCT_1:113
for Y be
set, f be
Function holds (Y
|` f)
= (f
| (f
" Y))
proof
let Y be
set, f be
Function;
A1: (Y
|` f)
c= (f
| (f
" Y)) by
RELAT_1: 188;
(f
| (f
" Y))
c= (Y
|` f)
proof
let x,y be
object;
assume
A2:
[x, y]
in (f
| (f
" Y));
then
A3: x
in (f
" Y) by
RELAT_1:def 11;
A4:
[x, y]
in f by
A2,
RELAT_1:def 11;
(f
. x)
in Y by
A3,
Def7;
then y
in Y by
A4,
Th1;
hence thesis by
A4,
RELAT_1:def 12;
end;
hence thesis by
A1;
end;
registration
let X be
set;
let x be
Element of X;
reduce ((
id X)
. x) to x;
reducibility
proof
per cases ;
suppose
A1: X is
empty;
then x is
empty by
SUBSET_1:def 1;
hence thesis by
A1;
end;
suppose X is non
empty;
hence thesis by
Th18;
end;
end;
end
theorem ::
FUNCT_1:114
(
rng f)
c= (
rng g) implies for x be
object st x
in (
dom f) holds ex y be
object st y
in (
dom g) & (f
. x)
= (g
. y)
proof
assume that
A1: (
rng f)
c= (
rng g);
let x be
object;
assume x
in (
dom f);
then (f
. x)
in (
rng f) by
Def3;
then
A2: (f
. x)
in (
rng g) by
A1;
ex y be
object st y
in (
dom g) & (f
. x)
= (g
. y) by
Def3,
A2;
hence thesis;
end;