let X, Y be finite set ; ( card X <= card Y implies card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! ) )
defpred S1[ Nat] means for X, Y being finite set st card Y = $1 & card X <= card Y holds
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! );
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
let X,
Y be
finite set ;
( card Y = n + 1 & card X <= card Y implies card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! ) )
assume that A3:
card Y = n + 1
and A4:
card X <= card Y
;
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! )
per cases
( X is empty or not X is empty )
;
suppose A5:
X is
empty
;
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! )set F1 =
{ F where F is Function of X,Y : F is one-to-one } ;
A6:
{ F where F is Function of X,Y : F is one-to-one } c= {{} }
A7:
rng {} c= Y
by XBOOLE_1:2;
(card Y) - (card X) = card Y
by A5, CARD_1:47;
then A8:
((card Y) -' (card X)) ! = (card Y) !
by XREAL_0:def 2;
(card Y) ! > 0
by NEWTON:23;
then A9:
((card Y) ! ) / (((card Y) -' (card X)) ! ) = 1
by A8, XCMPLX_1:60;
dom {} = X
by A5;
then
{} is
Function of
X,
Y
by A7, FUNCT_2:4;
then
{} in { F where F is Function of X,Y : F is one-to-one }
;
then
{ F where F is Function of X,Y : F is one-to-one } = {{} }
by A6, ZFMISC_1:39;
hence
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! )
by A9, CARD_1:50;
verum end; suppose
not
X is
empty
;
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! )then consider x being
set such that A10:
x in X
by XBOOLE_0:def 1;
defpred S2[
Function]
means $1 is
one-to-one ;
card Y,
Y are_equipotent
by CARD_1:def 5;
then consider f being
Function such that A12:
f is
one-to-one
and A13:
dom f = card Y
and A14:
rng f = Y
by WELLORD2:def 4;
reconsider f =
f as
Function of
(card Y),
Y by A13, A14, FUNCT_2:3;
A15:
not
Y is
empty
by A3;
A16:
(
f is
onto &
f is
one-to-one )
by A12, A14, FUNCT_2:def 3;
consider F being
XFinSequence of
NAT such that A17:
dom F = card Y
and A18:
card { g where g is Function of X,Y : S2[g] } = Sum F
and A19:
for
k being
Nat st
k in dom F holds
F . k = card { g where g is Function of X,Y : ( S2[g] & g . x = f . k ) }
from STIRL2_1:sch 7(A16, A15, A10);
A20:
for
k being
Nat st
k in dom F holds
F . k = (n ! ) / (((card Y) -' (card X)) ! )
proof
card X > 0
by A10;
then reconsider cX1 =
(card X) - 1 as
Element of
NAT by NAT_1:20;
set Xx =
X \ {x};
x in {x}
by TARSKI:def 1;
then A21:
not
x in X \ {x}
by XBOOLE_0:def 5;
A22:
X = (X \ {x}) \/ {x}
by A10, ZFMISC_1:140;
A23:
(cX1 + 1) - 1
<= (n + 1) - 1
by A3, A4, XREAL_1:11;
then A24:
n - cX1 >= cX1 - cX1
by XREAL_1:11;
let k be
Nat;
( k in dom F implies F . k = (n ! ) / (((card Y) -' (card X)) ! ) )
assume A25:
k in dom F
;
F . k = (n ! ) / (((card Y) -' (card X)) ! )
A26:
f . k in Y
by A13, A14, A17, A25, FUNCT_1:def 5;
set Yy =
Y \ {(f . k)};
A27:
Y = (Y \ {(f . k)}) \/ {(f . k)}
by A26, ZFMISC_1:140;
f . k in {(f . k)}
by TARSKI:def 1;
then A28:
not
f . k in Y \ {(f . k)}
by XBOOLE_0:def 5;
cX1 + 1
<= n + 1
by A3, A4;
then A29:
card (X \ {x}) = cX1
by A10, STIRL2_1:65;
A30:
card (Y \ {(f . k)}) = n
by A3, A26, STIRL2_1:65;
then A31:
(
Y \ {(f . k)} is
empty implies
X \ {x} is
empty )
by A23, A29, CARD_1:47;
A32:
card { g where g is Function of (X \ {x}),(Y \ {(f . k)}) : g is one-to-one } = (n ! ) / (((card (Y \ {(f . k)})) -' (card (X \ {x}))) ! )
by A2, A23, A29, A30;
(card Y) - (card X) >= (card X) - (card X)
by A4, XREAL_1:11;
then (card Y) -' (card X) =
(((card (Y \ {(f . k)})) + 1) - 1) - (((card (X \ {x})) + 1) - 1)
by A3, A29, A30, XREAL_0:def 2
.=
(card (Y \ {(f . k)})) -' (card (X \ {x}))
by A29, A30, A24, XREAL_0:def 2
;
then
card { g where g is Function of X,Y : ( g is one-to-one & g . x = f . k ) } = (n ! ) / (((card Y) -' (card X)) ! )
by A32, A27, A22, A28, A21, A31, Th5;
hence
F . k = (n ! ) / (((card Y) -' (card X)) ! )
by A19, A25;
verum
end; then
for
k being
Nat st
k in dom F holds
F . k >= (n ! ) / (((card Y) -' (card X)) ! )
;
then A33:
Sum F >= (len F) * ((n ! ) / (((card Y) -' (card X)) ! ))
by AFINSQ_2:72;
for
k being
Nat st
k in dom F holds
F . k <= (n ! ) / (((card Y) -' (card X)) ! )
by A20;
then
Sum F <= (len F) * ((n ! ) / (((card Y) -' (card X)) ! ))
by AFINSQ_2:71;
then Sum F =
(n + 1) * ((n ! ) / (((card Y) -' (card X)) ! ))
by A3, A17, A33, XXREAL_0:1
.=
((n + 1) * (n ! )) / (((card Y) -' (card X)) ! )
by XCMPLX_1:75
.=
((card Y) ! ) / (((card Y) -' (card X)) ! )
by A3, NEWTON:21
;
hence
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! )
by A18;
verum end;
end;
A34:
S1[ 0 ]
proof
let X,
Y be
finite set ;
( card Y = 0 & card X <= card Y implies card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! ) )
assume that A35:
card Y = 0
and A36:
card X <= card Y
;
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! )
(card Y) - (card X) = 0
by A35, A36;
then A37:
((card Y) -' (card X)) ! = 1
by NEWTON:18, XREAL_0:def 2;
set F1 =
{ F where F is Function of X,Y : F is one-to-one } ;
A38:
{ F where F is Function of X,Y : F is one-to-one } c= {{} }
(
dom {} = X &
rng {} = Y )
by A35, A36;
then
{} is
Function of
X,
Y
by FUNCT_2:3;
then
{} in { F where F is Function of X,Y : F is one-to-one }
;
then
{ F where F is Function of X,Y : F is one-to-one } = {{} }
by A38, ZFMISC_1:39;
hence
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! )
by A35, A37, CARD_1:50, NEWTON:18;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A34, A1);
hence
( card X <= card Y implies card { F where F is Function of X,Y : F is one-to-one } = ((card Y) ! ) / (((card Y) -' (card X)) ! ) )
; verum