let n be Nat; for i, j being Nat st i in Seg (n + 1) & n >= 2 holds
ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st
( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds
( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )
let i, j be Nat; ( i in Seg (n + 1) & n >= 2 implies ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st
( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds
( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) ) )
assume that
A1:
i in Seg (n + 1)
and
A2:
n >= 2
; ex Proj being Function of (2Set (Seg n)),(2Set (Seg (n + 1))) st
( rng Proj = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & Proj is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds
( ( m < i & k < i implies Proj . {k,m} = {k,m} ) & ( m >= i & k < i implies Proj . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies Proj . {k,m} = {(k + 1),(m + 1)} ) ) ) )
defpred S1[ object , object ] means for k, m being Nat st {k,m} = $1 & k < m holds
( ( m < i & k < i implies $2 = {k,m} ) & ( m >= i & k < i implies $2 = {k,(m + 1)} ) & ( m >= i & k >= i implies $2 = {(k + 1),(m + 1)} ) );
set X = { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } ;
set SS = 2Set (Seg n);
set n1 = n + 1;
set SS1 = 2Set (Seg (n + 1));
A3:
for k, m being Nat holds
( not {k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } or k = i or m = i )
proof
let k,
m be
Nat;
( not {k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } or k = i or m = i )
assume
{k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) }
;
( k = i or m = i )
then consider m1 being
Nat such that A4:
{k,m} = {m1,i}
and
{m1,i} in 2Set (Seg (n + 1))
;
i in {i,m1}
by TARSKI:def 2;
hence
(
k = i or
m = i )
by A4, TARSKI:def 2;
verum
end;
A5:
for x being object st x in 2Set (Seg n) holds
ex y being object st
( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S1[x,y] )
proof
n <= n + 1
by NAT_1:11;
then A6:
Seg n c= Seg (n + 1)
by FINSEQ_1:5;
reconsider N =
n as
Element of
NAT by ORDINAL1:def 12;
let x be
object ;
( x in 2Set (Seg n) implies ex y being object st
( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S1[x,y] ) )
assume
x in 2Set (Seg n)
;
ex y being object st
( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S1[x,y] )
then consider k,
m being
Nat such that A7:
k in Seg n
and A8:
m in Seg n
and A9:
k < m
and A10:
x = {k,m}
by MATRIX11:1;
A11:
m + 1
in Seg (N + 1)
by A8, FINSEQ_1:60;
reconsider e =
k as
Element of
NAT by ORDINAL1:def 12;
A12:
e + 1
in Seg (N + 1)
by A7, FINSEQ_1:60;
per cases
( ( m < i & k < i ) or ( m >= i & k < i ) or ( m < i & k >= i ) or ( m >= i & k >= i ) )
;
suppose A13:
(
m < i &
k < i )
;
ex y being object st
( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S1[x,y] )then A14:
not
{k,m} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) }
by A3;
{k,m} in 2Set (Seg (n + 1))
by A7, A8, A9, A6, MATRIX11:1;
then A15:
{k,m} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) }
by A14, XBOOLE_0:def 5;
S1[
{k,m},
{k,m}]
by A13, ZFMISC_1:6;
hence
ex
y being
object st
(
y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } &
S1[
x,
y] )
by A10, A15;
verum end; suppose A16:
(
m >= i &
k < i )
;
ex y being object st
( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S1[x,y] )A17:
S1[
{k,m},
{k,(m + 1)}]
proof
let k9,
m9 be
Nat;
( {k9,m9} = {k,m} & k9 < m9 implies ( ( m9 < i & k9 < i implies {k,(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {k,(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {k,(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) )
assume that A18:
{k9,m9} = {k,m}
and
k9 < m9
;
( ( m9 < i & k9 < i implies {k,(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {k,(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {k,(m + 1)} = {(k9 + 1),(m9 + 1)} ) )
(
k9 = k or
k9 = m )
by A18, ZFMISC_1:6;
hence
( (
m9 < i &
k9 < i implies
{k,(m + 1)} = {k9,m9} ) & (
m9 >= i &
k9 < i implies
{k,(m + 1)} = {k9,(m9 + 1)} ) & (
m9 >= i &
k9 >= i implies
{k,(m + 1)} = {(k9 + 1),(m9 + 1)} ) )
by A16, A18, ZFMISC_1:6;
verum
end;
m + 1
> i
by A16, NAT_1:13;
then A19:
not
{k,(m + 1)} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) }
by A3, A16;
m + 1
> k
by A9, NAT_1:13;
then
{k,(m + 1)} in 2Set (Seg (n + 1))
by A7, A6, A11, MATRIX11:1;
then
{k,(m + 1)} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) }
by A19, XBOOLE_0:def 5;
hence
ex
y being
object st
(
y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } &
S1[
x,
y] )
by A10, A17;
verum end; suppose A20:
(
m >= i &
k >= i )
;
ex y being object st
( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S1[x,y] )A21:
S1[
{k,m},
{(k + 1),(m + 1)}]
proof
let k9,
m9 be
Nat;
( {k9,m9} = {k,m} & k9 < m9 implies ( ( m9 < i & k9 < i implies {(k + 1),(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {(k + 1),(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {(k + 1),(m + 1)} = {(k9 + 1),(m9 + 1)} ) ) )
assume that A22:
{k9,m9} = {k,m}
and A23:
k9 < m9
;
( ( m9 < i & k9 < i implies {(k + 1),(m + 1)} = {k9,m9} ) & ( m9 >= i & k9 < i implies {(k + 1),(m + 1)} = {k9,(m9 + 1)} ) & ( m9 >= i & k9 >= i implies {(k + 1),(m + 1)} = {(k9 + 1),(m9 + 1)} ) )
(
k9 = k or
k9 = m )
by A22, ZFMISC_1:6;
hence
( (
m9 < i &
k9 < i implies
{(k + 1),(m + 1)} = {k9,m9} ) & (
m9 >= i &
k9 < i implies
{(k + 1),(m + 1)} = {k9,(m9 + 1)} ) & (
m9 >= i &
k9 >= i implies
{(k + 1),(m + 1)} = {(k9 + 1),(m9 + 1)} ) )
by A20, A22, A23, ZFMISC_1:6;
verum
end; A24:
k + 1
> i
by A20, NAT_1:13;
m + 1
> k + 1
by A9, XREAL_1:8;
then A25:
{(k + 1),(m + 1)} in 2Set (Seg (n + 1))
by A11, A12, MATRIX11:1;
m + 1
> i
by A20, NAT_1:13;
then
not
{(k + 1),(m + 1)} in { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) }
by A3, A24;
then
{(k + 1),(m + 1)} in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) }
by A25, XBOOLE_0:def 5;
hence
ex
y being
object st
(
y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } &
S1[
x,
y] )
by A10, A21;
verum end; end;
end;
consider f being Function of (2Set (Seg n)),((2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } ) such that
A26:
for x being object st x in 2Set (Seg n) holds
S1[x,f . x]
from FUNCT_2:sch 1(A5);
ex y being object st
( y in (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & S1[{1,2},y] )
by A2, A5, MATRIX11:3;
then reconsider SSX = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } as non empty set ;
reconsider f = f as Function of (2Set (Seg n)),SSX ;
A27:
SSX c= rng f
proof
let x be
object ;
TARSKI:def 3 ( not x in SSX or x in rng f )
assume A28:
x in SSX
;
x in rng f
consider k,
m being
Nat such that A29:
k in Seg (n + 1)
and A30:
m in Seg (n + 1)
and A31:
k < m
and A32:
x = {k,m}
by A28, MATRIX11:1;
A33:
(
k <> i &
m <> i )
A34:
1
<= m
by A30, FINSEQ_1:1;
1
<= k
by A29, FINSEQ_1:1;
then reconsider k1 =
k - 1,
m1 =
m - 1 as
Element of
NAT by A34, NAT_1:21;
reconsider m9 =
m,
k9 =
k as
Element of
NAT by ORDINAL1:def 12;
per cases
( ( k < i & m < i ) or ( k > i & m < i ) or ( k < i & m > i ) or ( k > i & m > i ) )
by A33, XXREAL_0:1;
suppose A35:
(
k < i &
m < i )
;
x in rng fA36:
i <= n + 1
by A1, FINSEQ_1:1;
then
k < n + 1
by A35, XXREAL_0:2;
then A37:
k <= n
by NAT_1:13;
m < n + 1
by A35, A36, XXREAL_0:2;
then A38:
m <= n
by NAT_1:13;
1
<= m
by A30, FINSEQ_1:1;
then A39:
m in Seg n
by A38;
A40:
dom f = 2Set (Seg n)
by FUNCT_2:def 1;
1
<= k
by A29, FINSEQ_1:1;
then
k in Seg n
by A37;
then A41:
{k9,m9} in 2Set (Seg n)
by A31, A39, MATRIX11:1;
then
x = f . x
by A26, A31, A32, A35;
hence
x in rng f
by A32, A41, A40, FUNCT_1:def 3;
verum end; suppose A42:
(
k < i &
m > i )
;
x in rng f
1
<= i
by A1, FINSEQ_1:1;
then A43:
1
< m1 + 1
by A42, XXREAL_0:2;
then A44:
i <= m1
by A42, NAT_1:13;
then A45:
k < m1
by A42, XXREAL_0:2;
i <= n + 1
by A1, FINSEQ_1:1;
then
k < n + 1
by A42, XXREAL_0:2;
then A46:
k <= n
by NAT_1:13;
A47:
dom f = 2Set (Seg n)
by FUNCT_2:def 1;
m1 + 1
<= n + 1
by A30, FINSEQ_1:1;
then
m1 < n + 1
by NAT_1:13;
then A48:
m1 <= n
by NAT_1:13;
1
<= m1
by A43, NAT_1:13;
then A49:
m1 in Seg n
by A48;
1
<= k
by A29, FINSEQ_1:1;
then
k in Seg n
by A46;
then A50:
{k9,m1} in 2Set (Seg n)
by A49, A45, MATRIX11:1;
then
f . {k9,m1} = {k9,(m1 + 1)}
by A26, A42, A44, A45;
hence
x in rng f
by A32, A50, A47, FUNCT_1:def 3;
verum end; suppose A51:
(
k > i &
m > i )
;
x in rng f
k1 + 1
<= n + 1
by A29, FINSEQ_1:1;
then
k1 < n + 1
by NAT_1:13;
then A52:
k1 <= n
by NAT_1:13;
A53:
dom f = 2Set (Seg n)
by FUNCT_2:def 1;
m1 + 1
<= n + 1
by A30, FINSEQ_1:1;
then
m1 < n + 1
by NAT_1:13;
then A54:
m1 <= n
by NAT_1:13;
A55:
k1 < m1
by A31, XREAL_1:9;
A56:
1
<= i
by A1, FINSEQ_1:1;
then A57:
1
< m1 + 1
by A51, XXREAL_0:2;
A58:
1
< k1 + 1
by A51, A56, XXREAL_0:2;
then A59:
i <= k1
by A51, NAT_1:13;
1
<= k1
by A58, NAT_1:13;
then A60:
k1 in Seg n
by A52;
1
<= m1
by A57, NAT_1:13;
then
m1 in Seg n
by A54;
then A61:
{k1,m1} in 2Set (Seg n)
by A60, A55, MATRIX11:1;
i <= m1
by A51, A57, NAT_1:13;
then
f . {k1,m1} = {(k1 + 1),(m1 + 1)}
by A26, A59, A55, A61;
hence
x in rng f
by A32, A61, A53, FUNCT_1:def 3;
verum end; end;
end;
A62:
rng f c= SSX
by RELAT_1:def 19;
then A63:
SSX = rng f
by A27, XBOOLE_0:def 10;
dom f = 2Set (Seg n)
by FUNCT_2:def 1;
then reconsider f = f as Function of (2Set (Seg n)),(2Set (Seg (n + 1))) by A63, FUNCT_2:2;
take
f
; ( rng f = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & f is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds
( ( m < i & k < i implies f . {k,m} = {k,m} ) & ( m >= i & k < i implies f . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies f . {k,m} = {(k + 1),(m + 1)} ) ) ) )
for x1, x2 being object st x1 in 2Set (Seg n) & x2 in 2Set (Seg n) & f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in 2Set (Seg n) & x2 in 2Set (Seg n) & f . x1 = f . x2 implies x1 = x2 )
assume that A64:
x1 in 2Set (Seg n)
and A65:
x2 in 2Set (Seg n)
and A66:
f . x1 = f . x2
;
x1 = x2
consider k2,
m2 being
Nat such that
k2 in Seg n
and
m2 in Seg n
and A67:
k2 < m2
and A68:
x2 = {k2,m2}
by A65, MATRIX11:1;
consider k1,
m1 being
Nat such that
k1 in Seg n
and
m1 in Seg n
and A69:
k1 < m1
and A70:
x1 = {k1,m1}
by A64, MATRIX11:1;
reconsider m1 =
m1,
m2 =
m2,
k1 =
k1,
k2 =
k2 as
Element of
NAT by ORDINAL1:def 12;
per cases
( ( k1 < i & m1 < i & k2 < i & m2 < i ) or ( k1 < i & m1 < i & ( k2 < i or k2 >= i ) & m2 >= i ) or ( k1 < i & m1 >= i & k2 < i & m2 >= i ) or ( k1 < i & m1 >= i & ( ( k2 >= i & m2 >= i ) or ( k2 < i & m2 < i ) ) ) or ( k1 >= i & m1 < i ) or ( k2 >= i & m2 < i ) or ( k1 >= i & m1 >= i & k2 >= i & m2 >= i ) or ( k1 >= i & m1 >= i & ( ( k2 < i & m2 < i ) or ( k2 < i & m2 >= i ) ) ) )
;
suppose A71:
(
k1 < i &
m1 < i &
k2 < i &
m2 < i )
;
x1 = x2end; suppose A72:
(
k1 < i &
m1 < i & (
k2 < i or
k2 >= i ) &
m2 >= i )
;
x1 = x2then A73:
(
f . x2 = {k2,(m2 + 1)} or
f . x2 = {(k2 + 1),(m2 + 1)} )
by A26, A65, A67, A68;
f . x1 = {k1,m1}
by A26, A64, A69, A70, A72;
then
( ( (
k1 = k2 or
k1 = m2 + 1 ) & (
m1 = k2 or
m1 = m2 + 1 ) ) or ( (
k1 = k2 + 1 or
k1 = m2 + 1 ) & (
m1 = k2 + 1 or
m1 = m2 + 1 ) ) )
by A66, A73, ZFMISC_1:6;
hence
x1 = x2
by A69, A72, NAT_1:13;
verum end; suppose A74:
(
k1 < i &
m1 >= i &
k2 < i &
m2 >= i )
;
x1 = x2then A75:
f . x2 = {k2,(m2 + 1)}
by A26, A65, A67, A68;
A76:
f . x1 = {k1,(m1 + 1)}
by A26, A64, A69, A70, A74;
then A77:
(
m1 + 1
= k2 or
m1 + 1
= m2 + 1 )
by A66, A75, ZFMISC_1:6;
(
k1 = k2 or
k1 = m2 + 1 )
by A66, A76, A75, ZFMISC_1:6;
hence
x1 = x2
by A70, A68, A74, A77, NAT_1:13;
verum end; suppose A78:
(
k1 < i &
m1 >= i & ( (
k2 >= i &
m2 >= i ) or (
k2 < i &
m2 < i ) ) )
;
x1 = x2then A79:
(
f . x2 = {(k2 + 1),(m2 + 1)} or
f . x2 = {k2,m2} )
by A26, A65, A67, A68;
f . x1 = {k1,(m1 + 1)}
by A26, A64, A69, A70, A78;
then
( ( (
k1 = k2 + 1 or
k1 = m2 + 1 ) & (
m1 + 1
= k2 + 1 or
m1 + 1
= m2 + 1 ) ) or ( (
k1 = k2 or
k1 = m2 ) & (
m1 + 1
= k2 or
m1 + 1
= m2 ) ) )
by A66, A79, ZFMISC_1:6;
hence
x1 = x2
by A78, NAT_1:13;
verum end; suppose
( (
k1 >= i &
m1 < i ) or (
k2 >= i &
m2 < i ) )
;
x1 = x2end; suppose A80:
(
k1 >= i &
m1 >= i &
k2 >= i &
m2 >= i )
;
x1 = x2then A81:
f . x2 = {(k2 + 1),(m2 + 1)}
by A26, A65, A67, A68;
A82:
f . x1 = {(k1 + 1),(m1 + 1)}
by A26, A64, A69, A70, A80;
then A83:
(
m1 + 1
= k2 + 1 or
m1 + 1
= m2 + 1 )
by A66, A81, ZFMISC_1:6;
(
k1 + 1
= k2 + 1 or
k1 + 1
= m2 + 1 )
by A66, A82, A81, ZFMISC_1:6;
hence
x1 = x2
by A69, A70, A68, A83;
verum end; suppose A84:
(
k1 >= i &
m1 >= i & ( (
k2 < i &
m2 < i ) or (
k2 < i &
m2 >= i ) ) )
;
x1 = x2then A85:
(
f . x2 = {k2,m2} or
f . x2 = {k2,(m2 + 1)} )
by A26, A65, A67, A68;
f . x1 = {(k1 + 1),(m1 + 1)}
by A26, A64, A69, A70, A84;
then
( ( (
k1 + 1
= k2 or
k1 + 1
= m2 ) & (
m1 + 1
= k2 or
m1 + 1
= m2 ) ) or ( (
k1 + 1
= k2 or
k1 + 1
= m2 + 1 ) & (
m1 + 1
= k2 or
m1 + 1
= m2 + 1 ) ) )
by A66, A85, ZFMISC_1:6;
hence
x1 = x2
by A69, A84, NAT_1:13;
verum end; end;
end;
hence
( rng f = (2Set (Seg (n + 1))) \ { {N,i} where N is Nat : {N,i} in 2Set (Seg (n + 1)) } & f is one-to-one & ( for k, m being Nat st k < m & {k,m} in 2Set (Seg n) holds
( ( m < i & k < i implies f . {k,m} = {k,m} ) & ( m >= i & k < i implies f . {k,m} = {k,(m + 1)} ) & ( m >= i & k >= i implies f . {k,m} = {(k + 1),(m + 1)} ) ) ) )
by A26, A27, A62, FUNCT_2:19, XBOOLE_0:def 10; verum