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 and
A3: 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 );
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:52; :: 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: verum
proof
( (X \/ {x}) /\ X = X & dom f = X \/ {x} ) by FUNCT_2:def 1, XBOOLE_1:21;
then A6: dom (f | X) = X by RELAT_1:61;
assume that
A7: f | X is one-to-one and
A8: rng ((f | X) | X) c= Y ; :: thesis: S1[f,X \/ {x},Y \/ {y}]
rng (f | X) c= Y by A8;
then f | X is Function of X,Y by A6, FUNCT_2:2;
hence S1[f,X \/ {x},Y \/ {y}] by A1, A3, A5, A7, A8, STIRL2_1:58; :: thesis: verum
end;
end;
set F3 = { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) } ;
A9: { 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 object ; :: 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 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 ) }
then consider F being Function of (X \/ {x}),(Y \/ {y}) such that
A10: z = F and
A11: ( F is one-to-one & F . x = y ) ;
rng (F | X) c= Y
proof
A12: dom F = X \/ {x} by FUNCT_2:def 1;
x in {x} by TARSKI:def 1;
then A13: x in dom F by A12, XBOOLE_0:def 3;
assume not rng (F | X) c= Y ; :: thesis: contradiction
then consider fz being object such that
A14: fz in rng (F | X) and
A15: not fz in Y ;
consider z being object such that
A16: z in dom (F | X) and
A17: fz = (F | X) . z by A14, FUNCT_1:def 3;
A18: z in dom F by A16, RELAT_1:57;
A19: ( fz in Y or fz in {y} ) by A14, XBOOLE_0:def 3;
A20: z in X by A16;
F . z = (F | X) . z by A16, FUNCT_1:47;
then y = F . z by A15, A17, A19, TARSKI:def 1;
hence contradiction by A2, A11, A13, A20, A18; :: 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 A10, A11; :: thesis: verum
end;
A21: { 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 object ; :: 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 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 ) }
then 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 ) ;
hence z in { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) } ; :: thesis: verum
end;
set F2 = { f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) } ;
set F1 = { F where F is Function of X,Y : F is one-to-one } ;
A22: { 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 ) }
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { F where F is Function of X,Y : F is one-to-one } or z in { f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) } )
assume z in { F where F is Function of X,Y : F is one-to-one } ; :: thesis: z in { f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) }
then consider F being Function of X,Y such that
A23: ( z = F & F is one-to-one ) ;
rng (F | X) c= rng F ;
hence z in { f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) } by A23; :: thesis: verum
end;
A24: not x in X by A2;
A25: 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, A24, A4);
 { 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 }
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) } or z in { F where F is Function of X,Y : F is one-to-one } )
assume z in { f where f is Function of X,Y : ( f is one-to-one & rng (f | X) c= Y ) } ; :: thesis: z in { F where F is Function of X,Y : F is one-to-one }
then ex f being Function of X,Y st
( z = f & f is one-to-one & rng (f | X) c= Y ) ;
hence z in { F where F is Function of X,Y : F is one-to-one } ; :: thesis: verum
end;
then { 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 A22;
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 A9, A21, A25, XBOOLE_0:def 10; :: thesis: verum