let X, Y be finite set ; :: thesis: for x, y being set st ( Y is empty implies X is empty ) & not x in X & not y in Y holds
card { F where F is Function of X,Y : F is one-to-one } = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }
let x, y be set ; :: thesis: ( ( Y is empty implies X is empty ) & not x in X & not y in Y implies card { F where F is Function of X,Y : F is one-to-one } = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) } )
assume that
A1:
( Y is empty implies X is empty )
and
A2:
( not x in X & not y in Y )
; :: thesis: card { F where F is Function of X,Y : F is one-to-one } = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }
defpred S1[ Function, set , set ] means ( $1 is one-to-one & rng ($1 | X) c= Y );
A3:
not x in X
by A2;
A4:
for f being Function of (X \/ {x}),(Y \/ {y}) st f . x = y holds
( S1[f,X \/ {x},Y \/ {y}] iff S1[f | X,X,Y] )
proof
let f be
Function of
(X \/ {x}),
(Y \/ {y});
:: thesis: ( f . x = y implies ( S1[f,X \/ {x},Y \/ {y}] iff S1[f | X,X,Y] ) )
assume A5:
f . x = y
;
:: thesis: ( S1[f,X \/ {x},Y \/ {y}] iff S1[f | X,X,Y] )
thus
(
S1[
f,
X \/ {x},
Y \/ {y}] implies
S1[
f | X,
X,
Y] )
by FUNCT_1:84, RELAT_1:101;
:: thesis: ( S1[f | X,X,Y] implies S1[f,X \/ {x},Y \/ {y}] )
thus
(
S1[
f | X,
X,
Y] implies
S1[
f,
X \/ {x},
Y \/ {y}] )
:: thesis: verumproof
assume A6:
(
f | X is
one-to-one &
rng ((f | X) | X) c= Y )
;
:: thesis: S1[f,X \/ {x},Y \/ {y}]
(
(X \/ {x}) /\ X = X &
dom f = X \/ {x} )
by FUNCT_2:def 1, XBOOLE_1:21;
then
(
dom (f | X) = X &
rng (f | X) c= Y )
by A6, RELAT_1:90, RELAT_1:101;
then
(
f | X is
Function of
X,
Y &
rng (f | X) c= Y )
by FUNCT_2:4;
hence
S1[
f,
X \/ {x},
Y \/ {y}]
by A1, A2, A5, A6, STIRL2_1:68;
:: thesis: verum
end;
end;
set F1 = { F where F is Function of X,Y : F is one-to-one } ;
set F2 = { f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) } ;
A7:
{ F where F is Function of X,Y : F is one-to-one } c= { f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) }
{ f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) } c= { F where F is Function of X,Y : F is one-to-one }
then A11:
{ f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) } = { F where F is Function of X,Y : F is one-to-one }
by A7, XBOOLE_0:def 10;
set F3 = { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) } ;
A12:
{ F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) } c= { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) }
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) } or z in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } )
assume A13:
z in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }
;
:: thesis: z in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) }
consider F being
Function of
(X \/ {x}),
(Y \/ {y}) such that A14:
(
z = F &
F is
one-to-one &
F . x = y )
by A13;
rng (F | X) c= Y
proof
assume
not
rng (F | X) c= Y
;
:: thesis: contradiction
then consider fz being
set such that A15:
(
fz in rng (F | X) & not
fz in Y )
by TARSKI:def 3;
consider z being
set such that A16:
(
z in dom (F | X) &
fz = (F | X) . z )
by A15, FUNCT_1:def 5;
rng (F | X) c= rng F
by RELAT_1:99;
then
(
fz in rng F &
x in {x} )
by A15, TARSKI:def 1;
then
( (
fz in Y or
fz in {y} ) &
x in X \/ {x} &
dom F = X \/ {x} &
dom (F | X) = (dom F) /\ X &
F . z = (F | X) . z )
by A16, FUNCT_1:70, FUNCT_2:def 1, RELAT_1:90, XBOOLE_0:def 3;
then
(
fz = y &
y = F . z &
z in dom F &
x in dom F &
z in X )
by A15, A16, TARSKI:def 1, XBOOLE_0:def 4;
hence
contradiction
by A2, A14, FUNCT_1:def 8;
:: thesis: verum
end;
hence
z in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) }
by A14;
:: thesis: verum
end;
A17:
{ f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } c= { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) } or z in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) } )
assume A18:
z in { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) }
;
:: thesis: z in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }
ex
f being
Function of
(X \/ {x}),
(Y \/ {y}) st
(
z = f &
S1[
f,
X \/ {x},
Y \/ {y}] &
rng (f | X) c= Y &
f . x = y )
by A18;
hence
z in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }
;
:: thesis: verum
end;
card { f where f is Function of X,Y : S1[f,X,Y] } = card { f where f is Function of (X \/ {x}),(Y \/ {y}) : ( S1[f,X \/ {x},Y \/ {y}] & rng (f | X) c= Y & f . x = y ) }
from STIRL2_1:sch 4(A1, A3, A4);
hence
card { F where F is Function of X,Y : F is one-to-one } = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }
by A11, A12, A17, XBOOLE_0:def 10; :: thesis: verum