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
;
(card Y) - (card X) = card Y
by A5;
then A8:
((card Y) -' (card X)) ! = (card Y) !
by XREAL_0:def 2;
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:2;
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:33;
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:30;
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
object such that A10:
x in X
;
reconsider x =
x as
set by TARSKI:1;
A11:
x in X
by A10;
defpred S2[
Function]
means $1 is
one-to-one ;
card Y,
Y are_equipotent
by CARD_1:def 2;
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:1;
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 6(A16, A15, A11);
A20:
for
k being
Nat st
k in dom F holds
F . k = (n !) / (((card Y) -' (card X)) !)
proof
card X > 0
by A11;
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 A11, ZFMISC_1:116;
A23:
(cX1 + 1) - 1
<= (n + 1) - 1
by A3, A4, XREAL_1:9;
then A24:
n - cX1 >= cX1 - cX1
by XREAL_1:9;
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 3;
set Yy =
Y \ {(f . k)};
A27:
Y = (Y \ {(f . k)}) \/ {(f . k)}
by A26, ZFMISC_1:116;
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 A11, STIRL2_1:55;
A30:
card (Y \ {(f . k)}) = n
by A3, A26, STIRL2_1:55;
then A31:
(
Y \ {(f . k)} is
empty implies
X \ {x} is
empty )
by A23, A29;
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:9;
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, Th4;
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:60;
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:59;
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:74
.=
((card Y) !) / (((card Y) -' (card X)) !)
by A3, NEWTON:15
;
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:12, 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:1;
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:33;
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:30, NEWTON:12;
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