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;
:: thesis: ( 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
;
:: thesis: S1[n + 1]
n >= 0
by NAT_1:2;
then
n + 1
>= 0 + 1
by XREAL_1:8;
then A3:
(
n >= 1 or
n + 1
= 1 )
by NAT_1:8;
let A be
finite Chain ;
:: thesis: ( card the carrier of A = n + 1 implies A, InclPoset (n + 1) are_isomorphic )
assume A4:
card the
carrier of
A = n + 1
;
:: thesis: 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
;
:: thesis: 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:63
.=
(n + 1) - 1
by A4, CARD_1:50
.=
n
;
(n + 1) - 1
> 1
- 1
by A10, XREAL_1:11;
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
by WAYBEL_1:def 8;
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:
n + 1 =
succ n
by NAT_1:39
.=
n \/ {n}
by ORDINAL1:def 1
;
then
{n} c= n + 1
by XBOOLE_1:7;
then reconsider n' =
{n} as non
empty Subset of
(InclPoset (n + 1)) by YELLOW_1:1;
set X =
InclPoset {(Top A)};
A15:
the
carrier of
(subrelstr n') = n'
by YELLOW_0:def 15;
{(Top A)} c= {(Top A)}
;
then reconsider b' =
{(Top A)} as non
empty Subset of
(InclPoset {(Top A)}) by YELLOW_1:1;
set X' =
subrelstr b';
set Y' =
subrelstr n';
set g = the
carrier of
(subrelstr b') --> n;
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;
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, Def3;
n <= n + 1
by NAT_1:11;
then
n c= n + 1
by NAT_1:40;
then
n c= the
carrier of
(InclPoset (n + 1))
by YELLOW_1:1;
then reconsider A2 = the
carrier of
(InclPoset n),
B2 =
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 b') = {(Top A)}
by YELLOW_0:def 15;
then reconsider g =
g as
Function of
(subrelstr {(Top A)}),
(subrelstr n') by A15, A29;
g . (Top A) in n'
by A15, A29, FUNCT_2:61;
then
g . (Top A) = n
by TARSKI:def 1;
then A31:
rng g = the
carrier of
(subrelstr n')
by A15, A29, FUNCT_2:62;
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:70;
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
by WAYBEL_1:def 8;
:: thesis: 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
; :: thesis: verum