let k, n, l be Element of NAT ; :: thesis: ( l < k implies card { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) } )
assume A1:
l < k
; :: thesis: card { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) }
set F1 = { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } ;
set F2 = { f where f is Function of n,k : ( f is onto & f is "increasing ) } ;
now per cases
not ( not ( k = 0 & n <> 0 ) & k = 0 & not n = 0 )
;
suppose
(
k = 0 implies
n = 0 )
;
:: thesis: card { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) } then A2:
(
k is
empty implies
n is
empty )
;
defpred S1[
set ,
set ,
set ]
means for
i,
j being
Element of
NAT st
i = $2 &
j = $3 holds
ex
f being
Function of
i,
j st
(
f = $1 &
f is
onto &
f is
"increasing & (
n < i implies
f " {(f . n)} <> {n} ) );
A3:
not
n in n
;
A4:
for
f being
Function of
(n \/ {n}),
(k \/ {l}) st
f . n = l holds
(
S1[
f,
n \/ {n},
k \/ {l}] iff
S1[
f | n,
n,
k] )
proof
let f' be
Function of
(n \/ {n}),
(k \/ {l});
:: thesis: ( f' . n = l implies ( S1[f',n \/ {n},k \/ {l}] iff S1[f' | n,n,k] ) )
assume A5:
f' . n = l
;
:: thesis: ( S1[f',n \/ {n},k \/ {l}] iff S1[f' | n,n,k] )
thus
(
S1[
f',
n \/ {n},
k \/ {l}] implies
S1[
f' | n,
n,
k] )
:: thesis: ( S1[f' | n,n,k] implies S1[f',n \/ {n},k \/ {l}] )proof
assume A6:
S1[
f',
n \/ {n},
k \/ {l}]
;
:: thesis: S1[f' | n,n,k]
(
n + 1
= n \/ {n} &
k = k \/ {l} )
by A1, Lm1, AFINSQ_1:4;
then consider f being
Function of
(n + 1),
k such that A7:
(
f = f' &
f is
onto &
f is
"increasing & (
n < n + 1 implies
f " {(f . n)} <> {n} ) )
by A6;
let i,
j be
Element of
NAT ;
:: thesis: ( i = n & j = k implies ex f being Function of i,j st
( f = f' | n & f is onto & f is "increasing & ( n < i implies f " {(f . n)} <> {n} ) ) )
assume A8:
(
i = n &
j = k )
;
:: thesis: ex f being Function of i,j st
( f = f' | n & f is onto & f is "increasing & ( n < i implies f " {(f . n)} <> {n} ) )
(
n <= n + 1 &
k <> 0 )
by A1, NAT_1:13;
then
(
dom f = n + 1 &
n c= n + 1 &
dom (f | n) = (dom f) /\ n )
by FUNCT_2:def 1, NAT_1:40, RELAT_1:90;
then
(
dom (f | n) = n &
rng (f | n) c= k )
by XBOOLE_1:28;
then reconsider fn =
f | n as
Function of
n,
k by FUNCT_2:4;
reconsider fi =
fn as
Function of
i,
j by A8;
(
fi = f' | n &
fi is
onto &
fi is
"increasing & (
n < i implies
fi " {(fi . n)} <> {n} ) )
by A7, A8, Th38, NAT_1:13;
hence
ex
f being
Function of
i,
j st
(
f = f' | n &
f is
onto &
f is
"increasing & (
n < i implies
f " {(f . n)} <> {n} ) )
;
:: thesis: verum
end;
thus
(
S1[
f' | n,
n,
k] implies
S1[
f',
n \/ {n},
k \/ {l}] )
:: thesis: verumproof
assume
S1[
f' | n,
n,
k]
;
:: thesis: S1[f',n \/ {n},k \/ {l}]
then consider fn being
Function of
n,
k such that A9:
fn = f' | n
and A10:
(
fn is
onto &
fn is
"increasing )
and
(
n < n implies
fn " {(fn . n)} <> {n} )
;
let i,
j be
Element of
NAT ;
:: thesis: ( i = n \/ {n} & j = k \/ {l} implies ex f being Function of i,j st
( f = f' & f is onto & f is "increasing & ( n < i implies f " {(f . n)} <> {n} ) ) )
assume A11:
(
i = n \/ {n} &
j = k \/ {l} )
;
:: thesis: ex f being Function of i,j st
( f = f' & f is onto & f is "increasing & ( n < i implies f " {(f . n)} <> {n} ) )
(
n \/ {n} = n + 1 &
k \/ {l} = k )
by A1, Lm1, AFINSQ_1:4;
then reconsider f =
f' as
Function of
(n + 1),
k ;
reconsider f1 =
f as
Function of
i,
j by A11;
(
n + 1
= i &
k = j )
by A1, A11, Lm1, AFINSQ_1:4;
then
(
f1 is
onto &
f1 is
"increasing & (
n < i implies
f1 " {(f1 . n)} <> {n} ) )
by A1, A5, A9, A10, Th41;
hence
ex
f being
Function of
i,
j st
(
f = f' &
f is
onto &
f is
"increasing & (
n < i implies
f " {(f . n)} <> {n} ) )
;
:: thesis: verum
end;
end; set FF1 =
{ f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) } ;
set FF2 =
{ f where f is Function of n,k : S1[f,n,k] } ;
A12:
card { f where f is Function of n,k : S1[f,n,k] } = card { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) }
from STIRL2_1:sch 4(A2, A3, A4);
A13:
{ f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) }
proof
thus
{ f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } c= { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) }
:: according to XBOOLE_0:def 10 :: thesis: { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) } c= { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } or x in { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) } )
assume A14:
x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) }
;
:: thesis: x in { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) }
consider f being
Function of
(n + 1),
k such that A15:
(
f = x &
f is
onto &
f is
"increasing &
f " {(f . n)} <> {n} &
f . n = l )
by A14;
S1[
f,
n \/ {n},
k \/ {l}]
then
(
S1[
f,
n \/ {n},
k \/ {l}] &
f . n = l &
rng (f | n) c= k &
n + 1
= n \/ {n} &
k = k \/ {l} )
by A1, A15, Lm1, AFINSQ_1:4;
hence
x in { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) }
by A15;
:: thesis: verum
end;
thus
{ f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) } c= { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) }
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) } or x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } )
assume A17:
x in { f where f is Function of (n \/ {n}),(k \/ {l}) : ( S1[f,n \/ {n},k \/ {l}] & rng (f | n) c= k & f . n = l ) }
;
:: thesis: x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) }
consider f being
Function of
(n \/ {n}),
(k \/ {l}) such that A18:
(
x = f &
S1[
f,
n \/ {n},
k \/ {l}] &
rng (f | n) c= k &
f . n = l )
by A17;
(
n + 1
= n \/ {n} &
k = k \/ {l} )
by A1, Lm1, AFINSQ_1:4;
then
ex
f' being
Function of
(n + 1),
k st
(
f = f' &
f' is
onto &
f' is
"increasing & (
n < n + 1 implies
f' " {(f' . n)} <> {n} ) )
by A18;
hence
x in { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) }
by A18, NAT_1:13;
:: thesis: verum
end;
end;
{ f where f is Function of n,k : ( f is onto & f is "increasing ) } = { f where f is Function of n,k : S1[f,n,k] }
proof
thus
{ f where f is Function of n,k : ( f is onto & f is "increasing ) } c= { f where f is Function of n,k : S1[f,n,k] }
:: according to XBOOLE_0:def 10 :: thesis: { f where f is Function of n,k : S1[f,n,k] } c= { f where f is Function of n,k : ( f is onto & f is "increasing ) } proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of n,k : ( f is onto & f is "increasing ) } or x in { f where f is Function of n,k : S1[f,n,k] } )
assume A19:
x in { f where f is Function of n,k : ( f is onto & f is "increasing ) }
;
:: thesis: x in { f where f is Function of n,k : S1[f,n,k] }
consider f being
Function of
n,
k such that A20:
(
x = f &
f is
onto &
f is
"increasing )
by A19;
S1[
x,
n,
k]
by A20;
hence
x in { f where f is Function of n,k : S1[f,n,k] }
by A20;
:: thesis: verum
end;
thus
{ f where f is Function of n,k : S1[f,n,k] } c= { f where f is Function of n,k : ( f is onto & f is "increasing ) }
:: thesis: verumproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of n,k : S1[f,n,k] } or x in { f where f is Function of n,k : ( f is onto & f is "increasing ) } )
assume A21:
x in { f where f is Function of n,k : S1[f,n,k] }
;
:: thesis: x in { f where f is Function of n,k : ( f is onto & f is "increasing ) }
consider f being
Function of
n,
k such that A22:
(
x = f &
S1[
f,
n,
k] )
by A21;
ex
g being
Function of
n,
k st
(
g = f &
g is
onto &
g is
"increasing & (
n < n implies
g " {(g . n)} <> {n} ) )
by A22;
hence
x in { f where f is Function of n,k : ( f is onto & f is "increasing ) }
by A22;
:: thesis: verum
end;
end; hence
card { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) }
by A12, A13;
:: thesis: verum end;
hence
card { f where f is Function of (n + 1),k : ( f is onto & f is "increasing & f " {(f . n)} <> {n} & f . n = l ) } = card { f where f is Function of n,k : ( f is onto & f is "increasing ) }
; :: thesis: verum