let X be finite set ; for k being Nat
for z, x, y being object st not z in X holds
card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
let k be Nat; for z, x, y being object st not z in X holds
card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
let z, x, y be object ; ( not z in X implies card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } )
set F1 = { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } ;
defpred S1[ set , set , set ] means for f being Function st f = $1 holds
card ((f | X) " {x}) = k;
A1:
for f being Function of (X \/ {z}),({x,y} \/ {x}) st f . z = x holds
( S1[f,X \/ {z},{x,y} \/ {x}] iff S1[f | X,X,{x,y}] )
proof
let f be
Function of
(X \/ {z}),
({x,y} \/ {x});
( f . z = x implies ( S1[f,X \/ {z},{x,y} \/ {x}] iff S1[f | X,X,{x,y}] ) )
assume
f . z = x
;
( S1[f,X \/ {z},{x,y} \/ {x}] iff S1[f | X,X,{x,y}] )
f | X = (f | X) | X
;
hence
(
S1[
f,
X \/ {z},
{x,y} \/ {x}] iff
S1[
f | X,
X,
{x,y}] )
;
verum
end;
set F3 = { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } ;
set F2 = { f where f is Function of X,{x,y} : S1[f,X,{x,y}] } ;
assume A2:
not z in X
; card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
A3:
{ f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } c= { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
proof
{x} \/ {x,y} = {x,x,y}
by ENUMSET1:2;
then A4:
{x,y} \/ {x} = {x,y}
by ENUMSET1:30;
z in {z}
by TARSKI:def 1;
then A5:
z in X \/ {z}
by XBOOLE_0:def 3;
let x1 be
object ;
TARSKI:def 3 ( not x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } or x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } )
assume
x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) }
;
x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
then consider f being
Function of
(X \/ {z}),
({x,y} \/ {x}) such that A6:
x1 = f
and A7:
S1[
f,
X \/ {z},
{x,y} \/ {x}]
and
rng (f | X) c= {x,y}
and A8:
f . z = x
;
(
dom f = X \/ {z} &
(X \/ {z}) \ {z} = X )
by A2, FUNCT_2:def 1, ZFMISC_1:117;
then A9:
{z} \/ ((f | X) " {x}) = f " {x}
by A8, A5, AFINSQ_2:66;
not
z in (dom f) /\ X
by A2, XBOOLE_0:def 4;
then
not
z in dom (f | X)
by RELAT_1:61;
then A10:
not
z in (f | X) " {x}
by FUNCT_1:def 7;
card ((f | X) " {x}) = k
by A7;
then
card (f " {x}) = k + 1
by A9, A10, CARD_2:41;
hence
x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
by A6, A8, A4;
verum
end;
A11:
{ f where f is Function of X,{x,y} : S1[f,X,{x,y}] } c= Choose (X,k,x,y)
proof
let x1 be
object ;
TARSKI:def 3 ( not x1 in { f where f is Function of X,{x,y} : S1[f,X,{x,y}] } or x1 in Choose (X,k,x,y) )
assume
x1 in { f where f is Function of X,{x,y} : S1[f,X,{x,y}] }
;
x1 in Choose (X,k,x,y)
then consider f being
Function of
X,
{x,y} such that A12:
x1 = f
and A13:
S1[
f,
X,
{x,y}]
;
f | X = f
;
then
card (f " {x}) = k
by A13;
hence
x1 in Choose (
X,
k,
x,
y)
by A12, Def1;
verum
end;
A14:
Choose (X,k,x,y) c= { f where f is Function of X,{x,y} : S1[f,X,{x,y}] }
proof
let x1 be
object ;
TARSKI:def 3 ( not x1 in Choose (X,k,x,y) or x1 in { f where f is Function of X,{x,y} : S1[f,X,{x,y}] } )
assume
x1 in Choose (
X,
k,
x,
y)
;
x1 in { f where f is Function of X,{x,y} : S1[f,X,{x,y}] }
then consider f being
Function of
X,
{x,y} such that A15:
x1 = f
and A16:
card (f " {x}) = k
by Def1;
S1[
f,
X,
{x,y}]
by A16;
hence
x1 in { f where f is Function of X,{x,y} : S1[f,X,{x,y}] }
by A15;
verum
end;
A17:
( {x,y} is empty implies X is empty )
;
A18:
card { f where f is Function of X,{x,y} : S1[f,X,{x,y}] } = card { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) }
from STIRL2_1:sch 4(A17, A2, A1);
{ f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } c= { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) }
proof
z in {z}
by TARSKI:def 1;
then A19:
z in X \/ {z}
by XBOOLE_0:def 3;
let x1 be
object ;
TARSKI:def 3 ( not x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } or x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) } )
assume
x1 in { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
;
x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) }
then consider f being
Function of
(X \/ {z}),
{x,y} such that A20:
x1 = f
and A21:
card (f " {x}) = k + 1
and A22:
f . z = x
;
not
z in (dom f) /\ X
by A2, XBOOLE_0:def 4;
then
not
z in dom (f | X)
by RELAT_1:61;
then A23:
not
z in (f | X) " {x}
by FUNCT_1:def 7;
(
dom f = X \/ {z} &
(X \/ {z}) \ {z} = X )
by A2, FUNCT_2:def 1, ZFMISC_1:117;
then
((f | X) " {x}) \/ {z} = f " {x}
by A22, A19, AFINSQ_2:66;
then
(card ((f | X) " {x})) + 1
= k + 1
by A21, A23, CARD_2:41;
then A24:
S1[
f,
X \/ {z},
{x,y} \/ {x}]
;
{x} \/ {x,y} = {x,x,y}
by ENUMSET1:2;
then
(
rng (f | X) c= {x,y} &
f is
Function of
(X \/ {z}),
({x,y} \/ {x}) )
by ENUMSET1:30;
hence
x1 in { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) }
by A20, A22, A24;
verum
end;
then
{ f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) } = { f where f is Function of (X \/ {z}),({x,y} \/ {x}) : ( S1[f,X \/ {z},{x,y} \/ {x}] & rng (f | X) c= {x,y} & f . z = x ) }
by A3;
hence
card (Choose (X,k,x,y)) = card { f where f is Function of (X \/ {z}),{x,y} : ( card (f " {x}) = k + 1 & f . z = x ) }
by A11, A14, A18, XBOOLE_0:def 10; verum