defpred S1[ Nat] means for A being finite Chain st card the carrier of A = $1 holds
A, InclPoset $1 are_isomorphic ;
A1:
S1[ 0 ]
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A4:
for
A being
finite Chain st
card the
carrier of
A = n holds
A,
InclPoset n are_isomorphic
;
:: thesis: S1[n + 1]
let A be
finite Chain ;
:: thesis: ( card the carrier of A = n + 1 implies A, InclPoset (n + 1) are_isomorphic )
assume A5:
card the
carrier of
A = n + 1
;
:: thesis: A, InclPoset (n + 1) are_isomorphic
n >= 0
by NAT_1:2;
then
n + 1
>= 0 + 1
by XREAL_1:8;
then A6:
(
n >= 1 or
n + 1
= 1 )
by NAT_1:8;
the
carrier of
A <> {}
by A5;
then reconsider A =
A as non
empty finite Chain ;
set b =
Top A;
per cases
( n + 1 = 1 or n + 1 > 1 )
by A6, NAT_1:13;
suppose
n + 1
> 1
;
:: thesis: A, InclPoset (n + 1) are_isomorphic then A12:
(n + 1) - 1
> 1
- 1
by XREAL_1:11;
A13:
card (the carrier of A \ {(Top A)}) =
(card the carrier of A) - (card {(Top A)})
by CARD_2:63
.=
(n + 1) - 1
by A5, CARD_1:50
.=
n
;
then reconsider Ab = the
carrier of
A \ {(Top A)} as non
empty Subset of
A by A12;
reconsider B =
subrelstr Ab as
finite Chain by Def1;
card the
carrier of
B = n
by A13, YELLOW_0:def 15;
then
B,
InclPoset n are_isomorphic
by A4;
then consider f being
Function of
B,
(InclPoset n) such that A14:
f is
isomorphic
by WAYBEL_1:def 8;
A15:
the
carrier of
B = the
carrier of
A \ {(Top A)}
by YELLOW_0:def 15;
n <= n + 1
by NAT_1:11;
then
n c= n + 1
by NAT_1:40;
then A16:
n c= the
carrier of
(InclPoset (n + 1))
by YELLOW_1:1;
A17:
the
carrier of
B,
{(Top A)} form_upper_lower_partition_of A
by A15, Th3;
A18:
the
carrier of
(InclPoset n) = n
by YELLOW_1:1;
A19:
n + 1 =
succ n
by NAT_1:39
.=
n \/ {n}
by ORDINAL1:def 1
;
then A20:
the
carrier of
(InclPoset n) \/ {n} = the
carrier of
(InclPoset (n + 1))
by A18, YELLOW_1:1;
for
a,
b being
Element of
(InclPoset (n + 1)) st
a in the
carrier of
(InclPoset n) &
b in {n} holds
a < b
then A26:
the
carrier of
(InclPoset n),
{n} form_upper_lower_partition_of InclPoset (n + 1)
by A20, Def3;
set X =
InclPoset {(Top A)};
{(Top A)} c= {(Top A)}
;
then reconsider b' =
{(Top A)} as non
empty Subset of
(InclPoset {(Top A)}) by YELLOW_1:1;
{n} c= n + 1
by A19, XBOOLE_1:7;
then reconsider n' =
{n} as non
empty Subset of
(InclPoset (n + 1)) by YELLOW_1:1;
set X' =
subrelstr b';
set Y' =
subrelstr n';
A27:
the
carrier of
(subrelstr b') = {(Top A)}
by YELLOW_0:def 15;
set g = the
carrier of
(subrelstr b') --> n;
A28:
dom (the carrier of (subrelstr b') --> n) = the
carrier of
(subrelstr b')
by FUNCOP_1:19;
then reconsider g = the
carrier of
(subrelstr b') --> n as
ManySortedSet of
by PARTFUN1:def 4;
rng g c= {n}
by FUNCOP_1:19;
then A29:
rng g c= the
carrier of
(subrelstr n')
by YELLOW_0:def 15;
for
x being
set st
x in the
carrier of
(subrelstr b') holds
g . x in the
carrier of
(subrelstr n')
then A30:
( the
carrier of
(subrelstr n') = n' & the
carrier of
(subrelstr {(Top A)}) = {(Top A)} &
g is
Function of the
carrier of
(subrelstr b'),the
carrier of
(subrelstr n') )
by A28, FUNCT_2:5, YELLOW_0:def 15;
then reconsider g =
g as
Function of
(subrelstr {(Top A)}),
(subrelstr n') by A27;
A31:
g is
one-to-one
by A30, PARTFUN1:70;
g . (Top A) in n'
by A30, FUNCT_2:61;
then
g . (Top A) = n
by TARSKI:def 1;
then A32:
rng g = the
carrier of
(subrelstr n')
by A30, FUNCT_2:62;
A33:
g is
isomorphic
reconsider A2 = the
carrier of
(InclPoset n),
B2 =
n' as
Subset of
(InclPoset (n + 1)) by A16, YELLOW_1:1;
n <= n + 1
by NAT_1:11;
then
(
A2 = n &
InclPoset n is
full SubRelStr of
InclPoset (n + 1) )
by Th1, YELLOW_1:1;
then
(
InclPoset n = subrelstr A2 & the
carrier of
B = Ab &
g is
Function of
(subrelstr {(Top A)}),
(subrelstr B2) )
by YELLOW_0:def 15;
then consider h being
Function of
A,
(InclPoset (n + 1)) such that A37:
(
h = f +* g &
h is
isomorphic )
by A14, A17, A26, A33, Th5;
thus
A,
InclPoset (n + 1) are_isomorphic
by A37, WAYBEL_1:def 8;
:: thesis: verum end;
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A3);
hence
for A being finite Chain
for n being Nat st card the carrier of A = n holds
A, InclPoset n are_isomorphic
; :: thesis: verum