defpred S1[ Nat] means for A being finite Chain st card the carrier of A = $1 holds
A, InclPoset $1 are_isomorphic ;
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:
for
A being
finite Chain st
card the
carrier of
A = n holds
A,
InclPoset n are_isomorphic
;
S1[n + 1]
n >= 0
by NAT_1:2;
then
n + 1
>= 0 + 1
by XREAL_1:6;
then A3:
(
n >= 1 or
n + 1
= 1 )
by NAT_1:8;
let A be
finite Chain ;
( card the carrier of A = n + 1 implies A, InclPoset (n + 1) are_isomorphic )
assume A4:
card the
carrier of
A = n + 1
;
A, InclPoset (n + 1) are_isomorphic
then reconsider A =
A as non
empty finite Chain ;
set b =
Top A;
per cases
( n + 1 = 1 or n + 1 > 1 )
by A3, NAT_1:13;
suppose A10:
n + 1
> 1
;
A, InclPoset (n + 1) are_isomorphic A11:
card ( the carrier of A \ {(Top A)}) =
(card the carrier of A) - (card {(Top A)})
by CARD_2:44
.=
(n + 1) - 1
by A4, CARD_1:30
.=
n
;
(n + 1) - 1
> 1
- 1
by A10, XREAL_1:9;
then reconsider Ab = the
carrier of
A \ {(Top A)} as non
empty Subset of
A by A11;
reconsider B =
subrelstr Ab as
finite Chain by Def1;
card the
carrier of
B = n
by A11, YELLOW_0:def 15;
then
B,
InclPoset n are_isomorphic
by A2;
then consider f being
Function of
B,
(InclPoset n) such that A12:
f is
isomorphic
;
the
carrier of
B = the
carrier of
A \ {(Top A)}
by YELLOW_0:def 15;
then A13:
the
carrier of
B,
{(Top A)} form_upper_lower_partition_of A
by Th3;
A14:
Segm (n + 1) = (Segm n) \/ {n}
by AFINSQ_1:2;
then
{n} c= Segm (n + 1)
by XBOOLE_1:7;
then reconsider n9 =
{n} as non
empty Subset of
(InclPoset (n + 1)) by YELLOW_1:1;
set X =
InclPoset {(Top A)};
A15:
the
carrier of
(subrelstr n9) = n9
by YELLOW_0:def 15;
{(Top A)} c= {(Top A)}
;
then reconsider b9 =
{(Top A)} as non
empty Subset of
(InclPoset {(Top A)}) by YELLOW_1:1;
set X9 =
subrelstr b9;
set g = the
carrier of
(subrelstr b9) --> n;
dom ( the carrier of (subrelstr b9) --> n) = the
carrier of
(subrelstr b9)
by FUNCOP_1:13;
then reconsider g = the
carrier of
(subrelstr b9) --> n as
ManySortedSet of the
carrier of
(subrelstr b9) by PARTFUN1:def 2;
A16:
for
a,
b being
Element of
(InclPoset (n + 1)) st
a in the
carrier of
(InclPoset n) &
b in {n} holds
a < b
the
carrier of
(InclPoset n) = n
by YELLOW_1:1;
then
the
carrier of
(InclPoset n) \/ {n} = the
carrier of
(InclPoset (n + 1))
by A14, YELLOW_1:1;
then A28:
the
carrier of
(InclPoset n),
{n} form_upper_lower_partition_of InclPoset (n + 1)
by A16;
n <= n + 1
by NAT_1:11;
then
Segm n c= Segm (n + 1)
by NAT_1:39;
then
n c= the
carrier of
(InclPoset (n + 1))
by YELLOW_1:1;
then reconsider A2 = the
carrier of
(InclPoset n) as
Subset of
(InclPoset (n + 1)) by YELLOW_1:1;
A29:
the
carrier of
(subrelstr {(Top A)}) = {(Top A)}
by YELLOW_0:def 15;
A30:
the
carrier of
(subrelstr b9) = {(Top A)}
by YELLOW_0:def 15;
then reconsider g =
g as
Function of
(subrelstr {(Top A)}),
(subrelstr n9) by A15, A29;
g . (Top A) in n9
by A15, A29, FUNCT_2:47;
then
g . (Top A) = n
by TARSKI:def 1;
then A31:
rng g = the
carrier of
(subrelstr n9)
by A15, A29, FUNCT_2:48;
A32:
for
e,
f being
Element of
(subrelstr {(Top A)}) holds
(
e <= f iff
g . e <= g . f )
g is
one-to-one
by A29, PARTFUN1:17;
then A34:
g is
isomorphic
by A31, A32, WAYBEL_0:66;
InclPoset n is
full SubRelStr of
InclPoset (n + 1)
by Th1, NAT_1:11;
then A35:
InclPoset n = subrelstr A2
by YELLOW_0:def 15;
the
carrier of
B = Ab
by YELLOW_0:def 15;
then
ex
h being
Function of
A,
(InclPoset (n + 1)) st
(
h = f +* g &
h is
isomorphic )
by A12, A13, A28, A34, A35, Th5;
hence
A,
InclPoset (n + 1) are_isomorphic
;
verum end;
end;
A36:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A36, A1);
hence
for A being finite Chain
for n being Nat st card the carrier of A = n holds
A, InclPoset n are_isomorphic
; verum