:: On the Isomorphism Between Finite Chains
:: by Marta Pruszy\'nska and Marek Dudzicz
::
:: Received June 29, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TREES_2, ORDERS_2, RELAT_2, XBOOLE_0, STRUCT_0, ZFMISC_1, CARD_3,
FINSET_1, CAT_1, YELLOW_0, SUBSET_1, XXREAL_0, TARSKI, NAT_1, YELLOW_1,
WELLORD2, WELLORD1, ARYTM_3, LATTICES, FUNCT_1, FUNCT_4, RELAT_1, CARD_1,
FUNCOP_1, ARYTM_1, PBOOLE, ORDERS_4;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
PBOOLE, CARD_3, RELAT_2, ORDERS_1, ORDERS_2, RELAT_1, FUNCT_1, FUNCT_2,
FUNCOP_1, FUNCT_4, DOMAIN_1, STRUCT_0, YELLOW_0, WAYBEL_0, YELLOW_1,
WAYBEL_1, WELLORD1, XXREAL_0;
constructors DOMAIN_1, NAT_1, NAT_D, MEMBERED, TOLER_1, LATTICE3, ORDERS_3,
WAYBEL_1, RELSET_1, CARD_3;
registrations XBOOLE_0, RELSET_1, FINSET_1, XREAL_0, NAT_1, MEMBERED,
STRUCT_0, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_2, YELLOW11,
CARD_1, ORDERS_2;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, WAYBEL_1;
equalities WELLORD1, ORDINAL1;
expansions TARSKI, WAYBEL_1;
theorems CARD_1, CARD_2, CARD_4, WAYBEL_0, YELLOW_0, YELLOW_1, ORDERS_2,
TARSKI, WELLORD2, NAT_1, AXIOMS, FUNCT_1, FUNCT_2, FUNCT_4, RELAT_1,
RELAT_2, FUNCOP_1, XBOOLE_0, XBOOLE_1, PARTFUN1, XREAL_1, XXREAL_0,
AFINSQ_1;
schemes NAT_1;
begin
definition
mode Chain -> RelStr means
:Def1:
it is connected non empty Poset or it is empty;
existence
proof
set R = the empty RelStr;
take R;
thus thesis;
end;
end;
registration
cluster empty -> reflexive transitive antisymmetric for RelStr;
coherence
proof
let A be RelStr;
assume
A1: A is empty;
then
for x,y,z be object holds x in the carrier of A & y in the carrier of A &
z in the carrier of A & [x,y] in the InternalRel of A & [y,z] in the
InternalRel of A implies [x,z] in the InternalRel of A;
then
A2: the InternalRel of A is_transitive_in the carrier of A by RELAT_2:def 8;
for x,y be object holds x in the carrier of A & y in the carrier of A & [
x,y] in the InternalRel of A & [y,x] in the InternalRel of A implies x = y by
A1;
then
A3: the InternalRel of A is_antisymmetric_in the carrier of A by RELAT_2:def 4;
for x be object holds x in the carrier of A implies [x,x] in the
InternalRel of A by A1;
then the InternalRel of A is_reflexive_in the carrier of A by RELAT_2:def 1
;
hence thesis by A2,A3,ORDERS_2:def 2,def 3,def 4;
end;
end;
registration
cluster -> reflexive transitive antisymmetric for Chain;
coherence
proof
let A be Chain;
A is connected non empty Poset or A is empty RelStr by Def1;
hence thesis;
end;
end;
registration
cluster non empty for Chain;
existence
proof
set A = the trivial reflexive transitive antisymmetric non empty RelStr;
A is Chain by Def1;
hence thesis;
end;
end;
registration
cluster -> connected for non empty Chain;
coherence by Def1;
end;
definition
let L be 1-sorted;
attr L is countable means
the carrier of L is countable;
end;
registration
cluster finite non empty for Chain;
existence
proof
set A = the trivial reflexive transitive antisymmetric non empty finite RelStr;
A is Chain by Def1;
hence thesis;
end;
end;
registration
cluster countable for Chain;
existence
proof
set L = the finite Chain;
take L;
the carrier of L is countable by CARD_4:1;
hence thesis;
end;
end;
registration
let A be connected non empty RelStr;
cluster full -> connected for non empty SubRelStr of A;
correctness
proof
let S be non empty SubRelStr of A;
assume
A1: S is full;
for x,y being Element of S holds x <= y or y <= x
proof
let x,y be Element of S;
A2: the carrier of S c= the carrier of A by YELLOW_0:def 13;
reconsider b=y as Element of A by A2;
reconsider a=x as Element of A by A2;
a <= b or b <= a by WAYBEL_0:def 29;
hence thesis by A1,YELLOW_0:60;
end;
hence thesis by WAYBEL_0:def 29;
end;
end;
registration
let A be finite RelStr;
cluster -> finite for SubRelStr of A;
correctness
proof
let S be SubRelStr of A;
the carrier of S c= the carrier of A by YELLOW_0:def 13;
hence thesis;
end;
end;
theorem Th1:
for n,m be Nat holds n <= m implies InclPoset(n) is full
SubRelStr of InclPoset(m)
proof
let n,m be Nat;
A1: the InternalRel of InclPoset m = RelIncl m by YELLOW_1:1;
assume n <= m;
then
A2: Segm n c= Segm m by NAT_1:39;
A3: RelIncl n c= RelIncl m
proof
let x be object;
assume x in RelIncl n;
then x in (RelIncl m) |_2 n by A2,WELLORD2:7;
hence thesis by XBOOLE_0:def 4;
end;
the carrier of InclPoset(m)=m by YELLOW_1:1;
then
A4: the carrier of InclPoset(n) c= the carrier of InclPoset(m) by A2,YELLOW_1:1
;
A5: the InternalRel of InclPoset n = RelIncl n by YELLOW_1:1;
then (RelIncl m) |_2 n = the InternalRel of InclPoset n by A2,WELLORD2:7;
then the InternalRel of InclPoset(n) = (the InternalRel of InclPoset(m))|_2
the carrier of InclPoset(n) by A1,YELLOW_1:1;
hence thesis by A4,A5,A1,A3,YELLOW_0:def 13,def 14;
end;
definition
let L be RelStr;
let A,B be set;
pred A,B form_upper_lower_partition_of L means
A \/ B = the carrier
of L & for a,b be Element of L st a in A & b in B holds a < b;
end;
theorem Th2:
for L be RelStr for A,B be set holds A,B
form_upper_lower_partition_of L implies A misses B
proof
let L be RelStr;
let A,B be set;
assume that
A1: A,B form_upper_lower_partition_of L and
A2: A meets B;
consider x be object such that
A3: x in A /\ B by A2,XBOOLE_0:4;
A4: x in B by A3,XBOOLE_0:def 4;
A5: x in A by A3,XBOOLE_0:def 4;
A \/ B = the carrier of L by A1;
then reconsider x as Element of L by A5,XBOOLE_0:def 3;
x < x by A1,A5,A4;
hence contradiction;
end;
theorem Th3:
for L be upper-bounded antisymmetric non empty RelStr holds ((the
carrier of L) \ { Top L }), { Top L } form_upper_lower_partition_of L
proof
let L be upper-bounded antisymmetric non empty RelStr;
A1: for a,b be Element of L st a in ((the carrier of L) \ { Top L }) & b in
{ Top L } holds a < b
proof
let a,b be Element of L;
assume that
A2: a in ((the carrier of L) \ { Top L }) and
A3: b in { Top L };
not a in { Top L } by A2,XBOOLE_0:def 5;
then
A4: a <> Top L by TARSKI:def 1;
A5: a <= Top L by YELLOW_0:45;
b = Top L by A3,TARSKI:def 1;
hence thesis by A4,A5,ORDERS_2:def 6;
end;
((the carrier of L) \ { Top L }) \/ { Top L } = the carrier of L by
XBOOLE_1:45;
hence thesis by A1;
end;
theorem Th4:
for L1,L2 be RelStr for f be Function of L1,L2 st f is isomorphic
holds (the carrier of L1 <> {} iff the carrier of L2 <> {}) & (the carrier of
L2 <> {} or the carrier of L1 = {}) & (the carrier of L1 = {} iff the carrier
of L2 = {})
proof
let L1,L2 be RelStr;
let f be Function of L1,L2 such that
A1: f is isomorphic;
the carrier of L1 = {} iff the carrier of L2 = {}
proof
hereby
assume the carrier of L1 = {};
then L1 is empty;
then L2 is empty by A1,WAYBEL_0:def 38;
hence the carrier of L2 = {};
end;
assume the carrier of L2 = {};
then L2 is empty;
then L1 is empty by A1,WAYBEL_0:def 38;
hence thesis;
end;
hence thesis;
end;
theorem Th5:
for L1,L2 be antisymmetric RelStr for A1,B1 be Subset of L1 st A1
,B1 form_upper_lower_partition_of L1 for A2,B2 be Subset of L2 st A2,B2
form_upper_lower_partition_of L2 for f be Function of subrelstr A1, subrelstr
A2 st f is isomorphic for g be Function of subrelstr B1, subrelstr B2 st g is
isomorphic ex h be Function of L1,L2 st h = f +* g & h is isomorphic
proof
let L1,L2 be antisymmetric RelStr;
let A1,B1 be Subset of L1 such that
A1: A1,B1 form_upper_lower_partition_of L1;
A2: A1 \/ B1 = the carrier of L1 by A1;
let A2,B2 be Subset of L2 such that
A3: A2,B2 form_upper_lower_partition_of L2;
A4: A2 misses B2 by A3,Th2;
A5: A2 \/ B2 = the carrier of L2 by A3;
A6: A1 misses B1 by A1,Th2;
let f be Function of subrelstr A1, subrelstr A2 such that
A7: f is isomorphic;
let g be Function of subrelstr B1, subrelstr B2 such that
A8: g is isomorphic;
set h = f +* g;
per cases;
suppose
A9: the carrier of L1 = {};
then
A10: A1 = {} by A2;
then the carrier of subrelstr A1 = {} by YELLOW_0:def 15;
then dom f = the carrier of subrelstr A1;
then
A11: dom f = A1 by YELLOW_0:def 15;
subrelstr A1 is empty by A10,YELLOW_0:def 15;
then subrelstr A2 is empty by A7,WAYBEL_0:def 38;
then
A12: A2 = {} by YELLOW_0:def 15;
A13: for x be object st x in the carrier of L1 holds h.x in the carrier of L2
by A9;
A14: B1 = {} by A2,A9;
then
the carrier of subrelstr B2 <> {} or the carrier of subrelstr B1 = {}
by YELLOW_0:def 15;
then dom g = the carrier of subrelstr B1 by FUNCT_2:def 1;
then dom g = B1 by YELLOW_0:def 15;
then dom h = the carrier of L1 by A2,A11,FUNCT_4:def 1;
then reconsider h as Function of L1,L2 by A13,FUNCT_2:3;
A15: L1 is empty by A9;
subrelstr B1 is empty by A14,YELLOW_0:def 15;
then L2 is empty by A8,A5,A12,WAYBEL_0:def 38;
then h is isomorphic by A15,WAYBEL_0:def 38;
hence thesis;
end;
suppose
A16: the carrier of L1 <> {};
then A1 <> {} or B1 <> {} by A2;
then subrelstr A1 is non empty or subrelstr B1 is non empty by
YELLOW_0:def 15;
then
A17: subrelstr A2 is non empty or subrelstr B2 is non empty by A7,A8,
WAYBEL_0:def 38;
(A2 <> {} or B2 <> {}) implies (B2 <> {} or B1 = {})
proof
assume A2 <> {} or B2 <> {};
the carrier of subrelstr B2 <> {} or the carrier of subrelstr B1 =
{} by A8,Th4;
hence thesis by YELLOW_0:def 15;
end;
then
A18: the carrier of subrelstr B2 <> {} or the carrier of subrelstr B1 = {}
by A17,YELLOW_0:def 15;
then
A19: dom g = the carrier of subrelstr B1 by FUNCT_2:def 1;
then
A20: dom g = B1 by YELLOW_0:def 15;
(A1 <> {} or B1 <> {}) implies (A2 <> {} or A1 = {})
proof
assume A1 <> {} or B1 <> {};
the carrier of subrelstr A2 <> {} or the carrier of subrelstr A1 =
{} by A7,Th4;
hence thesis by YELLOW_0:def 15;
end;
then
the carrier of subrelstr A2 <> {} or the carrier of subrelstr A1 = {}
by YELLOW_0:def 15;
then dom f = the carrier of subrelstr A1 by FUNCT_2:def 1;
then
A21: dom f = A1 by YELLOW_0:def 15;
A22: dom h = dom f \/ dom g by FUNCT_4:def 1;
A23: dom f misses dom g implies rng h = rng f \/ rng g
proof
assume
A24: dom f misses dom g;
A25: rng f \/ rng g c= rng h
proof
let x be object;
assume
A26: x in rng f \/ rng g;
per cases by A26,XBOOLE_0:def 3;
suppose
x in rng f;
then consider z be object such that
A27: z in dom f and
A28: x = f.z by FUNCT_1:def 3;
not z in dom g by A24,A27,XBOOLE_0:3;
then
A29: x = h.z by A28,FUNCT_4:11;
z in dom h by A22,A27,XBOOLE_0:def 3;
hence thesis by A29,FUNCT_1:def 3;
end;
suppose
x in rng g;
then consider z be object such that
A30: z in dom g and
A31: x = g.z by FUNCT_1:def 3;
z in dom h & h.z = g.z by A22,A30,FUNCT_4:13,XBOOLE_0:def 3;
hence thesis by A31,FUNCT_1:def 3;
end;
end;
rng h c= rng f \/ rng g by FUNCT_4:17;
hence thesis by A25,XBOOLE_0:def 10;
end;
A32: rng h = the carrier of L2
proof
per cases;
suppose
A33: A2 = {} & A1 = {};
then subrelstr B1 is non empty by A2,A16,YELLOW_0:def 15;
then
A34: rng g = the carrier of subrelstr B2 by A8,A17,A33,WAYBEL_0:66
,YELLOW_0:def 15;
rng f = {} by A21,A33,RELAT_1:42;
hence thesis by A5,A21,A23,A33,A34,XBOOLE_1:65,YELLOW_0:def 15;
end;
suppose
A2 = {} & A1 <> {};
then
the carrier of subrelstr A2 = {} & the carrier of subrelstr A1 <>
{} by YELLOW_0:def 15;
hence thesis by A7,Th4;
end;
suppose
A2 <> {} & A1 = {};
then
the carrier of subrelstr A2 <> {} & the carrier of subrelstr A1 =
{} by YELLOW_0:def 15;
hence thesis by A7,Th4;
end;
suppose
A35: A2 <> {} & A1 <> {};
rng h = the carrier of L2
proof
per cases;
suppose
A36: B2 <> {};
then the carrier of subrelstr B2 <> {} by YELLOW_0:def 15;
then the carrier of subrelstr B1 <> {} by A8,Th4;
then
A37: subrelstr B1 is non empty;
subrelstr A2 is non empty & subrelstr A1 is non empty by A35,
YELLOW_0:def 15;
then rng f = the carrier of subrelstr A2 by A7,WAYBEL_0:66;
then
A38: rng f = A2 by YELLOW_0:def 15;
subrelstr B2 is non empty by A36,YELLOW_0:def 15;
then rng g = the carrier of subrelstr B2 by A8,A37,WAYBEL_0:66;
hence thesis by A1,A5,A21,A20,A23,A38,Th2,YELLOW_0:def 15;
end;
suppose
A39: B2 = {};
subrelstr A2 is non empty & subrelstr A1 is non empty by A35,
YELLOW_0:def 15;
then
A40: rng f = the carrier of subrelstr A2 by A7,WAYBEL_0:66;
g = {} by A18,A39,YELLOW_0:def 15;
hence thesis by A5,A23,A39,A40,RELAT_1:38,XBOOLE_1:65
,YELLOW_0:def 15;
end;
end;
hence thesis;
end;
end;
A41: dom h = the carrier of L1 by A2,A21,A19,A22,YELLOW_0:def 15;
then
A42: for x be object st x in the carrier of L1 holds h.x in the carrier of L2
by A32,FUNCT_1:def 3;
A2 <> {} or B2 <> {} by A17,YELLOW_0:def 15;
then reconsider L2 as non empty RelStr by A5;
reconsider L1 as non empty RelStr by A16;
reconsider h as Function of L1,L2 by A41,A42,FUNCT_2:3;
A43: for x,y being Element of L1 holds x <= y iff h.x <= h.y
proof
let x,y be Element of L1;
A44: dom f misses dom g by A6,A21,A19,YELLOW_0:def 15;
per cases by A2,XBOOLE_0:def 3;
suppose
A45: x in A1 & y in A1;
then the carrier of subrelstr A2 <> {} by A7,Th4;
then reconsider A29 = A2 as non empty Subset of L2 by YELLOW_0:def 15;
reconsider A19 = A1 as non empty Subset of L1 by A45;
reconsider ax = x, ay = y as Element of subrelstr A19 by A45,
YELLOW_0:def 15;
reconsider f9 = f as Function of subrelstr A19, subrelstr A29;
A46: h.x = f.x & h.y = f.y by A1,A21,A20,A45,Th2,FUNCT_4:16;
hereby
assume x <= y;
then ax <= ay by YELLOW_0:60;
then f9.ax <= f9.ay by A7,WAYBEL_0:66;
hence h.x <= h.y by A46,YELLOW_0:59;
end;
assume h.x <= h.y;
then f9.ax <= f9.ay by A46,YELLOW_0:60;
then ax <= ay by A7,WAYBEL_0:66;
hence thesis by YELLOW_0:59;
end;
suppose
A47: x in A1 & y in B1;
hereby
the carrier of subrelstr A2 <> {} & the carrier of subrelstr
B2 <> {} by A7,A8,A47,Th4;
then reconsider A29 = A2, B29 = B2 as non empty Subset of L2 by
YELLOW_0:def 15;
reconsider A19 = A1, B19 = B1 as non empty Subset of L1 by A47;
assume x <= y;
reconsider f9 = f as Function of subrelstr A19, subrelstr A29;
reconsider g9 = g as Function of subrelstr B19, subrelstr B29;
reconsider ax = x as Element of subrelstr A19 by A47,YELLOW_0:def 15;
reconsider ay = y as Element of subrelstr B19 by A47,YELLOW_0:def 15;
f9.ax in the carrier of subrelstr A29;
then
A48: f9.ax in A29 by YELLOW_0:def 15;
g9.ay in the carrier of subrelstr B29;
then
A49: g9.ay in B29 by YELLOW_0:def 15;
f.x = h.x & g.y = h.y by A21,A20,A44,A47,FUNCT_4:13,16;
then h.x < h.y by A3,A48,A49;
hence h.x <= h.y by ORDERS_2:def 6;
end;
assume h.x <= h.y;
x < y by A1,A47;
hence thesis by ORDERS_2:def 6;
end;
suppose
A50: x in B1 & y in A1;
then the carrier of subrelstr B2 is non empty by A8,Th4;
then subrelstr B2 is non empty;
then
A51: rng g = the carrier of subrelstr B2 by A8,A50,WAYBEL_0:66;
g.x in rng g by A20,A50,FUNCT_1:def 3;
then
A52: g.x in B2 by A51,YELLOW_0:def 15;
the carrier of subrelstr A2 is non empty by A7,A50,Th4;
then subrelstr A2 is non empty;
then
A53: rng f = the carrier of subrelstr A2 by A7,A50,WAYBEL_0:66;
f.y in rng f by A21,A50,FUNCT_1:def 3;
then
A54: f.y in A2 by A53,YELLOW_0:def 15;
y < x by A1,A50;
hence x <= y implies h.x <= h.y by ORDERS_2:6;
assume
A55: h.x <= h.y;
g.x = h.x & f.y = h.y by A1,A21,A20,A50,Th2,FUNCT_4:13,16;
then h.x > h.y by A3,A52,A54;
hence thesis by A55,ORDERS_2:6;
end;
suppose
A56: x in B1 & y in B1;
then the carrier of subrelstr B2 <> {} by A8,Th4;
then reconsider B29 = B2 as non empty Subset of L2 by YELLOW_0:def 15;
reconsider B19 = B1 as non empty Subset of L1 by A56;
reconsider ax = x, ay = y as Element of subrelstr B19 by A56,
YELLOW_0:def 15;
reconsider g9 = g as Function of subrelstr B19, subrelstr B29;
A57: h.x = g.x & h.y = g.y by A20,A56,FUNCT_4:13;
hereby
assume x <= y;
then ax <= ay by YELLOW_0:60;
then g9.ax <= g9.ay by A8,WAYBEL_0:66;
hence h.x <= h.y by A57,YELLOW_0:59;
end;
assume h.x <= h.y;
then g9.ax <= g9.ay by A57,YELLOW_0:60;
then ax <= ay by A8,WAYBEL_0:66;
hence thesis by YELLOW_0:59;
end;
end;
h is one-to-one
proof
let x1,x2 be Element of L1;
assume
A58: h.x1 = h.x2;
per cases by A2,XBOOLE_0:def 3;
suppose
A59: x1 in A1 & x2 in A1;
then not x1 in B1 by A6,XBOOLE_0:3;
then
A60: h.x1 = f.x1 by A20,FUNCT_4:11;
the carrier of subrelstr A2 <> {} by A7,A59,Th4;
then
A61: subrelstr A2 is non empty;
not x2 in B1 by A6,A59,XBOOLE_0:3;
then f.x1 = f.x2 by A20,A58,A60,FUNCT_4:11;
hence thesis by A7,A21,A59,A61,FUNCT_1:def 4;
end;
suppose
A62: x1 in A1 & x2 in B1;
then the carrier of subrelstr A2 <> {} by A7,Th4;
then subrelstr A2 is non empty;
then rng f = the carrier of subrelstr A2 by A7,A62,WAYBEL_0:66;
then
A63: rng f = A2 by YELLOW_0:def 15;
not x1 in B1 by A6,A62,XBOOLE_0:3;
then h.x2 = f.x1 by A20,A58,FUNCT_4:11;
then
A64: h.x2 in rng f by A21,A62,FUNCT_1:def 3;
h.x2 = g.x2 by A20,A62,FUNCT_4:13;
then
A65: h.x2 in rng g by A20,A62,FUNCT_1:def 3;
the carrier of subrelstr B2 <> {} by A8,A62,Th4;
then subrelstr B2 is non empty;
then rng g = the carrier of subrelstr B2 by A8,A62,WAYBEL_0:66;
then rng f misses rng g by A4,A63,YELLOW_0:def 15;
hence thesis by A64,A65,XBOOLE_0:3;
end;
suppose
A66: x1 in B1 & x2 in A1;
then not x2 in dom g by A6,A20,XBOOLE_0:3;
then h.x2 = f.x2 by FUNCT_4:11;
then
A67: h.x2 in rng f by A21,A66,FUNCT_1:def 3;
the carrier of subrelstr B2 <> {} by A8,A66,Th4;
then subrelstr B2 is non empty;
then
A68: rng g = the carrier of subrelstr B2 by A8,A66,WAYBEL_0:66;
h.x2 = g.x1 by A20,A58,A66,FUNCT_4:13;
then
A69: h.x2 in rng g by A20,A66,FUNCT_1:def 3;
the carrier of subrelstr A2 <> {} by A7,A66,Th4;
then subrelstr A2 is non empty;
then rng f = the carrier of subrelstr A2 by A7,A66,WAYBEL_0:66
.= A2 by YELLOW_0:def 15;
then rng f misses rng g by A4,A68,YELLOW_0:def 15;
hence thesis by A69,A67,XBOOLE_0:3;
end;
suppose
A70: x1 in B1 & x2 in B1;
then the carrier of subrelstr B2 <> {} by A8,Th4;
then
A71: subrelstr B2 is non empty;
h.x1 = g.x1 by A20,A70,FUNCT_4:13;
then g.x1 = g.x2 by A20,A58,A70,FUNCT_4:13;
hence thesis by A8,A20,A70,A71,FUNCT_1:def 4;
end;
end;
then h is isomorphic by A32,A43,WAYBEL_0:66;
hence thesis;
end;
end;
theorem
for A being finite Chain, n being Nat st card(the carrier of A) = n
holds A,InclPoset n are_isomorphic
proof
defpred P[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 P[n] holds P[n + 1]
proof
let n be Nat;
assume
A2: for A being finite Chain st card(the carrier of A) = n holds A,
InclPoset(n) are_isomorphic;
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;
assume
A4: card(the carrier of A) = n + 1;
then reconsider A as non empty finite Chain;
set b = Top A;
per cases by A3,NAT_1:13;
suppose
A5: n + 1 = 1;
then consider x be object such that
A6: the carrier of A = {x} by A4,CARD_2:42;
A,InclPoset(1) are_isomorphic
proof
set g = (the carrier of A) --> 0;
A7: rng g = {0} by FUNCOP_1:8;
A8: {0} = the carrier of InclPoset 1 by CARD_1:49,YELLOW_1:1;
then reconsider g as
Function of A, InclPoset 1;
A9: for e,f being Element of A holds e <= f iff g.e <= g.f
proof
let e,f be Element of A;
hereby
assume e <= f;
g.e = 0 by FUNCOP_1:7;
hence g.e <= g.f by FUNCOP_1:7;
end;
assume g.e <= g.f;
e = x by A6,TARSKI:def 1;
hence thesis by A6,TARSKI:def 1;
end;
g is one-to-one
proof
let x1,x2 be Element of A;
assume g.x1 = g.x2;
x1 = x by A6,TARSKI:def 1;
hence thesis by A6,TARSKI:def 1;
end;
then g is isomorphic by A7,A8,A9,WAYBEL_0:66;
hence thesis;
end;
hence thesis by A5;
end;
suppose
A10: n + 1 > 1;
A11: card((the carrier of A) \ {b}) = (card the carrier of A) - card {b}
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)\{b} 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 be Function of B,InclPoset(n) such that
A12: f is isomorphic;
the carrier of B = (the carrier of A)\{b} by YELLOW_0:def 15;
then
A13: (the carrier of B) , { b } 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 {b};
A15: the carrier of subrelstr n9 = n9 by YELLOW_0:def 15;
{b} c= {b};
then reconsider b9 = {b} as non empty Subset of X by YELLOW_1:1;
set X9 = subrelstr b9;
set g = (the carrier of X9) --> n;
dom g = the carrier of X9 by FUNCOP_1:13;
then reconsider g as ManySortedSet of the carrier of X9 by PARTFUN1:def 2
;
A16: for a,b be Element of InclPoset(n+1) st a in (the carrier of
InclPoset(n)) & b in {n} holds a < b
proof
let a,b be Element of InclPoset(n+1);
assume that
A17: a in the carrier of InclPoset(n) and
A18: b in {n};
A19: a in n by A17,YELLOW_1:1;
then a in { i where i is Nat: i < n } by AXIOMS:4;
then consider h be Nat such that
A20: h = a and
A21: h < n;
A22: b = n by A18,TARSKI:def 1;
a c= b
proof
assume not a c= b;
then consider x be object such that
A23: x in a and
A24: not x in b;
x in { w where w is Nat: w < h } by A20,A23,AXIOMS:4;
then consider w9 be Nat such that
A25: w9 = x and
A26: w9 < h;
w9 < n by A21,A26,XXREAL_0:2;
then w9 in { t where t is Nat: t < n};
hence contradiction by A22,A24,A25,AXIOMS:4;
end;
then
A27: a <= b by YELLOW_1:3;
a <> b by A19,A22;
hence thesis by A27,ORDERS_2:def 6;
end;
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 {b } = {b} by YELLOW_0:def 15;
A30: the carrier of X9 = {b} by YELLOW_0:def 15;
then reconsider g as Function of subrelstr {b}, subrelstr n9 by A15,A29;
g.b in n9 by A15,A29,FUNCT_2:47;
then g.b = 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 {b} holds e <= f iff g.e <= g.f
proof
let e,f be Element of subrelstr {b};
reconsider f1=f as Element of X9 by A30,YELLOW_0:def 15;
reconsider e1=e as Element of X9 by A30,YELLOW_0:def 15;
hereby
assume e <= f;
g.e1 = n & g.f1 = n by FUNCOP_1:7;
hence g.e <= g.f;
end;
assume g.e <= g.f;
e in the carrier of subrelstr {b};
then e in {b} by YELLOW_0:def 15;
then
A33: e = b by TARSKI:def 1;
f in the carrier of subrelstr {b};
then f in {b} by YELLOW_0:def 15;
hence thesis by A33,TARSKI:def 1;
end;
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 be Function of A,InclPoset(n+1) st h = f +* g & h is isomorphic
by A12,A13,A28,A34,A35,Th5;
hence thesis;
end;
end;
A36: P[ 0 ]
proof
let A be finite Chain;
set f = the Function of A, InclPoset 0;
assume card(the carrier of A) = 0;
then
A37: A is empty;
take f;
InclPoset(0) is empty by YELLOW_1:1;
hence thesis by A37,WAYBEL_0:def 38;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A36,A1);
hence thesis;
end;