:: Dickson's lemma
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received March 12, 2002
:: Copyright (c) 2002-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 FUNCT_1, RELAT_1, FUNCOP_1, NAT_1, TARSKI, ARYTM_3, XBOOLE_0,
SUBSET_1, NUMBERS, XXREAL_0, FINSET_1, CARD_1, ORDERS_2, REARRAN1,
RELAT_2, STRUCT_0, WELLORD1, WAYBEL_4, WAYBEL20, EQREL_1, ORDERS_1,
ZFMISC_1, WELLFND1, SETFAM_1, VALUED_0, ORDINAL2, MCART_1, CAT_1,
YELLOW_1, PBOOLE, CARD_3, RLVECT_2, YELLOW_6, WAYBEL_3, FUNCT_4,
YELLOW_3, DICKSON, XCMPLX_0, WELLORD2, ORDINAL1, PARTFUN1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
PBOOLE, RELSET_1, XXREAL_2, SEQ_4, PARTFUN1, FUNCT_2, CARD_3, ORDINAL1,
XCMPLX_0, NAT_1, STRUCT_0, RELAT_2, XXREAL_0, FUNCT_4, FUNCOP_1,
DOMAIN_1, FINSET_1, XTUPLE_0, MCART_1, WELLORD1, WELLORD2,
ORDERS_2, ORDERS_1,
EQREL_1, WELLFND1, WAYBEL_0, CARD_1, NUMBERS, WAYBEL_4, VALUED_0,
PRALG_1, YELLOW_3, WAYBEL_1, YELLOW_1, WAYBEL_3, YELLOW_6;
constructors WELLORD1, DOMAIN_1, PRALG_1, ORDERS_3, WAYBEL_1, YELLOW_3,
WAYBEL_3, WAYBEL_4, WELLFND1, SEQ_4, RELSET_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FUNCOP_1, FINSET_1, XXREAL_0, NAT_1, MEMBERED, EQREL_1, PRE_CIRC,
STRUCT_0, ORDERS_2, YELLOW_1, YELLOW_3, WAYBEL18, WAYBEL_3, VALUED_0,
CARD_1, XXREAL_2, CARD_3, ZFMISC_1, RELSET_1, XTUPLE_0;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, RELAT_2, ORDERS_1;
equalities FUNCOP_1, ORDINAL1, NAT_1;
expansions TARSKI, RELAT_2, ORDERS_2, ORDERS_1;
theorems WELLORD1, ORDERS_1, SUBSET_1, TARSKI, RELAT_1, RELAT_2, RELSET_1,
ZFMISC_1, EQREL_1, WAYBEL_0, ORDERS_2, NAT_1, FUNCT_1, FUNCT_2, CARD_2,
CARD_1, NORMSP_1, SEQM_3, FINSET_1, AXIOMS, YELLOW_3, WAYBEL_1, WAYBEL20,
YELLOW_1, CARD_3, FUNCOP_1, WAYBEL_3, MCART_1, FUNCT_4, WELLFND1,
WAYBEL_4, PRALG_1, YELLOW_6, AFINSQ_1, XBOOLE_0, XBOOLE_1, PARTFUN1,
XXREAL_0, ORDINAL1, XXREAL_2, VALUED_0, XTUPLE_0, NUMBERS, TAXONOM1,
WELLORD2;
schemes PRE_CIRC, RECDEF_1, NAT_1, FUNCT_2, DOMAIN_1, FRAENKEL, FINSEQ_1,
FUNCT_1, RELSET_1;
begin :: Preliminaries
theorem Th1:
for g being Function, x being set st dom g = {x} holds g = x .--> g.x
proof
let g be Function, x be set such that
A1: dom g = {x};
now
let a,b be object;
A2: dom (x .-->g.x) = {x};
hereby
assume
A3: [a,b] in g;
then
A4: a in {x} by A1,FUNCT_1:1;
then
A5: a = x by TARSKI:def 1;
then b = g.x by A3,FUNCT_1:1;
then (x.-->g.x).a = b by A5,FUNCOP_1:72;
hence [a,b] in x.-->g.x by A2,A4,FUNCT_1:1;
end;
assume
A6: [a,b] in x.-->g.x;
then
A7: a in {x} by A2,FUNCT_1:1;
then
A8: a = x by TARSKI:def 1;
b = (x.-->g.x).a by A6,FUNCT_1:1
.= g.a by A8,FUNCOP_1:72;
hence [a,b] in g by A1,A7,FUNCT_1:1;
end;
hence thesis by RELAT_1:def 2;
end;
::$CT
theorem Th2:
for X being infinite set ex f being sequence of X st f is one-to-one
proof
let X be infinite set;
card NAT c= card X by CARD_3:85;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = NAT and
A3: rng f c= X by CARD_1:10;
for x being object st x in NAT holds f.x in X by A3,A2,FUNCT_1:3;
then reconsider f as sequence of X by A2,FUNCT_2:3;
take f;
thus thesis by A1;
end;
definition
let R be RelStr, f be sequence of R;
attr f is ascending means
for n being Element of NAT
holds f.(n+1) <> f.n & [f.n, f.(n+1)] in the InternalRel of R;
end;
definition
let R be RelStr, f be sequence of R;
attr f is weakly-ascending means
for n being Nat holds [f.n, f.(n+1)] in the InternalRel of R;
end;
theorem Th3:
for R being non empty transitive RelStr, f being sequence of R
st f is weakly-ascending
for i,j being Nat st i < j holds f.i <= f.j
proof
let R be non empty transitive RelStr, f be sequence of R such that
A1: f is weakly-ascending;
let i be Nat;
defpred P[Nat] means i < $1 implies f.i <= f.$1;
A2: P[ 0 ] by NAT_1:2;
A3: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat such that
A4: P[j] and
A5: i < j+1;
reconsider fj1 = f.(j+1) as Element of R;
A6: [f.j, f.(j+1)] in the InternalRel of R by A1;
then
A7: f.j <= fj1;
A8: i <= j by A5,NAT_1:13;
per cases by A8,XXREAL_0:1;
suppose i < j;
hence thesis by A4,A7,ORDERS_2:3;
end;
suppose i = j;
hence thesis by A6;
end;
end;
thus for j being Nat holds P[j] from NAT_1:sch 2(A2,A3);
end;
theorem Th4:
for R being non empty RelStr holds R is connected iff
the InternalRel of R is_strongly_connected_in the carrier of R
proof
let R be non empty RelStr;
set IR = the InternalRel of R, CR = the carrier of R;
hereby
assume
A1: R is connected;
now
let x, y be object such that
A2: x in CR and
A3: y in CR;
reconsider x9=x, y9=y as Element of R by A2,A3;
x9 <= y9 or y9 <= x9 by A1,WAYBEL_0:def 29;
hence [x,y] in IR or [y,x] in IR;
end;
hence IR is_strongly_connected_in CR;
end;
assume IR is_strongly_connected_in CR;
then for x, y be Element of R holds x <= y or y <= x;
hence thesis by WAYBEL_0:def 29;
end;
theorem Th5:
for L being RelStr, Y being set, a being set
holds (the InternalRel of L)-Seg(a) misses Y & a in Y iff
a is_minimal_wrt Y, the InternalRel of L
proof
let L be RelStr, Y be set, a be set;
set IR = the InternalRel of L;
hereby
assume that
A1: IR-Seg(a) misses Y and
A2: a in Y;
A3: IR-Seg(a) /\ Y = {} by A1,XBOOLE_0:def 7;
now
assume ex y being set st y in Y & y<>a & [y,a] in IR;
then consider y being set such that
A4: y in Y and
A5: y <> a and
A6: [y,a] in IR;
y in IR-Seg(a) by A5,A6,WELLORD1:1;
hence contradiction by A3,A4,XBOOLE_0:def 4;
end;
hence a is_minimal_wrt Y, IR by A2,WAYBEL_4:def 25;
end;
assume
A7: a is_minimal_wrt Y, IR;
now
assume not IR-Seg(a) misses Y;
then IR-Seg(a) /\ Y <> {} by XBOOLE_0:def 7;
then consider y being object such that
A8: y in IR-Seg(a) /\ Y by XBOOLE_0:def 1;
A9: y in IR-Seg(a) by A8,XBOOLE_0:def 4;
A10: y in Y by A8,XBOOLE_0:def 4;
A11: y <> a by A9,WELLORD1:1;
[y,a] in IR by A9,WELLORD1:1;
hence contradiction by A7,A10,A11,WAYBEL_4:def 25;
end;
hence IR-Seg(a) misses Y;
thus thesis by A7,WAYBEL_4:def 25;
end;
theorem Th6:
for L being non empty transitive antisymmetric RelStr,
x being Element of L, a, N being set
st a is_minimal_wrt (the InternalRel of L)-Seg(x) /\ N,(the InternalRel of L)
holds a is_minimal_wrt N, (the InternalRel of L)
proof
let L be non empty transitive antisymmetric RelStr,
x be Element of L, a,N be set such that
A1: a
is_minimal_wrt (the InternalRel of L)-Seg(x) /\ N,(the InternalRel of L);
set IR = the InternalRel of L, CR = the carrier of L;
A2: IR is_transitive_in CR by ORDERS_2:def 3;
now
A3: a in IR-Seg(x) /\ N by A1,WAYBEL_4:def 25;
then
A4: a in IR-Seg(x) by XBOOLE_0:def 4;
then
A5: a <> x by WELLORD1:1;
A6: [a,x] in IR by A4,WELLORD1:1;
then reconsider a9 = a as Element of L by ZFMISC_1:87;
thus a in N by A3,XBOOLE_0:def 4;
now
assume ex y being set st y in N & y <> a & [y,a] in IR;
then consider y being set such that
A7: y in N and
A8: y <> a and
A9: [y,a] in IR;
A10: a in CR by A9,ZFMISC_1:87;
y in CR by A9,ZFMISC_1:87;
then
A11: [y,x] in IR by A2,A6,A9,A10;
per cases;
suppose x = y;
then
A12: x <= a9 by A9;
a9 <= x by A6;
hence contradiction by A5,A12,ORDERS_2:2;
end;
suppose x <> y;
then y in IR-Seg(x) by A11,WELLORD1:1;
then y in IR-Seg(x) /\ N by A7,XBOOLE_0:def 4;
hence contradiction by A1,A8,A9,WAYBEL_4:def 25;
end;
end;
hence not ex y being set st y in N & y <> a & [y,a] in IR;
end;
hence thesis by WAYBEL_4:def 25;
end;
begin :: Chapter 4.2
definition
let R be RelStr; :: Def 4.19 (ix)
attr R is quasi_ordered means
R is reflexive transitive;
end;
definition :: Lemma 4.24.i
let R be RelStr such that
A1: R is quasi_ordered;
func EqRel R -> Equivalence_Relation of the carrier of R equals
:Def4:
(the InternalRel of R) /\ (the InternalRel of R)~;
coherence
proof
set IR = the InternalRel of R, CR = the carrier of R;
R is reflexive by A1;
then
A2: IR is_reflexive_in CR;
R is transitive by A1;
then
A3: IR is_transitive_in CR;
then
A4: IR quasi_orders CR by A2;
A5: IR /\ IR~ is_reflexive_in CR
proof
let x be object;
assume x in CR;
then
A6: [x,x] in IR by A2;
then [x,x] in IR~ by RELAT_1:def 7;
hence thesis by A6,XBOOLE_0:def 4;
end;
then
A7: dom(IR /\ IR~) = CR by ORDERS_1:13;
A8: field(IR /\ IR~) = CR by A5,ORDERS_1:13;
A9: IR /\ IR~ is_symmetric_in CR
proof
let x,y be object such that x in CR and y in CR and
A10: [x,y] in IR /\ IR~;
A11: [x,y] in IR by A10,XBOOLE_0:def 4;
A12: [x,y] in IR~ by A10,XBOOLE_0:def 4;
A13: [y,x] in IR~ by A11,RELAT_1:def 7;
[y,x] in IR by A12,RELAT_1:def 7;
hence thesis by A13,XBOOLE_0:def 4;
end;
IR /\ IR~ is_transitive_in CR
proof
let x, y, z be object such that
A14: x in CR and
A15: y in CR and
A16: z in CR and
A17: [x,y] in IR /\ IR~ and
A18: [y,z] in IR /\ IR~;
A19: [x,y] in IR by A17,XBOOLE_0:def 4;
A20: [x,y] in IR~ by A17,XBOOLE_0:def 4;
A21: [y,z] in IR by A18,XBOOLE_0:def 4;
A22: [y,z] in IR~ by A18,XBOOLE_0:def 4;
A23: [x,z] in IR by A3,A14,A15,A16,A19,A21;
IR~ quasi_orders CR by A4,ORDERS_1:40;
then IR~ is_transitive_in CR;
then [x,z] in IR~ by A14,A15,A16,A20,A22;
hence thesis by A23,XBOOLE_0:def 4;
end;
hence thesis by A7,A8,A9,PARTFUN1:def 2,RELAT_2:def 11,def 16;
end;
end;
theorem Th7:
for R being RelStr, x,y being Element of R
st R is quasi_ordered holds x in Class(EqRel R, y) iff x <= y & y <= x
proof
let R be RelStr, x,y be Element of R such that
A1: R is quasi_ordered;
set IR = the InternalRel of R;
hereby
assume x in Class(EqRel R,y);
then [x,y] in EqRel R by EQREL_1:19;
then
A2: [x,y] in IR /\ IR~ by A1,Def4;
then
A3: [x,y] in IR by XBOOLE_0:def 4;
A4: [x,y] in IR~ by A2,XBOOLE_0:def 4;
thus x <= y by A3;
[y,x] in IR by A4,RELAT_1:def 7;
hence y <= x;
end;
assume that
A5: x <= y and
A6: y <= x;
A7: [y,x] in IR by A6;
A8: [x,y] in IR by A5;
[x,y] in IR~ by A7,RELAT_1:def 7;
then [x,y] in IR /\ IR~ by A8,XBOOLE_0:def 4;
then [x,y] in EqRel R by A1,Def4;
hence thesis by EQREL_1:19;
end;
definition :: Lemma 4.24, (the InternalRel of R) / EqRel R
let R be RelStr;
func <=E R -> Relation of Class EqRel R means
:Def5:
for A, B being object holds [A,B] in it iff ex a, b being Element of R
st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b;
existence
proof
set IR = the InternalRel of R, CR = the carrier of R;
per cases;
suppose
A1: CR = {};
reconsider IT = {} as Relation of Class(EqRel R) by RELSET_1:12;
take IT;
let A, B be object;
thus [A,B] in IT implies ex a, b being Element of R
st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b;
given a, b being Element of R such that
A = Class(EqRel R, a) and B = Class(EqRel R, b) and
A2: a <= b;
IR = {} by A1;
hence thesis by A2;
end;
suppose CR is non empty;
then reconsider R9 = R as non empty RelStr;
set IT = {[Class(EqRel R, a), Class(EqRel R, b)]
where a,b is Element of R9 : a <= b};
set Y = Class(EqRel R);
IT c= [:Y,Y:]
proof
let x be object;
assume x in IT;
then consider a, b being Element of R9 such that
A3: x = [Class(EqRel R, a), Class(EqRel R, b)] and a <= b;
A4: Class(EqRel R, a) in Y by EQREL_1:def 3;
Class(EqRel R, b) in Y by EQREL_1:def 3;
hence thesis by A3,A4,ZFMISC_1:def 2;
end;
then reconsider IT as Relation of Class(EqRel R);
take IT;
let A, B be object;
hereby
assume [A,B] in IT;
then consider a,b being Element of R such that
A5: [A,B] = [Class(EqRel R, a), Class(EqRel R, b)] and
A6: a <= b;
reconsider a9 = a, b9 = b as Element of R;
take a9, b9;
thus A = Class(EqRel R, a9) & B = Class(EqRel R, b9) &
a9 <= b9 by A5,A6,XTUPLE_0:1;
end;
given a, b being Element of R such that
A7: A = Class(EqRel R, a) and
A8: B = Class(EqRel R, b) and
A9: a <= b;
thus thesis by A7,A8,A9;
end;
end;
uniqueness
proof
let IT1, IT2 be Relation of Class(EqRel R) such that
A10: for A, B being object
holds [A,B] in IT1 iff ex a, b being Element of R
st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b and
A11: for A, B being object
holds [A,B] in IT2 iff ex a, b being Element of R
st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b;
now
let x be object;
hereby
assume
A12: x in IT1;
set Y = Class(EqRel R);
consider A, B being object such that A in Y and B in Y and
A13: x = [A,B] by A12,ZFMISC_1:def 2;
ex a, b being Element of R st ( A = Class(EqRel R, a))&( B =
Class(EqRel R, b))&( a <= b) by A10,A12,A13;
hence x in IT2 by A11,A13;
end;
assume
A14: x in IT2;
set Y = Class(EqRel R);
consider A, B being object such that A in Y and B in Y and
A15: x = [A,B] by A14,ZFMISC_1:def 2;
ex a, b being Element of R st ( A = Class(EqRel R, a))&( B =
Class(EqRel R, b))&( a <= b) by A11,A14,A15;
hence x in IT1 by A10,A15;
end;
hence IT1 = IT2 by TARSKI:2;
end;
end;
theorem Th8: :: Lemma 4.24.ii
for R being RelStr
st R is quasi_ordered holds <=E R partially_orders Class(EqRel R)
proof
let R be RelStr;
set CR = the carrier of R;
set IR = the InternalRel of R;
assume
A1: R is quasi_ordered;
then R is transitive;
then
A2: IR is_transitive_in CR;
thus <=E R is_reflexive_in Class(EqRel R)
proof
let x be object;
assume x in Class(EqRel R);
then consider a being object such that
A3: a in CR and
A4: x = Class(EqRel R,a) by EQREL_1:def 3;
R is reflexive by A1;
then IR is_reflexive_in CR;
then
A5: [a,a] in IR by A3;
reconsider a9= a as Element of R by A3;
a9 <= a9 by A5;
hence thesis by A4,Def5;
end;
thus <=E R is_transitive_in Class(EqRel R)
proof
let x,y,z be object such that
A6: x in Class(EqRel R) and y in Class(EqRel R)
and z in Class(EqRel R) and
A7: [x,y] in <=E R and
A8: [y,z] in <=E R;
consider a,b being Element of R such that
A9: x = Class(EqRel R, a) and
A10: y = Class(EqRel R, b) and
A11: a <= b by A7,Def5;
consider c,d being Element of R such that
A12: y = Class(EqRel R,c) and
A13: z = Class(EqRel R,d) and
A14: c <= d by A8,Def5;
A15: [a,b] in IR by A11;
A16: [c,d] in IR by A14;
A17: ex x1 being object st ( x1 in CR)&( x = Class(EqRel R, x1)) by A6,
EQREL_1:def 3;
then b in Class(EqRel R, c) by A10,A12,EQREL_1:23;
then [b,c] in EqRel R by EQREL_1:19;
then [b,c] in IR/\ IR~ by A1,Def4;
then [b,c] in IR by XBOOLE_0:def 4;
then [a,c] in IR by A2,A15,A17;
then [a,d] in IR by A2,A16,A17;
then a<=d;
hence thesis by A9,A13,Def5;
end;
thus <=E R is_antisymmetric_in Class(EqRel R)
proof
let x,y be object such that
A18: x in Class(EqRel R) and y in Class(EqRel R) and
A19: [x,y] in <=E R and
A20: [y,x] in <=E R;
consider a,b being Element of R such that
A21: x = Class(EqRel R, a) and
A22: y = Class(EqRel R, b) and
A23: a <= b by A19,Def5;
consider c,d being Element of R such that
A24: y = Class(EqRel R, c) and
A25: x = Class(EqRel R, d) and
A26: c <= d by A20,Def5;
A27: [a,b] in IR by A23;
A28: [c,d] in IR by A26;
A29: ex x1 being object st ( x1 in CR)&( x = Class(EqRel R, x1)) by A18,
EQREL_1:def 3;
then
A30: d in Class(EqRel R, a) by A21,A25,EQREL_1:23;
a in Class(EqRel R, a) by A29,EQREL_1:20;
then
A31: [a,d] in EqRel R by A30,EQREL_1:22;
A32: c in Class(EqRel R, b) by A22,A24,A29,EQREL_1:23;
b in Class(EqRel R, b) by A29,EQREL_1:20;
then
A33: [b,c] in EqRel R by A32,EQREL_1:22;
[a,d] in IR /\ IR~ by A1,A31,Def4;
then [a,d] in IR~ by XBOOLE_0:def 4;
then
A34: [d,a] in IR by RELAT_1:def 7;
[b,c] in IR /\ IR~ by A1,A33,Def4;
then [b,c] in IR by XBOOLE_0:def 4;
then [b,d] in IR by A2,A28,A29;
then
A35: [b,a] in IR by A2,A29,A34;
[b,a] in IR~ by A27,RELAT_1:def 7;
then [b,a] in IR /\ IR~ by A35,XBOOLE_0:def 4;
then [b,a] in EqRel R by A1,Def4;
then b in Class(EqRel R, a) by EQREL_1:19;
hence thesis by A21,A22,EQREL_1:23;
end;
end;
theorem ::Lemma 4.24.iii
for R being non empty RelStr st R is quasi_ordered & R is connected
holds <=E R linearly_orders Class(EqRel R)
proof
let R be non empty RelStr such that
A1: R is quasi_ordered and
A2: R is connected;
A3: <=E R partially_orders Class(EqRel R) by A1,Th8;
hence <=E R is_reflexive_in Class(EqRel R);
thus <=E R is_transitive_in Class(EqRel R) by A3;
thus <=E R is_antisymmetric_in Class(EqRel R) by A3;
thus <=E R is_connected_in Class(EqRel R)
proof
set CR = the carrier of R;
let x, y be object such that
A4: x in Class(EqRel R) and
A5: y in Class(EqRel R) and x <> y and
A6: not [x,y] in <=E R;
consider a being object such that
A7: a in CR and
A8: x = Class(EqRel R, a) by A4,EQREL_1:def 3;
consider b being object such that
A9: b in CR and
A10: y = Class(EqRel R, b) by A5,EQREL_1:def 3;
reconsider a9=a,b9=b as Element of R by A7,A9;
not a9 <= b9 by A6,A8,A10,Def5;
then b9 <= a9 by A2,WAYBEL_0:def 29;
hence thesis by A8,A10,Def5;
end;
end;
definition :: "strict part" of a relation, p. 155
let R be Relation;
func R\~ -> Relation equals
R \ R~;
correctness;
end;
registration
let R be Relation;
cluster R \~ -> asymmetric;
coherence
proof
now
let x,y be object such that x in field (R\~) and
y in field (R\~) and
A1: [x,y] in R\~;
not [x,y] in R~ by A1,XBOOLE_0:def 5;
hence not [y,x] in R\~ by RELAT_1:def 7;
end;
then R \~ is_asymmetric_in field (R\~);
hence thesis;
end;
end;
definition
let X be set, R be Relation of X;
redefine func R\~ -> Relation of X; :: redefines \~ (DICKSON, definition)
coherence
proof
R\~ = R \ R~;
hence thesis;
end;
end;
definition
let R be RelStr;
func R\~ -> strict RelStr equals
RelStr(# the carrier of R, (the InternalRel of R)\~ #);
correctness;
end;
registration
let R be non empty RelStr;
cluster R\~ -> non empty;
coherence;
end;
registration
let R be transitive RelStr;
cluster R\~ -> transitive;
coherence
proof
set IR = the InternalRel of R, CR = the carrier of R;
set IR9= the InternalRel of R\~, CR9 = the carrier of R\~;
A1: IR is_transitive_in CR by ORDERS_2:def 3;
now
let x,y,z be object such that
A2: x in CR9 and
A3: y in CR9 and
A4: z in CR9 and
A5: [x,y] in IR9 and
A6: [y,z] in IR9;
A7: not [x,y] in IR~ by A5,XBOOLE_0:def 5;
A8: [x,z] in IR by A1,A2,A3,A4,A5,A6;
now
assume [x,z] in IR~;
then [z, x] in IR by RELAT_1:def 7;
then [y, x] in IR by A1,A2,A3,A4,A6;
hence contradiction by A7,RELAT_1:def 7;
end;
hence [x,z] in IR9 by A8,XBOOLE_0:def 5;
end;
then IR9 is_transitive_in CR9;
hence thesis;
end;
end;
registration
let R be RelStr;
cluster R\~ -> antisymmetric;
coherence
proof
set IR = the InternalRel of R;
set IR9= the InternalRel of R\~, CR9 = the carrier of R\~;
now
let x, y be object such that x in CR9 and y in CR9 and
A1: [x,y] in IR9 and
A2: [y,x] in IR9;
not [x,y] in IR~ by A1,XBOOLE_0:def 5;
hence x = y by A2,RELAT_1:def 7;
end;
then IR9 is_antisymmetric_in CR9;
hence thesis;
end;
end;
theorem ::Exercise 4.27:
for R being non empty Poset, x being Element of R
holds Class(EqRel R, x) = {x}
proof
let R be non empty Poset;
set IR = the InternalRel of R, CR = the carrier of R;
let x be Element of CR;
A1: R is quasi_ordered;
A2: IR is_antisymmetric_in CR by ORDERS_2:def 4;
now
let z be object;
hereby
assume z in Class(EqRel R, x);
then [z,x] in EqRel R by EQREL_1:19;
then
A3: [z,x] in IR /\ IR~ by A1,Def4;
then
A4: [z,x] in IR by XBOOLE_0:def 4;
[z,x] in IR~ by A3,XBOOLE_0:def 4;
then
A5: [x,z] in IR by RELAT_1:def 7;
z in dom IR by A4,XTUPLE_0:def 12;
then z = x by A2,A4,A5;
hence z in {x} by TARSKI:def 1;
end;
assume z in {x};
then z = x by TARSKI:def 1;
hence z in Class(EqRel R, x) by EQREL_1:20;
end;
hence thesis by TARSKI:2;
end;
theorem :: Exercise 4.29.i
for R being Relation holds R = R\~ iff R is asymmetric
proof
let R be Relation;
thus R = R\~ implies R is asymmetric;
assume R is asymmetric;
then
A1: R is_asymmetric_in field R;
now
let a,b be object;
hereby
assume
A2: [a,b] in R;
then
A3: a in field R by RELAT_1:15;
b in field R by A2,RELAT_1:15;
then not [b,a] in R by A1,A2,A3;
then not [a,b] in R~ by RELAT_1:def 7;
hence [a,b] in R\~ by A2,XBOOLE_0:def 5;
end;
assume [a,b] in R\~;
hence [a,b] in R;
end;
hence thesis by RELAT_1:def 2;
end;
theorem :: Exercise 4.29.ii
for R being Relation st R is transitive holds R\~ is transitive
proof
let R be Relation;
assume R is transitive;
then
A1: R is_transitive_in field R;
now
let x, y, z be object such that
x in field (R\~) and y in field (R\~)
and z in field (R\~) and
A2: [x,y] in R\~ and
A3: [y,z] in R\~;
A4: x in field R by A2,RELAT_1:15;
A5: y in field R by A2,RELAT_1:15;
A6: z in field R by A3,RELAT_1:15;
then
A7: [x,z] in R by A1,A2,A3,A4,A5;
not [x,y] in R~ by A2,XBOOLE_0:def 5;
then not [y,x] in R by RELAT_1:def 7;
then not [z,x] in R by A1,A3,A4,A5,A6;
then not [x,z] in R~ by RELAT_1:def 7;
hence [x,z] in R\~ by A7,XBOOLE_0:def 5;
end;
then R\~ is_transitive_in field (R\~);
hence thesis;
end;
theorem :: Exercise 4.29.iii
for R being Relation, a, b being set st R is antisymmetric
holds [a,b] in R\~ iff [a,b] in R & a <> b
proof
let R be Relation, a, b be set;
assume R is antisymmetric;
then
A1: R is_antisymmetric_in field R;
A2: R\~ is_asymmetric_in field (R\~) by RELAT_2:def 13;
hereby
assume
A3: [a,b] in R\~;
hence [a,b] in R;
now
assume
A4: a = b;
a in field (R\~) by A3,RELAT_1:15;
hence contradiction by A2,A3,A4;
end;
hence a <> b;
end;
assume that
A5: [a,b] in R and
A6: a <> b;
A7: a in field R by A5,RELAT_1:15;
b in field R by A5,RELAT_1:15;
then not [b,a] in R by A1,A5,A6,A7;
then not [a,b] in R~ by RELAT_1:def 7;
hence thesis by A5,XBOOLE_0:def 5;
end;
theorem Th14: :: Exercise 4.29 (addition)
for R being RelStr st R is well_founded holds R\~ is well_founded
proof
let R be RelStr such that
A1: R is well_founded;
set IR = the InternalRel of R, CR = the carrier of R;
set IR9 = the InternalRel of R\~, CR9 = the carrier of R\~;
A2: IR is_well_founded_in CR by A1,WELLFND1:def 2;
now
let Y be set such that
A3: Y c= CR9 and
A4: Y <> {};
consider a being object such that
A5: a in Y and
A6: IR-Seg(a) misses Y by A2,A3,A4,WELLORD1:def 3;
A7: IR-Seg(a) /\ Y = {} by A6,XBOOLE_0:def 7;
take a;
thus a in Y by A5;
now
given z being object such that
A8: z in IR9-Seg(a) /\ Y;
A9: z in IR9-Seg(a) by A8,XBOOLE_0:def 4;
A10: z in Y by A8,XBOOLE_0:def 4;
A11: z <> a by A9,WELLORD1:1;
[z,a] in IR9 by A9,WELLORD1:1;
then z in IR-Seg(a) by A11,WELLORD1:1;
hence contradiction by A7,A10,XBOOLE_0:def 4;
end;
then IR9-Seg(a) /\ Y = {} by XBOOLE_0:def 1;
hence IR9-Seg(a) misses Y by XBOOLE_0:def 7;
end;
then IR9 is_well_founded_in CR9 by WELLORD1:def 3;
hence thesis by WELLFND1:def 2;
end;
theorem Th15: :: Exercise 4.29 (addition)
for R being RelStr
st R\~ is well_founded & R is antisymmetric holds R is well_founded
proof
let R be RelStr such that
A1: R\~ is well_founded and
A2: R is antisymmetric;
set IR = the InternalRel of R, CR = the carrier of R;
set IR9 = the InternalRel of R\~;
A3: IR is_antisymmetric_in CR by A2;
A4: IR9 is_well_founded_in CR by A1,WELLFND1:def 2;
now
let Y be set such that
A5: Y c= CR and
A6: Y <> {};
consider a being object such that
A7: a in Y and
A8: IR9-Seg(a) misses Y by A4,A5,A6,WELLORD1:def 3;
A9: IR9-Seg(a) /\ Y = {} by A8,XBOOLE_0:def 7;
take a;
thus a in Y by A7;
now
assume IR-Seg(a) /\ Y <> {};
then consider z being object such that
A10: z in IR-Seg(a) /\ Y by XBOOLE_0:def 1;
A11: z in IR-Seg(a) by A10,XBOOLE_0:def 4;
A12: z in Y by A10,XBOOLE_0:def 4;
A13: z <> a by A11,WELLORD1:1;
A14: [z,a] in IR by A11,WELLORD1:1;
then not [a,z] in IR by A3,A5,A7,A12,A13;
then not [z,a] in IR~ by RELAT_1:def 7;
then [z,a] in IR \ IR~ by A14,XBOOLE_0:def 5;
then z in IR9-Seg(a) by A13,WELLORD1:1;
hence contradiction by A9,A12,XBOOLE_0:def 4;
end;
hence IR-Seg(a) misses Y by XBOOLE_0:def 7;
end;
then IR is_well_founded_in CR by WELLORD1:def 3;
hence thesis by WELLFND1:def 2;
end;
begin :: Chapter 4.3
theorem Th16: :: Def 4.30 (see WAYBEL_4:def 26)
for L being RelStr, N being set, x being Element of L\~
holds x is_minimal_wrt N, the InternalRel of (L\~) iff (x in N &
for y being Element of L st y in N & [y,x] in the InternalRel of L
holds [x,y] in the InternalRel of L)
proof
let L be RelStr, N be set, x be Element of L\~;
set IR = the InternalRel of L;
set IR9 = the InternalRel of L\~;
hereby
assume
A1: x is_minimal_wrt N, the InternalRel of (L\~);
hence x in N by WAYBEL_4:def 25;
let y be Element of L such that
A2: y in N;
assume
A3: [y,x] in IR;
now per cases;
suppose x = y;
hence [x,y] in IR by A3;
end;
suppose x <> y;
then not [y,x] in IR9 by A1,A2,WAYBEL_4:def 25;
then [y,x] in IR~ by A3,XBOOLE_0:def 5;
hence [x,y] in IR by RELAT_1:def 7;
end;
end;
hence [x,y] in the InternalRel of L;
end;
assume that
A4: x in N and
A5: for y being Element of L st y in N holds [y,x] in (the InternalRel
of L) implies [x,y] in (the InternalRel of L);
now
assume ex y being set st y in N & y <> x & [y,x] in IR9;
then consider y being set such that
A6: y in N and y <> x and
A7: [y,x] in IR9;
reconsider y9=y as Element of L by A7,ZFMISC_1:87;
A8: not [y,x] in IR~ by A7,XBOOLE_0:def 5;
[y9,x] in IR implies [x,y9] in IR by A5,A6;
hence contradiction by A7,A8,RELAT_1:def 7;
end;
hence thesis by A4,WAYBEL_4:def 25;
end;
:: Proposition 4.31 - see WELLFND1:15
:: Omitting Example 4.32, Exercise 4.33, Exercise 4.34
theorem ::L_4_35: :: Lemma 4.35
for R, S being non empty RelStr, m being Function of R,S
st R is quasi_ordered & S is antisymmetric & S\~ is well_founded &
for a,b being Element of R holds
(a <= b implies m.a <= m.b) & (m.a = m.b implies [a,b] in EqRel R)
holds R\~ is well_founded
proof
let R, S be non empty RelStr, m be Function of R, S such that
A1: R is quasi_ordered and
A2: S is antisymmetric and
A3: S\~ is well_founded and
A4: for a,b being Element of R holds (a <= b implies m.a <= m.b) &
(m.a = m.b implies [a,b] in EqRel R);
set IR = the InternalRel of R, IS = the InternalRel of S;
A5: IS is_antisymmetric_in the carrier of S by A2;
now
assume ex f being sequence of R\~ st f is descending;
then consider f being sequence of R\~ such that
A6: f is descending;
reconsider f9=f as sequence of R;
deffunc F(Element of NAT) = m.(f9.$1);
consider g9 being sequence of the carrier of S such that
A7: for k being Element of NAT holds g9.k = F(k) from FUNCT_2:sch 4;
reconsider g=g9 as sequence of S\~;
now
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A8: [f.(n+1), f.n] in the InternalRel of R\~ by A6,WELLFND1:def 6;
A9: [f.(n+1), f.n] in IR \ IR~ by A6,WELLFND1:def 6;
A10: not [f.(n+1), f.n] in IR~ by A8,XBOOLE_0:def 5;
A11: g.n1 = m.(f.n1) by A7;
A12: now
assume g.(n+1) = g.n;
then m.(f.(n+1)) = m.(f.n) by A7,A11;
then [f9.(n+1), f9.n] in EqRel R by A4;
then [f.(n+1), f.n] in (IR /\ IR~) by A1,Def4;
hence contradiction by A10,XBOOLE_0:def 4;
end;
hence g.(n+1) <> g.n;
reconsider fn1 = f.(n+1) as Element of R;
reconsider fn = f.n as Element of R;
A13: fn1 <= fn by A9;
A14: g9.(n+1) = m.fn1 by A7;
g9.n1 = m.fn by A7;
then g9.(n+1) <= g9.n by A4,A13,A14;
then
A15: [g.(n+1), g.n] in IS;
then not [g.n, g.(n+1)] in IS by A5,A12;
then not [g.(n+1), g.n] in IS~ by RELAT_1:def 7;
hence [g.(n+1), g.n] in the InternalRel of S\~ by A15,XBOOLE_0:def 5;
end;
then g is descending by WELLFND1:def 6;
hence contradiction by A3,WELLFND1:14;
end;
hence thesis by WELLFND1:14;
end;
definition :: p. 158, restricted eq classes
let R be non empty RelStr, N be Subset of R;
func min-classes N -> Subset-Family of R means
:Def8:
for x being set holds x in it iff ex y being Element of R\~
st y is_minimal_wrt N, the InternalRel of (R\~) & x = Class(EqRel R,y) /\ N;
existence
proof
set IR9 = the InternalRel of R\~;
set C = {x /\ N where x is Element of Class(EqRel R) :
ex y being Element of R\~ st x = Class(EqRel R, y) &
y is_minimal_wrt N, IR9};
now
let x be object;
assume x in C;
then ex xx being Element of Class(EqRel R) st ( x = xx /\ N)&( ex
y being Element of R\~ st xx = Class(EqRel R, y) & y is_minimal_wrt N, IR9);
hence x in bool the carrier of R;
end;
then reconsider C as Subset-Family of R by TARSKI:def 3;
take C;
let x be set;
hereby
assume x in C;
then ex xx being Element of Class(EqRel R) st ( x = xx /\ N)&( ex
y being Element of R\~ st xx = Class(EqRel R, y) & y is_minimal_wrt N, IR9);
hence ex y being Element of R\~ st y is_minimal_wrt N, IR9 &
x = Class(EqRel R,y) /\ N;
end;
given y being Element of R\~ such that
A1: y is_minimal_wrt N, IR9 and
A2: x = Class(EqRel R,y) /\ N;
reconsider y9 = y as Element of R;
EqClass(EqRel R, y9) in Class(EqRel R);
hence thesis by A1,A2;
end;
uniqueness
proof
set IR = the InternalRel of R\~;
let IT1, IT2 be Subset-Family of R such that
A3: for x being set holds x in IT1 iff
ex y being Element of R\~ st y is_minimal_wrt N, IR &
x = Class(EqRel R,y) /\ N and
A4: for x being set holds x in IT2 iff
ex y being Element of R\~ st y is_minimal_wrt N, IR &
x = Class(EqRel R, y) /\ N;
now
let x be object;
hereby
assume x in IT1;
then ex y being Element of R\~ st y is_minimal_wrt N, IR &
x = Class(EqRel R,y) /\ N by A3;
hence x in IT2 by A4;
end;
assume x in IT2;
then ex y being Element of R\~ st y is_minimal_wrt N, IR &
x = Class(EqRel R,y) /\ N by A4;
hence x in IT1 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th18: :: Lemma 4.36
for R being non empty RelStr, N being Subset of R, x being set
st R is quasi_ordered & x in min-classes N
holds for y being Element of R\~ st y in x
holds y is_minimal_wrt N, the InternalRel of R\~
proof
let R be non empty RelStr, N be Subset of R, x be set such that
A1: R is quasi_ordered and
A2: x in min-classes N;
set IR = the InternalRel of R, CR = the carrier of R;
set IR9 = the InternalRel of R\~;
let c be Element of R\~ such that
A3: c in x;
consider b being Element of R\~ such that
A4: b is_minimal_wrt N, IR9 and
A5: x = Class(EqRel R, b) /\ N by A2,Def8;
c in Class(EqRel R, b) by A3,A5,XBOOLE_0:def 4;
then [c,b] in EqRel R by EQREL_1:19;
then [c,b] in IR /\ IR~ by A1,Def4;
then
A6: [c,b] in IR by XBOOLE_0:def 4;
A7: now
assume ex d being set st d in N & d <> c & [d,c] in IR9;
then consider d being set such that
A8: d in N and d <> c and
A9: [d,c] in IR9;
A10: not [d,c] in IR~ by A9,XBOOLE_0:def 5;
R is transitive by A1;
then
A11: IR is_transitive_in CR;
then
A12: [d,b] in IR by A6,A8,A9;
now
assume [d,b] in IR~;
then [b,d] in IR by RELAT_1:def 7;
then [c,d] in IR by A6,A8,A11;
hence contradiction by A10,RELAT_1:def 7;
end;
then
A13: [d,b] in IR9 by A12,XBOOLE_0:def 5;
b <> d by A6,A10,RELAT_1:def 7;
hence contradiction by A4,A8,A13,WAYBEL_4:def 25;
end;
c in N by A3,A5,XBOOLE_0:def 4;
hence thesis by A7,WAYBEL_4:def 25;
end;
theorem Th19:
for R being non empty RelStr holds R\~ is well_founded iff
for N being Subset of R st N <> {}
ex x being object st x in min-classes N
proof
let R be non empty RelStr;
set CR = the carrier of R;
set IR9= the InternalRel of R\~, CR9 = the carrier of R\~;
hereby
assume R\~ is well_founded;
then
A1: IR9 is_well_founded_in CR9 by WELLFND1:def 2;
let N be Subset of CR such that
A2: N <> {};
reconsider N9=N as Subset of CR9;
consider y being object such that
A3: y in N9 and
A4: IR9-Seg(y) misses N9 by A1,A2,WELLORD1:def 3;
A5: IR9-Seg(y) /\ N9 = {} by A4,XBOOLE_0:def 7;
reconsider y as Element of R\~ by A3;
set x = Class(EqRel R, y) /\ N;
now
assume ex z being set st z in N & z <> y & [z,y] in IR9;
then consider z being set such that
A6: z in N and
A7: z <> y and
A8: [z,y] in IR9;
z in IR9-Seg(y) by A7,A8,WELLORD1:1;
hence contradiction by A5,A6,XBOOLE_0:def 4;
end;
then y is_minimal_wrt N, IR9 by A3,WAYBEL_4:def 25;
then x in min-classes N by Def8;
hence ex x being object st x in min-classes N;
end;
assume
A9: for N being Subset of R st N <> {}
ex x being object st x in min-classes N;
now
let N be set such that
A10: N c= CR9 and
A11: N <> {};
reconsider N9=N as Subset of R by A10;
consider x being object such that
A12: x in min-classes N9 by A9,A11;
consider a being Element of R\~ such that
A13: a is_minimal_wrt N9, IR9 and x = Class(EqRel R, a) /\ N9 by A12,Def8;
reconsider a9=a as object;
take a9;
thus a9 in N by A13,WAYBEL_4:def 25;
now
assume IR9-Seg(a9) /\ N <> {};
then consider z being object such that
A14: z in IR9-Seg(a9) /\ N by XBOOLE_0:def 1;
A15: z in IR9-Seg(a9) by A14,XBOOLE_0:def 4;
A16: z in N by A14,XBOOLE_0:def 4;
then reconsider z as Element of R\~ by A10;
A17: z <> a9 by A15,WELLORD1:1;
[z,a] in IR9 by A15,WELLORD1:1;
hence contradiction by A13,A16,A17,WAYBEL_4:def 25;
end;
hence IR9-Seg(a9) misses N by XBOOLE_0:def 7;
end;
then IR9 is_well_founded_in CR9 by WELLORD1:def 3;
hence thesis by WELLFND1:def 2;
end;
theorem Th20:
for R being non empty RelStr, N being Subset of R, y being Element of R\~
st y is_minimal_wrt N, the InternalRel of (R\~)
holds min-classes N is non empty
proof
let R be non empty RelStr, N be Subset of R, y be Element of R\~ such that
A1: y is_minimal_wrt N, the InternalRel of (R\~);
ex x being set st ( x = Class(EqRel R,y) /\ N);
hence thesis by A1,Def8;
end;
theorem Th21:
for R being non empty RelStr, N being Subset of R, x being set st
x in min-classes N holds x is non empty
proof
let R be non empty RelStr, N be Subset of R, x be set;
assume x in min-classes N;
then consider y being Element of R\~ such that
A1: y is_minimal_wrt N, the InternalRel of R\~ and
A2: x = Class(EqRel R, y) /\ N by Def8;
A3: y in N by A1,WAYBEL_4:def 25;
y in Class(EqRel R, y) by EQREL_1:20;
hence thesis by A2,A3,XBOOLE_0:def 4;
end;
theorem Th22: :: Lemma 4.37
for R being non empty RelStr st R is quasi_ordered
holds R is connected & R\~ is well_founded iff
for N being non empty Subset of R holds card min-classes N = 1
proof
let R be non empty RelStr such that
A1: R is quasi_ordered;
set IR = the InternalRel of R, CR = the carrier of R;
set IR9 = the InternalRel of R\~;
hereby
assume that
A2: R is connected and
A3: R\~ is well_founded;
let N be non empty Subset of CR;
consider x being object such that
A4: x in min-classes N by A3,Th19;
consider a being Element of R\~ such that
A5: a is_minimal_wrt N, the InternalRel of (R\~) and
A6: x = Class(EqRel R, a) /\ N by A4,Def8;
A7: a in N by A5,WAYBEL_4:def 25;
now
let y be object;
hereby
assume y in min-classes N;
then consider b being Element of R\~ such that
A8: b is_minimal_wrt N, IR9 and
A9: y = Class(EqRel R, b) /\ N by Def8;
A10: b in N by A8,WAYBEL_4:def 25;
reconsider a9=a as Element of R;
reconsider b9=b as Element of R;
A11: now per cases by A2,WAYBEL_0:def 29;
suppose
A12: a9 <= b9;
then
A13: [a, b] in IR;
now per cases;
suppose a = b;
hence [b,a] in IR by A12;
end;
suppose
A14: a <> b;
now
assume not [b,a] in IR;
then not [a,b] in IR~ by RELAT_1:def 7;
then [a,b] in IR \ IR~ by A13,XBOOLE_0:def 5;
hence contradiction by A7,A8,A14,WAYBEL_4:def 25;
end;
hence [b,a] in IR;
end;
end;
hence [a,b] in IR & [b,a] in IR by A12;
end;
suppose
A15: b9 <= a9;
then
A16: [b, a] in IR;
now per cases;
suppose a = b;
hence [a,b] in IR by A15;
end;
suppose
A17: a <> b;
now
assume not [a,b] in IR;
then not [b,a] in IR~ by RELAT_1:def 7;
then [b,a] in IR \ IR~ by A16,XBOOLE_0:def 5;
hence contradiction by A5,A10,A17,WAYBEL_4:def 25;
end;
hence [a,b] in IR;
end;
end;
hence [a,b] in IR & [b,a] in IR by A15;
end;
end;
then [b,a] in IR~ by RELAT_1:def 7;
then [b,a] in IR /\ IR~ by A11,XBOOLE_0:def 4;
then [b,a] in EqRel R by A1,Def4;
then b in Class(EqRel R, a) by EQREL_1:19;
then Class(EqRel R, b) = Class(EqRel R, a) by EQREL_1:23;
hence y in {x} by A6,A9,TARSKI:def 1;
end;
assume y in {x};
then y = Class(EqRel R, a) /\ N by A6,TARSKI:def 1;
hence y in min-classes N by A5,Def8;
end;
then min-classes N = {x} by TARSKI:2;
hence card min-classes N = 1 by CARD_1:30;
end;
assume
A18: for N being non empty Subset of R holds card min-classes N = 1;
now
let a,b be Element of R;
assume that
A19: not a <= b and
A20: not a >= b;
A21: not [a,b] in IR by A19;
then
A22: not [b,a] in IR~ by RELAT_1:def 7;
not [b,a] in IR by A20;
then
A23: not [a,b] in IR~ by RELAT_1:def 7;
set N9 = {a,b};
set MCN = {{a},{b}};
now
let x be object;
reconsider xx =x as set by TARSKI:1;
hereby
assume x in min-classes N9;
then consider y being Element of R\~ such that
A24: y is_minimal_wrt N9, IR9 and
A25: x = Class(EqRel R, y) /\ N9 by Def8;
A26: y in N9 by A24,WAYBEL_4:def 25;
per cases by A26,TARSKI:def 2;
suppose
A27: y = a;
now
let z be object;
hereby
assume
A28: z in xx;
then
A29: z in Class(EqRel R,a) by A25,A27,XBOOLE_0:def 4;
A30: z in N9 by A25,A28,XBOOLE_0:def 4;
now per cases by A30,TARSKI:def 2;
suppose z = a;
hence z in {a} by TARSKI:def 1;
end;
suppose z = b;
then [b,a] in EqRel R by A29,EQREL_1:19;
then [b,a] in IR /\ IR~ by A1,Def4;
hence z in {a} by A22,XBOOLE_0:def 4;
end;
end;
hence z in {a};
end;
assume z in {a};
then
A31: z = a by TARSKI:def 1;
then
A32: z in N9 by TARSKI:def 2;
z in Class(EqRel R, a) by A31,EQREL_1:20;
hence z in xx by A25,A27,A32,XBOOLE_0:def 4;
end;
then x = {a} by TARSKI:2;
hence x in MCN by TARSKI:def 2;
end;
suppose
A33: y = b;
now
let z be object;
hereby
assume
A34: z in xx;
then
A35: z in Class(EqRel R,b) by A25,A33,XBOOLE_0:def 4;
A36: z in N9 by A25,A34,XBOOLE_0:def 4;
now per cases by A36,TARSKI:def 2;
suppose z = b;
hence z in {b} by TARSKI:def 1;
end;
suppose z = a;
then [a,b] in EqRel R by A35,EQREL_1:19;
then [a,b] in IR /\ IR~ by A1,Def4;
hence z in {b} by A21,XBOOLE_0:def 4;
end;
end;
hence z in {b};
end;
assume z in {b};
then
A37: z = b by TARSKI:def 1;
then
A38: z in N9 by TARSKI:def 2;
z in Class(EqRel R, b) by A37,EQREL_1:20;
hence z in xx by A25,A33,A38,XBOOLE_0:def 4;
end;
then x = {b} by TARSKI:2;
hence x in MCN by TARSKI:def 2;
end;
end;
assume
A39: x in MCN;
per cases by A39,TARSKI:def 2;
suppose
A40: x = {a};
now reconsider a9=a as Element of R\~;
take a9;
A41: a9 in N9 by TARSKI:def 2;
now
assume ex y being set st y in N9 & y <> a9 & [y,a9] in IR9;
then consider y being set such that
A42: y in N9 and
A43: y <> a9 and
A44: [y,a9] in IR9;
y = b by A42,A43,TARSKI:def 2;
hence contradiction by A20,A44;
end;
hence a9 is_minimal_wrt N9, the InternalRel of (R\~)
by A41,WAYBEL_4:def 25;
now
let z be object;
hereby
assume z in xx;
then
A45: z = a by A40,TARSKI:def 1;
then z in Class(EqRel R, a) by EQREL_1:20;
hence z in Class(EqRel R, a) /\ N9 by A41,A45,XBOOLE_0:def 4;
end;
assume
A46: z in Class(EqRel R, a) /\ N9;
then
A47: z in Class(EqRel R, a) by XBOOLE_0:def 4;
A48: z in N9 by A46,XBOOLE_0:def 4;
per cases by A48,TARSKI:def 2;
suppose z = a;
hence z in xx by A40,TARSKI:def 1;
end;
suppose z = b;
then [b,a] in EqRel R by A47,EQREL_1:19;
then [b,a] in IR /\ IR~ by A1,Def4;
hence z in xx by A22,XBOOLE_0:def 4;
end;
end;
hence x = Class(EqRel R, a9) /\ N9 by TARSKI:2;
end;
hence x in min-classes N9 by Def8;
end;
suppose
A49: x = {b};
now reconsider b9=b as Element of R\~;
take b9;
A50: b9 in N9 by TARSKI:def 2;
now
assume ex y being set st y in N9 & y <> b9 & [y,b9] in IR9;
then consider y being set such that
A51: y in N9 and
A52: y <> b9 and
A53: [y,b9] in IR9;
y = a by A51,A52,TARSKI:def 2;
hence contradiction by A19,A53;
end;
hence b9 is_minimal_wrt N9, the InternalRel of (R\~)
by A50,WAYBEL_4:def 25;
now
let z be object;
hereby
assume z in xx;
then
A54: z = b by A49,TARSKI:def 1;
then z in Class(EqRel R, b) by EQREL_1:20;
hence z in Class(EqRel R, b) /\ N9 by A50,A54,XBOOLE_0:def 4;
end;
assume
A55: z in Class(EqRel R, b) /\ N9;
then
A56: z in Class(EqRel R, b) by XBOOLE_0:def 4;
A57: z in N9 by A55,XBOOLE_0:def 4;
per cases by A57,TARSKI:def 2;
suppose z = b;
hence z in xx by A49,TARSKI:def 1;
end;
suppose z = a;
then [a,b] in EqRel R by A56,EQREL_1:19;
then [a,b] in IR /\ IR~ by A1,Def4;
hence z in xx by A23,XBOOLE_0:def 4;
end;
end;
hence x = Class(EqRel R, b9) /\ N9 by TARSKI:2;
end;
hence x in min-classes N9 by Def8;
end;
end;
then min-classes N9 = MCN by TARSKI:2;
then
A58: card MCN = 1 by A18;
now
assume {a} = {b};
then
A59: a = b by ZFMISC_1:3;
R is reflexive by A1;
then IR is_reflexive_in CR;
hence contradiction by A21,A59;
end;
hence contradiction by A58,CARD_2:57;
end;
hence R is connected by WAYBEL_0:def 29;
now
let N be Subset of R;
assume N <> {};
then card min-classes N = 1 by A18;
then min-classes N <> {};
hence ex x being object st x in min-classes N by XBOOLE_0:def 1;
end;
hence thesis by Th19;
end;
theorem :: Lemma 4.38
for R being non empty Poset
holds the InternalRel of R well_orders the carrier of R iff
for N being non empty Subset of R holds card min-classes N = 1
proof
let R be non empty Poset;
set IR = the InternalRel of R, CR = the carrier of R;
A1: R is quasi_ordered;
hereby
assume
A2: IR well_orders CR;
then
A3: IR is_reflexive_in CR by WELLORD1:def 5;
A4: IR is_connected_in CR by A2,WELLORD1:def 5;
A5: IR is_well_founded_in CR by A2,WELLORD1:def 5;
IR is_strongly_connected_in CR by A3,A4,ORDERS_1:7;
then
A6: R is connected by Th4;
R is well_founded by A5,WELLFND1:def 2;
then R\~ is well_founded by Th14;
hence for N being non empty Subset of R holds
card min-classes N = 1 by A1,A6,Th22;
end;
assume
A7: for N being non empty Subset of R holds card min-classes N = 1;
then
A8: R is connected by A1,Th22;
A9: R\~ is well_founded by A1,A7,Th22;
A10: IR is_strongly_connected_in CR by A8,Th4;
A11: R is well_founded by A9,Th15;
A12: IR is_reflexive_in CR by ORDERS_2:def 2;
A13: IR is_transitive_in CR by ORDERS_2:def 3;
A14: IR is_antisymmetric_in CR by ORDERS_2:def 4;
A15: IR is_connected_in CR by A10;
IR is_well_founded_in CR by A11,WELLFND1:def 2;
hence thesis by A12,A13,A14,A15,WELLORD1:def 5;
end;
definition :: Def 4.39
let R be RelStr, N be Subset of R, B be set;
pred B is_Dickson-basis_of N,R means
B c= N & for a being Element of R st a in N
ex b being Element of R st b in B & b <= a;
end;
theorem
for R being RelStr holds {} is_Dickson-basis_of {} the carrier of R, R;
theorem Th25:
for R being non empty RelStr, N being non empty Subset of R, B being set
st B is_Dickson-basis_of N,R holds B is non empty
proof
let R be non empty RelStr, N be non empty Subset of R, B be set;
assume
A1: B is_Dickson-basis_of N,R;
set a = the Element of N;
ex b being Element of R st ( b in B)&( b <= a) by A1;
hence thesis;
end;
definition :: Def 4.39
let R be RelStr;
attr R is Dickson means
for N being Subset of R
ex B being set st B is_Dickson-basis_of N,R & B is finite;
end;
theorem Th26: :: Lemma 4:40
for R being non empty RelStr
st R\~ is well_founded & R is connected holds R is Dickson
proof
let R be non empty RelStr such that
A1: R\~ is well_founded and
A2: R is connected;
set IR9 = the InternalRel of R\~, CR9 = the carrier of R\~;
set IR = the InternalRel of R, CR = the carrier of R;
let N be Subset of CR;
per cases;
suppose
A3: N = {} CR;
take B = {};
thus B is_Dickson-basis_of N,R by A3;
thus thesis;
end;
suppose
A4: N <> {} CR;
IR9 is_well_founded_in CR9 by A1,WELLFND1:def 2;
then consider b being object such that
A5: b in N and
A6: IR9-Seg(b) misses N by A4,WELLORD1:def 3;
A7: IR9-Seg(b) /\ N = {} by A6,XBOOLE_0:def 7;
take B = {b};
reconsider b as Element of N by A5;
thus B is_Dickson-basis_of N,R
proof
{b} is Subset of N by A4,SUBSET_1:33;
hence B c= N;
let a be Element of R such that
A8: a in N;
reconsider b as Element of R by A5;
take b;
thus b in B by TARSKI:def 1;
per cases by A2,WAYBEL_0:def 29;
suppose b <= a;
hence thesis;
end;
suppose
A9: a <= b;
then
A10: [a,b] in IR;
now per cases;
suppose a = b;
hence thesis by A9;
end;
suppose
A11: not a = b;
now per cases;
suppose [a,b] in IR9;
then a in IR9-Seg(b) by A11,WELLORD1:1;
hence thesis by A7,A8,XBOOLE_0:def 4;
end;
suppose not [a,b] in IR9;
then [a,b] in IR~ by A10,XBOOLE_0:def 5;
then [b,a] in IR by RELAT_1:def 7;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
thus thesis;
end;
end;
theorem Th27: :: Exercise 4.41
for R, S being RelStr st (the InternalRel of R) c= (the InternalRel of S) &
R is Dickson & (the carrier of R) = (the carrier of S) holds S is Dickson
proof
let r, s be RelStr such that
A1: the InternalRel of r c= the InternalRel of s and
A2: r is Dickson and
A3: the carrier of r = the carrier of s;
let N be Subset of s;
reconsider N9 = N as Subset of r by A3;
consider B being set such that
A4: B is_Dickson-basis_of N9,r and
A5: B is finite by A2;
take B;
thus B c= N by A4;
hereby
let a be Element of s such that
A6: a in N;
reconsider a9 = a as Element of r by A3;
consider b being Element of r such that
A7: b in B and
A8: b <= a9 by A4,A6;
reconsider b9 = b as Element of s by A3;
take b9;
[b,a9] in the InternalRel of r by A8;
hence b9 in B & b9 <= a by A1,A7;
end;
thus thesis by A5;
end;
definition
let f be Function, b be set such that
A1: dom f = NAT and
A2: b in rng f;
func f mindex b -> Element of NAT means
:Def11:
f.it = b & for i being Element of NAT st f.i = b holds it <= i;
existence
proof
set N = {i where i is Element of NAT : f.i = b};
consider x being object such that
A3: x in NAT and
A4: f.x = b by A1,A2,FUNCT_1:def 3;
reconsider x as Element of NAT by A3;
A5: x in N by A4;
now
let x be object;
assume x in N;
then ex i being Element of NAT st ( x = i)&( f.i = b);
hence x in NAT;
end;
then reconsider N as non empty Subset of NAT by A5,TARSKI:def 3;
take I = min N;
I in N by XXREAL_2:def 7;
then ex II being Element of NAT st ( II = I)&( f.II = b);
hence f.I = b;
let i be Element of NAT;
assume f.i = b;
then i in N;
hence thesis by XXREAL_2:def 7;
end;
uniqueness
proof
let IT1, IT2 be Element of NAT such that
A6: f.IT1 = b and
A7: for i being Element of NAT st f.i = b holds IT1 <= i and
A8: f.IT2 = b and
A9: for i being Element of NAT st f.i = b holds IT2 <= i;
assume
A10: IT1 <> IT2;
per cases by A10,XXREAL_0:1;
suppose IT1 < IT2;
hence contradiction by A6,A9;
end;
suppose IT1 > IT2;
hence contradiction by A7,A8;
end;
end;
end;
definition
let R be non empty 1-sorted, f be sequence of R, b be set,
m be Element of NAT;
assume
A1: ex j being Element of NAT st m < j & f.j = b;
func f mindex (b,m) -> Element of NAT means
: Def12:
f.it = b & m < it & for i being Element of NAT st m < i & f.i = b
holds it <= i;
existence
proof
set N = {i where i is Element of NAT : m < i & f.i = b};
consider j being Element of NAT such that
A2: m < j and
A3: f.j = b by A1;
A4: j in N by A2,A3;
now
let x be object;
assume x in N;
then ex i being Element of NAT st ( x = i)&( m < i)&( f.i = b);
hence x in NAT;
end;
then reconsider N as non empty Subset of NAT by A4,TARSKI:def 3;
take I = min N;
I in N by XXREAL_2:def 7;
then ex II being Element of NAT st ( II = I)&( m < II)&( f.II = b);
hence f.I = b & m < I;
let i be Element of NAT such that
A5: m < i and
A6: f.i = b;
i in N by A5,A6;
hence thesis by XXREAL_2:def 7;
end;
uniqueness
proof
let IT1, IT2 be Element of NAT such that
A7: f.IT1 = b and
A8: m < IT1 and
A9: for i being Element of NAT st m < i & f.i = b holds IT1 <= i and
A10: f.IT2 = b and
A11: m < IT2 and
A12: for i being Element of NAT st m < i & f.i = b holds IT2 <= i;
assume
A13: IT1 <> IT2;
per cases by A13,XXREAL_0:1;
suppose IT1 < IT2;
hence contradiction by A7,A8,A12;
end;
suppose IT1 > IT2;
hence contradiction by A9,A10,A11;
end;
end;
end;
theorem Th28: :: Prop 4.42 (i) -> (ii)
for R being non empty RelStr st R is Dickson
for f being sequence of R ex i,j being Nat st i < j & f.i <= f.j
proof
let R be non empty RelStr such that
A1: R is Dickson;
let f be sequence of R;
set N = rng f;
A2: dom f = NAT by FUNCT_2:def 1;
consider B being set such that
A3: B is_Dickson-basis_of N,R and
A4: B is finite by A1;
reconsider B as finite non empty set by A3,A4,Th25;
defpred P[set] means not contradiction;
deffunc F(set) = f mindex $1;
set BI = { F(b) where b is Element of B : P[b] };
A5: BI is finite from PRE_CIRC:sch 1;
set b = the Element of B;
A6: f mindex b in BI;
now
let x be object;
assume x in BI;
then ex b being Element of B st ( x = f mindex b);
hence x in NAT;
end;
then reconsider BI as finite non empty Subset of NAT by A5,A6,TARSKI:def 3;
reconsider mB = max BI as Element of NAT by ORDINAL1:def 12;
set j = mB+1;
reconsider fj = f.j as Element of R;
fj in N by A2,FUNCT_1:3;
then consider b being Element of R such that
A7: b in B and
A8: b <= fj by A3;
A9: B c= N by A3;
take i = f mindex b;
take j;
i in BI by A7;
then i <= max(BI) by XXREAL_2:def 8;
hence i < j by NAT_1:13;
dom f = NAT by NORMSP_1:12;
hence thesis by A7,A8,A9,Def11;
end;
theorem Th29:
for R being RelStr, N being Subset of R, x being Element of R\~
st R is quasi_ordered & x in N &
((the InternalRel of R)-Seg(x)) /\ N c= Class(EqRel R,x)
holds x is_minimal_wrt N, the InternalRel of R\~
proof
let R be RelStr, N be Subset of R, x be Element of R\~ such that
A1: R is quasi_ordered and
A2: x in N and
A3: ((the InternalRel of R)-Seg(x)) /\ N c= Class(EqRel R,x);
set IR = the InternalRel of R;
set IR9= the InternalRel of R\~;
now
assume ex y being set st y in N & y<>x & [y,x] in IR9;
then consider y being set such that
A4: y in N and
A5: y <> x and
A6: [y,x] in IR9;
A7: not [y,x] in IR~ by A6,XBOOLE_0:def 5;
y in IR-Seg(x) by A5,A6,WELLORD1:1;
then y in IR-Seg(x) /\ N by A4,XBOOLE_0:def 4;
then [y,x] in EqRel R by A3,EQREL_1:19;
then [y,x] in IR /\ IR~ by A1,Def4;
hence contradiction by A7,XBOOLE_0:def 4;
end;
hence thesis by A2,WAYBEL_4:def 25;
end;
theorem Th30: :: Prop 4.42 (ii) -> (iii)
for R being non empty RelStr st R is quasi_ordered &
(for f being sequence of R ex i,j being Nat st i < j & f.i <= f.j)
holds for N being non empty Subset of R
holds min-classes N is finite & min-classes N is non empty
proof
let R be non empty RelStr such that
A1: R is quasi_ordered and
A2: for f being sequence of R
ex i,j being Nat st i < j & f.i <= f.j;
set IR = the InternalRel of R;
set IR9= the InternalRel of R\~;
A3: R is transitive by A1;
let N be non empty Subset of R such that
A4: not (min-classes N is finite & min-classes N is non empty);
per cases by A4;
suppose
A5: min-classes N is infinite;
then reconsider MCN = min-classes N as infinite set;
consider f being sequence of min-classes N such that
A6: f is one-to-one by A5,Th2;
deffunc F(object) = the Element of f.$1;
A7: now
let x be object;
assume x in NAT;
then reconsider x9 = x as Element of NAT;
f.x9 is Element of min-classes N;
then
A8: f.x in MCN;
then f.x is non empty by Th21;
then the Element of f.x9 in f.x;
hence F(x) in the carrier of R by A8;
end;
:: !!! wykorzystac PBOOLE:sch 1 ??
consider g being sequence of the carrier of R such that
A9: for x being object st x in NAT holds g.x = F(x) from FUNCT_2:sch 2(A7);
reconsider g as sequence of R;
consider i,j being Nat such that
A10: i < j and
A11: g.i <= g.j by A2;
reconsider gi = g.i, gj= g.j as Element of R\~;
A12: [gi, gj] in IR by A11;
A13: f.i in MCN;
then
A14: f.i is non empty by Th21;
A15: f.j in MCN;
then
A16: f.j is non empty by Th21;
j in NAT by ORDINAL1:def 12;
then
A17: g.j = the Element of f.j by A9;
i in NAT by ORDINAL1:def 12;
then
A18: g.i = the Element of f.i by A9;
A19: gj is_minimal_wrt N, the InternalRel of R\~ by A1,A15,A16,A17,Th18;
gi is_minimal_wrt N, the InternalRel of R\~ by A1,A13,A14,A18,Th18;
then
A20: gi in N by WAYBEL_4:def 25;
A21: now per cases;
suppose gi = gj;
hence [gi, gj] in IR~ by A12,RELAT_1:def 7;
end;
suppose
A22: gi <> gj;
now
assume not [gi, gj] in IR~;
then [gi, gj] in IR \ IR~ by A12,XBOOLE_0:def 5;
hence contradiction by A19,A20,A22,WAYBEL_4:def 25;
end;
hence [gi, gj] in IR~;
end;
end;
[gi,gj] in IR by A11;
then [gi,gj] in IR /\ IR~ by A21,XBOOLE_0:def 4;
then [gi,gj] in EqRel R by A1,Def4;
then gi in Class(EqRel R, gj) by EQREL_1:19;
then
A23: Class(EqRel R, gj) = Class(EqRel R, gi) by EQREL_1:23;
consider mj being Element of R\~ such that
mj is_minimal_wrt N, IR9 and
A24: f.j = Class(EqRel R,mj) /\ N by A15,Def8;
consider mi being Element of R\~ such that
mi is_minimal_wrt N, IR9 and
A25: f.i = Class(EqRel R,mi) /\ N by A13,Def8;
gj in Class(EqRel R, mj) by A16,A17,A24,XBOOLE_0:def 4;
then
A26: Class(EqRel R, gj) = Class(EqRel R, mj) by EQREL_1:23;
A27: i in NAT by ORDINAL1:def 12;
A28: j in NAT by ORDINAL1:def 12;
gi in Class(EqRel R, mi) by A14,A18,A25,XBOOLE_0:def 4;
then f.i = f.j by A23,A24,A25,A26,EQREL_1:23;
hence contradiction by A5,A6,A10,FUNCT_2:19,A27,A28;
end;
suppose
A29: min-classes N is empty;
deffunc F(set,set) = the Element of IR-Seg($2) /\ N\Class(EqRel R,$2);
consider f being Function such that
A30: dom f = NAT and
A31: f.0 = the Element of N and
A32: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 11;
defpred P[Nat] means f.$1 in N;
A33: P[ 0 ] by A31;
A34: now
let i be Nat such that
A35: P[i];
reconsider fi = f.i as Element of R\~ by A35;
set IC = IR-Seg(fi) /\ N\Class(EqRel R,fi);
A36: f.(i+1) = the Element of IR-Seg(f.i) /\ N\Class(EqRel R,f.i) by A32;
now
assume IC is empty;
then IR-Seg(fi) /\ N c= Class(EqRel R,fi) by XBOOLE_1:37;
hence contradiction by A1,A29,A35,Th20,Th29;
end;
then f.(i+1) in IR-Seg(f.i) /\ N by A36,XBOOLE_0:def 5;
hence P[i+1] by XBOOLE_0:def 4;
end;
A37: for i being Nat holds P[i] from NAT_1:sch 2(A33,A34);
now
let x being object;
assume x in NAT;
then f.x in N by A37;
hence f.x in the carrier of R;
end;
then reconsider f as sequence of R by A30,FUNCT_2:3;
A38: now
let i be Nat;
defpred P[Nat] means i < $1 implies f.i >= f.$1;
A39: P[ 0 ] by NAT_1:2;
A40: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat such that
A41: i < j implies f.i >= f.j and
A42: i < j+1;
A43: i <= j by A42,NAT_1:13;
reconsider fj = f.j, fj1 = f.(j+1) as Element of R\~;
set IC = IR-Seg(fj) /\ N\Class(EqRel R,fj);
A44: fj in N by A37;
A45: fj1 = the Element of IC by A32;
now
assume IC is empty;
then IR-Seg(fj) /\ N c= Class(EqRel R,fj) by XBOOLE_1:37;
hence contradiction by A1,A29,A44,Th20,Th29;
end;
then fj1 in IR-Seg(fj) /\ N by A45,XBOOLE_0:def 5;
then fj1 in IR-Seg(fj) by XBOOLE_0:def 4;
then
A46: [fj1, fj] in IR by WELLORD1:1;
then
A47: f.j >= f.(j+1);
per cases by A43,XXREAL_0:1;
suppose i < j;
hence thesis by A3,A41,A47,ORDERS_2:3;
end;
suppose i = j;
hence thesis by A46;
end;
end;
thus for j being Nat holds P[j] from NAT_1:sch 2(A39,A40);
end;
now
let i be Nat;
defpred P[Nat] means i < $1 implies not f.i <= f.$1;
A48: P[ 0 ] by NAT_1:2;
A49: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat such that
i < j implies not f.i <= f.j and
A50: i < j+1;
A51: i <= j by A50,NAT_1:13;
reconsider fj = f.j, fj1 = f.(j+1) as Element of R\~;
A52: fj in N by A37;
per cases by A51,XXREAL_0:1;
suppose
A53: i < j;
assume
A54: f.i <= f.(j+1);
j < j+1 by NAT_1:13;
then
A55: f.j >= f.(j+1) by A38;
f.i >= f.j by A38,A53;
then f.j <= f.(j+1) by A3,A54,ORDERS_2:3;
then
A56: fj1 in Class(EqRel R, fj) by A1,A55,Th7;
set IC = IR-Seg(fj) /\ N\Class(EqRel R,fj);
A57: fj1 = the Element of IC by A32;
now
assume IC is empty;
then IR-Seg(fj) /\ N c= Class(EqRel R,fj) by XBOOLE_1:37;
hence contradiction by A1,A29,A52,Th20,Th29;
end;
hence contradiction by A56,A57,XBOOLE_0:def 5;
end;
suppose
A58: i = j;
assume
A59: f.i <= f.(j+1);
j < j+1 by NAT_1:13;
then f.(j+1) <= f.j by A38;
then
A60: fj1 in Class(EqRel R, fj) by A1,A58,A59,Th7;
set IC = IR-Seg(fj) /\ N\Class(EqRel R,fj);
A61: fj1 = the Element of IC by A32;
now
assume IC is empty;
then IR-Seg(fj) /\ N c= Class(EqRel R,fj) by XBOOLE_1:37;
hence contradiction by A1,A29,A52,Th20,Th29;
end;
hence contradiction by A60,A61,XBOOLE_0:def 5;
end;
end;
thus for j being Nat holds P[j] from NAT_1:sch 2(A48,A49);
end;
hence contradiction by A2;
end;
end;
theorem Th31: :: Prop (iii) -> (i)
for R being non empty RelStr st R is quasi_ordered &
(for N being non empty Subset of R
holds min-classes N is finite & min-classes N is non empty)
holds R is Dickson
proof
let R be non empty RelStr such that
A1: R is quasi_ordered and
A2: for N being non empty Subset of R
holds min-classes N is finite & min-classes N is non empty;
A3: R is transitive by A1;
A4: R is reflexive by A1;
set IR = the InternalRel of R, CR = the carrier of R;
set IR9 = the InternalRel of R\~;
let N be Subset of CR;
per cases;
suppose
A5: N = {} CR;
take B = {};
thus B is_Dickson-basis_of N,R by A5;
thus thesis;
end;
suppose not N is empty;
then reconsider N9=N as non empty Subset of CR;
reconsider MCN9 = min-classes N9 as finite non empty Subset-Family of CR
by A2;
take B = the set of all the Element of x where x is Element of MCN9 ;
thus B is_Dickson-basis_of N,R
proof
now
let x be object;
assume x in B;
then consider y being Element of MCN9 such that
A6: x = the Element of y;
A7: ex z being Element of R\~ st ( z is_minimal_wrt N, IR9)&( y
= Class(EqRel R, z) /\ N) by Def8;
y is non empty by Th21;
hence x in N by A6,A7,XBOOLE_0:def 4;
end;
hence B c= N;
let a be Element of R such that
A8: a in N;
defpred P[Element of R] means $1 <= a;
set NN9 = {d where d is Element of N9 : P[d]};
A9: NN9 is Subset of N9 from DOMAIN_1:sch 7;
a <= a by A4,ORDERS_2:1;
then a in NN9 by A8;
then reconsider NN9 as non empty Subset of CR by A9,XBOOLE_1:1;
set m = the Element of min-classes NN9;
A10: min-classes NN9 is non empty by A2;
then reconsider m9 = m as non empty set by Th21;
set c = the Element of m9;
consider y being Element of R\~ such that
y is_minimal_wrt NN9, IR9 and
A11: m9 = Class(EqRel R, y) /\ NN9 by A10,Def8;
A12: c in Class(EqRel R, y) by A11,XBOOLE_0:def 4;
A13: c in NN9 by A11,XBOOLE_0:def 4;
reconsider c as Element of R\~ by A12;
reconsider c9=c as Element of R;
A14: ex d being Element of N9 st ( c = d)&( d <= a) by A13;
A15: c is_minimal_wrt NN9, IR9 by A1,A10,Th18;
now
assume not c is_minimal_wrt N, IR9;
then consider w being set such that
A16: w in N and
A17: w <> c and
A18: [w,c] in IR9 by A14,WAYBEL_4:def 25;
reconsider w9 = w as Element of R by A18,ZFMISC_1:87;
w9 <= c9 by A18;
then w9 <= a by A3,A14,ORDERS_2:3;
then w9 in NN9 by A16;
hence contradiction by A15,A17,A18,WAYBEL_4:def 25;
end;
then
A19: Class(EqRel R, c) /\ N in min-classes N by Def8;
then
A20: Class(EqRel R, c) /\ N is non empty by Th21;
set t = the Element of Class(EqRel R, c) /\ N;
t in N by A20,XBOOLE_0:def 4;
then reconsider t as Element of R;
take t;
thus t in B by A19;
t in Class(EqRel R, c) by A20,XBOOLE_0:def 4;
then [t,c] in EqRel R by EQREL_1:19;
then [t,c] in IR /\ IR~ by A1,Def4;
then [t,c] in IR by XBOOLE_0:def 4;
then t <= c9;
hence thesis by A3,A14,ORDERS_2:3;
end;
:: !!! Choice
deffunc F(set) = the Element of $1;
defpred P[set] means not contradiction;
{F(x) where x is Element of MCN9 : P[x]} is finite from PRE_CIRC: sch 1;
hence thesis;
end;
end;
theorem Th32: :: Corollary 4.44
for R being non empty RelStr st R is quasi_ordered & R is Dickson
holds R\~ is well_founded
proof
let R be non empty RelStr such that
A1: R is quasi_ordered and
A2: R is Dickson;
A3: for
f being sequence of R ex i,j being Nat st i < j & f.i <= f.j
by A2,Th28;
now
let N be Subset of R;
assume N <> {};
then min-classes N is non empty by A1,A3,Th30;
hence ex x being object st x in min-classes N by XBOOLE_0:def 1;
end;
hence thesis by Th19;
end;
theorem :: Corollary 4.43
for R being non empty Poset, N being non empty Subset of R st R is Dickson
holds ex B being set st B is_Dickson-basis_of N, R &
for C being set st C is_Dickson-basis_of N, R holds B c= C
proof
let R be non empty Poset, N be non empty Subset of R such that
A1: R is Dickson;
set IR=the InternalRel of R, CR = the carrier of R;
set IR9=the InternalRel of R\~;
set B = {b where b is Element of R\~ : b is_minimal_wrt N, IR9};
A2: R is quasi_ordered;
for f being sequence of R ex i,j being Nat
st i < j & f.i <= f.j by A1,Th28;
then min-classes N is non empty by A2,Th30;
then consider x being object such that
A3: x in min-classes N by XBOOLE_0:def 1;
consider y being Element of R\~ such that
A4: y is_minimal_wrt N, IR9 and x = Class(EqRel R, y) /\ N by A3,Def8;
y in B by A4;
then reconsider B as non empty set;
take B;
A5: now
let x be object;
assume x in B;
then ex b being Element of R\~ st ( x = b)&( b is_minimal_wrt N, IR9);
hence x in N by WAYBEL_4:def 25;
end;
then
A6: B c= N;
thus B is_Dickson-basis_of N, R
proof
thus B c= N by A5;
let a be Element of R such that
A7: a in N;
reconsider a9=a as Element of R\~;
now
assume
A8: not ex b being Element of R st b in B & b <= a;
per cases;
suppose IR9-Seg(a) /\ N = {};
then IR9-Seg(a) misses N by XBOOLE_0:def 7;
then a9 is_minimal_wrt N, IR9 by A7,Th5;
then a in B;
hence contradiction by A8;
end;
suppose
A9: IR9-Seg(a) /\ N <> {};
R\~ is well_founded by A1,A2,Th32;
then IR9 is_well_founded_in CR by WELLFND1:def 2;
then consider z being object such that
A10: z in IR9-Seg(a) /\ N and
A11: IR9-Seg(z) misses (IR9-Seg(a) /\ N) by A9,WELLORD1:def 3;
A12: z in IR9-Seg(a) by A10,XBOOLE_0:def 4;
then [z,a] in IR9 by WELLORD1:1;
then z in dom IR9 by XTUPLE_0:def 12;
then reconsider z as Element of R\~;
reconsider z9 = z as Element of R;
z is_minimal_wrt IR9-Seg(a9) /\ N, IR9 by A10,A11,Th5;
then z is_minimal_wrt N, IR9 by Th6;
then
A13: z in B;
[z,a] in IR \ IR~ by A12,WELLORD1:1;
then z9 <= a;
hence contradiction by A8,A13;
end;
end;
hence ex b being Element of R st b in B & b <= a;
end;
let C be set such that
A14: C is_Dickson-basis_of N, R;
A15: C c= N by A14;
now
let b be object such that
A16: b in B;
b in N by A5,A16;
then reconsider b9=b as Element of R;
consider c being Element of R such that
A17: c in C and
A18: c <= b9 by A6,A14,A16;
A19: ex b99 being Element of R\~ st ( b99 = b)&( b99
is_minimal_wrt N, IR9) by A16;
A20: [c,b] in IR by A18;
A21: IR is_antisymmetric_in CR by ORDERS_2:def 4;
[b,c] in IR by A15,A17,A19,A20,Th16;
hence b in C by A17,A18,A21;
end;
hence thesis;
end;
definition
let R be non empty RelStr, N be Subset of R such that
A1: R is Dickson;
func Dickson-bases (N,R) -> non empty Subset-Family of R means
:Def13:
for B being set holds B in it iff B is_Dickson-basis_of N,R;
existence
proof
set BB = {b where b is Subset of N: b is_Dickson-basis_of N,R};
set CR = the carrier of R;
consider bp being set such that
A2: bp is_Dickson-basis_of N,R and bp is finite by A1;
A3: bp in BB by A2;
now
let x be object;
assume x in BB;
then consider b being Subset of N such that
A4: x = b and b is_Dickson-basis_of N,R;
b c= CR by XBOOLE_1:1;
hence x in bool CR by A4;
end;
then reconsider BB as non empty Subset-Family of CR by A3,TARSKI:def 3;
take BB;
let B be set;
hereby
assume B in BB;
then ex b being Subset of N st ( b = B)&( b is_Dickson-basis_of N,R);
hence B is_Dickson-basis_of N,R;
end;
assume
A5: B is_Dickson-basis_of N,R;
thus thesis by A5;
end;
uniqueness
proof
let IT1, IT2 be non empty Subset-Family of R such that
A6: for B being set holds B in IT1 iff B is_Dickson-basis_of N, R and
A7: for B being set holds B in IT2 iff B is_Dickson-basis_of N, R;
for x being object holds x in IT1 iff x in IT2 by A6,A7;
hence thesis by TARSKI:2;
end;
end;
theorem Th34: :: Proposition 4.45
for R being non empty RelStr, s being sequence of R st R is Dickson
ex t being sequence of R st t is subsequence of s & t is weakly-ascending
proof
let R be non empty RelStr, s be sequence of R such that
A1: R is Dickson;
set CR = the carrier of R;
deffunc Bi(Element of rng s, Element of NAT)
= {n where n is Element of NAT : $1 <= s.n & $2 < n};
deffunc Bi2(Element of rng s) = {n where n is Element of NAT : $1 <= s.n};
defpred P[set,Element of NAT,set] means
ex N being Subset of CR, B being non empty Subset of CR
st N = {s.w where w is Element of NAT : s.$2 <= s.w & $2 < w} &
{ w where w is Element of NAT : s.$2 <= s.w & $2 < w} is infinite &
B = the Element of {BB where BB is Element of Dickson-bases(N,R):
BB is finite} &
$3 = s mindex ( the Element of {b where b is Element of B :
ex b9 being Element of rng s st b9=b & Bi(b9,$2) is infinite}, $2);
defpred Q[set,Element of NAT,set] means
{w where w is Element of NAT : s.$2 <= s.w & $2 < w} is infinite
implies P[$1,$2,$3];
A2: for n being Nat for x being Element of NAT
ex y being Element of NAT st Q[n,x,y]
proof
let n be Nat, x be Element of NAT;
set N = {s.w where w is Element of NAT : s.x <= s.w & x < w};
now
let y be object;
assume y in N;
then ex w being Element of NAT st ( y = s.w)&( s.x <= s.w)&( x < w);
hence y in CR;
end;
then reconsider N as Subset of CR by TARSKI:def 3;
set W = {w where w is Element of NAT : s.x <= s.w & x < w};
per cases;
suppose
A3: N is empty;
take 1;
assume W is infinite;
then consider ww being object such that
A4: ww in W by XBOOLE_0:def 1;
consider www being Element of NAT such that www = ww and
A5: s.x <= s.www and
A6: x < www by A4;
s.www in N by A5,A6;
hence thesis by A3;
end;
suppose
A7: N is non empty;
set BBX = {BB where BB is Element of Dickson-bases(N,R): BB is finite};
set B = the Element of BBX;
consider BD1 being set such that
A8: BD1 is_Dickson-basis_of N,R and
A9: BD1 is finite by A1;
BD1 in Dickson-bases(N,R) by A1,A8,Def13;
then BD1 in BBX by A9;
then B in BBX;
then ex BBB being Element of Dickson-bases(N,R) st ( B = BBB)&(
BBB is finite);
then
A10: B is_Dickson-basis_of N,R by A1,Def13;
reconsider B as non empty Subset of CR by A7,A10,Th25,XBOOLE_1:1;
set y = s mindex ( the Element of {b where b is Element of B :
ex b9 being Element of rng s st b9=b & Bi(b9,x) is infinite}, x);
take y;
set W = {w where w is Element of NAT : s.x <= s.w & x < w};
assume
A11: W is infinite;
take N;
reconsider B as non empty Subset of CR;
take B;
thus N = {s.w where w is Element of NAT : s.x <= s.w & x < w};
thus { w where w is Element of NAT : s.x <= s.w & x < w}
is infinite by A11;
thus B = the Element of {BB where BB is Element of Dickson-bases(N,R):
BB is finite};
thus thesis;
end;
end;
consider B being set such that
A12: B is_Dickson-basis_of rng s, R and
A13: B is finite by A1;
reconsider B as non empty set by A12,Th25;
set BALL = {b where b is Element of B :
ex b9 being Element of rng s st b9=b & Bi2(b9) is infinite};
set b1 = the Element of BALL;
consider f being sequence of NAT such that
A14: f.0 = s mindex b1 and
A15: for n being Nat holds Q[n, f.n, f.(n+1)]
from RECDEF_1:sch 2(A2);
A16: dom f = NAT by FUNCT_2:def 1;
A17: rng f c= NAT;
now
A18: B is finite by A13;
assume
A19: for b being Element of rng s st b in B holds Bi2(b) is finite;
set Ball = {Bi2(b) where b is Element of rng s: b in B};
A20: Ball is finite from FRAENKEL:sch 21(A18);
now
let X be set;
assume X in Ball;
then ex b being Element of rng s st ( X = Bi2(b))&( b in B);
hence X is finite by A19;
end;
then
A21: union Ball is finite by A20,FINSET_1:7;
now
let x be object;
assume x in NAT;
then reconsider x9= x as Element of NAT;
dom s = NAT by FUNCT_2:def 1;
then x9 in dom s;
then
A22: s.x in rng s by FUNCT_1:3;
then reconsider sx = s.x as Element of R;
consider b being Element of R such that
A23: b in B and
A24: b <= sx by A12,A22;
B c= rng s by A12;
then reconsider b as Element of rng s by A23;
A25: x9 in Bi2(b) by A24;
Bi2(b) in Ball by A23;
hence x in union Ball by A25,TARSKI:def 4;
end;
then NAT c= union Ball;
hence contradiction by A21;
end;
then consider tb being Element of rng s such that
A26: tb in B and
A27: Bi2(tb) is infinite;
A28: tb in BALL by A26,A27;
then b1 in BALL;
then
A29: ex bt being Element of B st ( b1 = bt)&( ex b9 being
Element of rng s st b9 = bt & Bi2(b9) is infinite);
dom s = NAT by NORMSP_1:12;
then
A30: s.(f.0) = b1 by A14,A29,Def11;
b1 in BALL by A28;
then
A31: ex eb being Element of B st ( b1 = eb)&( ex eb9 being
Element of rng s st eb9=eb & Bi2(eb9) is infinite);
deffunc F(set) = $1;
defpred P[Nat] means 0 <= $1 & s.(f.0) <= s.$1;
set W1 = {w where w is Element of NAT: s.(f.0) <= s.w};
set W2 = {w where w is Element of NAT: s.(f.0) <= s.w & f.0 < w};
set W3 = {F(w) where w is Nat: w <= f.0 & P[w]};
A32: W3 is finite from FINSEQ_1:sch 6;
now
let x be object;
hereby
assume x in W1;
then consider w being Element of NAT such that
A33: x = w and
A34: s.(f.0) <= s.w;
A35: 0 <= w by NAT_1:2;
w <= f.0 or w > f.0;
then x in W2 or x in W3 by A33,A34,A35;
hence x in W2 \/ W3 by XBOOLE_0:def 3;
end;
assume
A36: x in W2 \/ W3;
per cases by A36,XBOOLE_0:def 3;
suppose x in W2;
then ex w being Element of NAT st ( x = w)&( s.(f.0) <= s.w)&( f .0 < w);
hence x in W1;
end;
suppose x in W3;
then
A37: ex w being Nat st x = w & w <= f.0 & 0 <= w & s.(f.0) <= s.w;
then reconsider w=x as Element of NAT by ORDINAL1:def 12;
0 <= w & w <= f.0 & s.(f.0) <= s.w by A37;
hence x in W1;
end;
end;
then
A38: W2 is infinite by A30,A31,A32,TARSKI:2;
defpred R[Nat] means P[$1, f.$1, f.($1+1)];
A39: R[ 0 ] by A15,A38;
A40: now
let k be Nat;
assume R[k];
then consider
N being Subset of CR, B being non empty Subset of CR such that
A41: N = {s.w where w is Element of NAT : s.(f.k) <= s.w & f.k < w} and
A42: {w where w is Element of NAT : s.(f.k) <= s.w & f.k < w} is infinite and
A43: B = the Element of {BB where BB is Element of Dickson-bases(N, R) :
BB is finite} and
A44: f.(k+1)=s mindex (the Element of {b where b is Element of B :
ex b9 being Element of rng s
st b9=b & Bi(b9,f.k) is infinite},f.k);
set BALL={b where b is Element of B: ex b9 being Element of rng s
st b9=b & Bi(b9,f.k) is infinite};
set BBX ={BB where BB is Element of Dickson-bases(N, R): BB is finite};
set iN = {w where w is Element of NAT : s.(f.k) <= s.w & f.k < w};
consider BD being set such that
A45: BD is_Dickson-basis_of N,R and
A46: BD is finite by A1;
BD in Dickson-bases(N,R) by A1,A45,Def13;
then BD in BBX by A46;
then B in BBX by A43;
then
A47: ex BB being Element of Dickson-bases(N,R) st ( B = BB)&( BB is finite);
then
A48: B is_Dickson-basis_of N,R by A1,Def13;
now
deffunc F(Element of rng s) = Bi($1, f.k);
A49: B is finite by A47;
assume
A50: for b being Element of rng s st b in B holds Bi(b, f.k) is finite;
set Ball = {F(b) where b is Element of rng s : b in B };
A51: Ball is finite from FRAENKEL:sch 21(A49);
now
let X be set;
assume X in Ball;
then ex b being Element of rng s st ( X = Bi(b, f.k))&( b in B);
hence X is finite by A50;
end;
then
A52: union Ball is finite by A51,FINSET_1:7;
iN c= union Ball
proof
let x be object;
assume x in iN;
then consider w being Element of NAT such that
A53: x = w and
A54: s.(f.k) <= s.w and
A55: f.k < w;
A56: s.w in N by A41,A54,A55;
reconsider sw = s.w as Element of R;
consider b being Element of R such that
A57: b in B and
A58: b <= sw by A48,A56;
A59: B c= N by A48;
N c= rng s
proof
let x be object;
assume x in N;
then
A60: ex u being Element of NAT st ( x = s.u)&( s.(f.k) <= s.u)&(
f.k < u) by A41;
dom s = NAT by FUNCT_2:def 1;
hence thesis by A60,FUNCT_1:3;
end;
then B c= rng s by A59;
then reconsider b as Element of rng s by A57;
A61: w in Bi(b, f.k) by A55,A58;
Bi(b, f.k) in Ball by A57;
hence thesis by A53,A61,TARSKI:def 4;
end;
hence contradiction by A42,A52;
end;
then consider b being Element of rng s such that
A62: b in B and
A63: Bi(b, f.k) is infinite;
b in BALL by A62,A63;
then the Element of BALL in BALL;
then consider b being Element of B such that
A64: b = the Element of BALL and
A65: ex b9 being Element of rng s st b9=b & Bi(b9,f.k) is infinite;
B c= N by A48;
then b in N;
then
A66: ex w being Element of NAT st ( b = s.w)&( s.(f.k) <= s.w)&(
f.k < w) by A41;
then
A67: s.(f.(k+1)) = the Element of BALL by A44,A64,Def12;
A68: f.k < f.(k+1) by A44,A64,A66,Def12;
deffunc F(set) = $1;
defpred P[Nat] means f.k < $1 & s.(f.(k+1)) <= s.$1;
set W1 = {w1 where w1 is Element of NAT : s.(f.(k+1)) <= s.w1 & f.k < w1};
set W2 = {w1 where w1 is Element of NAT :
s.(f.(k+1)) <= s.w1 & f.(k+1) < w1};
set W3 = {F(w1) where w1 is Nat : w1 <= f.(k+1) & P[w1]};
A69: W3 is finite from FINSEQ_1:sch 6;
now
let x be object;
hereby
assume x in W1;
then consider w being Element of NAT such that
A70: x = w and
A71: s.(f.(k+1)) <= s.w and
A72: f.k < w;
w <= f.(k+1) or w > f.(k+1);
then x in W2 or x in W3 by A70,A71,A72;
hence x in W2 \/ W3 by XBOOLE_0:def 3;
end;
assume
A73: x in W2 \/ W3;
per cases by A73,XBOOLE_0:def 3;
suppose x in W2;
then consider w being Element of NAT such that
A74: x = w and
A75: s.(f.(k+1)) <= s.w and
A76: f.(k+1) < w;
f.k < w by A68,A76,XXREAL_0:2;
hence x in W1 by A74,A75;
end;
suppose x in W3;
then consider w being Nat such that
A77: x = w & w <= f.(k+1) & f.k < w & s.(f.(k+1)) <= s.w;
reconsider w as Element of NAT by ORDINAL1:def 12;
x = w & f.k < w & w <= f.(k+1) & s.(f.(k+1)) <= s.w by A77;
hence x in W1;
end;
end;
then W2 is infinite by A64,A65,A67,A69,TARSKI:2;
hence R[k+1] by A15;
end;
A78: for n being Nat holds R[n] from NAT_1:sch 2(A39,A40);
set t = s * f;
take t;
reconsider f as sequence of REAL by FUNCT_2:7,NUMBERS:19;
now
now
let n be Nat;
A79: n in NAT by ORDINAL1:def 12;
f.n in rng f by A16,A79,FUNCT_1:def 3;
then reconsider fn = f.n as Element of NAT by A17;
consider N being Subset of CR, B being non empty Subset of CR such that
A80: N = {s.w where w is Element of NAT : s.(fn) <= s.w & fn < w} and
A81: {w where w is Element of NAT : s.(fn) <= s.w & fn < w} is infinite and
A82: B = the Element of {BB where BB is Element of Dickson-bases(N, R):
BB is finite} and
A83: f.(n+1) = s mindex (the Element of {b where b is Element of B :
ex b9 being Element of rng s st b9=b & Bi(b9,fn) is infinite}, fn)
by A78;
set BBX = {BB where BB is Element of Dickson-bases(N, R): BB is finite};
set BJ = {b where b is Element of B : ex b9 being Element of rng s
st b9=b & Bi(b9,fn) is infinite};
set BC = the Element of BJ;
consider BD being set such that
A84: BD is_Dickson-basis_of N,R and
A85: BD is finite by A1;
BD in Dickson-bases(N,R) by A1,A84,Def13;
then BD in BBX by A85;
then B in BBX by A82;
then
A86: ex BB being Element of Dickson-bases(N,R) st ( B = BB)&( BB is finite);
then
A87: B is_Dickson-basis_of N,R by A1,Def13;
then
A88: B c= N;
now
A89: B is finite by A86;
assume
A90: for b being Element of rng s st b in B holds Bi(b, fn) is finite;
deffunc F(Element of rng s) = Bi($1, fn);
set Ball = {F(b) where b is Element of rng s : b in B};
set iN = {w where w is Element of NAT : s.(fn) <= s.w & fn < w};
A91: Ball is finite from FRAENKEL:sch 21(A89);
now
let X be set;
assume X in Ball;
then ex b being Element of rng s st ( X = Bi(b, fn))&( b in B);
hence X is finite by A90;
end;
then
A92: union Ball is finite by A91,FINSET_1:7;
iN c= union Ball
proof
let x be object;
assume x in iN;
then consider w being Element of NAT such that
A93: x = w and
A94: s.(fn) <= s.w and
A95: f.n < w;
A96: s.w in N by A80,A94,A95;
reconsider sw = s.w as Element of R;
consider b being Element of R such that
A97: b in B and
A98: b <= sw by A87,A96;
A99: B c= N by A87;
N c= rng s
proof
let x be object;
assume x in N;
then
A100: ex u being Element of NAT st ( x = s.u)&( s.(fn) <= s.u)&(
fn < u) by A80;
dom s = NAT by FUNCT_2:def 1;
hence thesis by A100,FUNCT_1:3;
end;
then B c= rng s by A99;
then reconsider b as Element of rng s by A97;
A101: w in Bi(b, fn) by A95,A98;
Bi(b, fn) in Ball by A97;
hence thesis by A93,A101,TARSKI:def 4;
end;
hence contradiction by A81,A92;
end;
then consider b being Element of rng s such that
A102: b in B and
A103: Bi(b, fn) is infinite;
b in BJ by A102,A103;
then BC in BJ;
then ex b being Element of B st ( BC = b)&( ex b9 being Element
of rng s st b9=b & Bi(b9,fn) is infinite);
then BC in N by A88;
then ex j being Element of NAT st ( BC = s.j)&( s.(fn) <= s.j)&(
fn < j) by A80;
hence f.n < f.(n+1) by A83,Def12;
end;
hence f is increasing by SEQM_3:def 6;
let n be Element of NAT;
f.n in rng f by A16,FUNCT_1:def 3;
hence f.n is Element of NAT by A17;
end;
then reconsider f as increasing sequence of NAT;
t = s * f;
hence t is subsequence of s;
let n be Nat;
n in NAT by ORDINAL1:def 12;
then
A104: t.n = s.(f.n) by A16,FUNCT_1:13;
A105: t.(n+1) = s.(f.(n+1)) by A16,FUNCT_1:13;
consider N being Subset of CR, B being non empty Subset of CR such that
A106: N = {s.w where w is Element of NAT : s.(f.n) <= s.w & f.n < w} and
A107: {w where w is Element of NAT: s.(f.n) <= s.w & f.n < w} is infinite and
A108: B = the Element of
{BB where BB is Element of Dickson-bases(N, R):BB is finite}
and
A109: f.(n+1) = s mindex ( the Element of {b where b is Element of B :
ex b9 being Element of rng s st b9=b & Bi(b9,f.n) is infinite}, f.n) by A78;
set BX = {b where b is Element of B : ex b9 being Element of rng s
st b9=b & Bi(b9,f.n) is infinite};
set sfn1 = the Element of BX;
set BBX = {BB where BB is Element of Dickson-bases(N, R):BB is finite};
consider BD being set such that
A110: BD is_Dickson-basis_of N,R and
A111: BD is finite by A1;
BD in Dickson-bases(N,R) by A1,A110,Def13;
then BD in BBX by A111;
then B in BBX by A108;
then
A112: ex BB being Element of Dickson-bases(N, R) st ( BB = B)&( BB is finite);
then
A113: B is_Dickson-basis_of N,R by A1,Def13;
now
A114: B is finite by A112;
assume
A115: for b being Element of rng s st b in B holds Bi(b, f.n) is finite;
deffunc F(Element of rng s) = Bi($1, f.n);
set Ball = {F(b) where b is Element of rng s : b in B };
set iN = {w where w is Element of NAT : s.(f.n) <= s.w & f.n < w};
A116: Ball is finite from FRAENKEL:sch 21(A114);
now
let X be set;
assume X in Ball;
then ex b being Element of rng s st ( X = Bi(b, f.n))&( b in B);
hence X is finite by A115;
end;
then
A117: union Ball is finite by A116,FINSET_1:7;
iN c= union Ball
proof
let x be object;
assume x in iN;
then consider w being Element of NAT such that
A118: x = w and
A119: s.(f.n) <= s.w and
A120: f.n < w;
A121: s.w in N by A106,A119,A120;
reconsider sw = s.w as Element of R;
consider b being Element of R such that
A122: b in B and
A123: b <= sw by A113,A121;
A124: B c= N by A113;
N c= rng s
proof
let x be object;
assume x in N;
then
A125: ex u being Element of NAT st ( x = s.u)&( s.(f.n) <= s.u)&(
f.n < u) by A106;
dom s = NAT by FUNCT_2:def 1;
hence thesis by A125,FUNCT_1:3;
end;
then B c= rng s by A124;
then reconsider b as Element of rng s by A122;
A126: w in Bi(b, f.n) by A120,A123;
Bi(b, f.n) in Ball by A122;
hence thesis by A118,A126,TARSKI:def 4;
end;
hence contradiction by A107,A117;
end;
then consider b being Element of rng s such that
A127: b in B and
A128: Bi(b, f.n) is infinite;
b in BX by A127,A128;
then sfn1 in BX;
then ex b being Element of B st ( b = sfn1)&( ex b9 being
Element of rng s st b9 = b & Bi(b9,f.n) is infinite);
then
A129: sfn1 in B;
B c= N by A113;
then sfn1 in N by A129;
then ex w being Element of NAT st ( sfn1 = s.w)&( s.(f.n) <= s.w
)&( f.n < w) by A106;
then t.n <= t.(n+1) by A104,A105,A109,Def12;
hence [t.n, t.(n+1)] in the InternalRel of R;
end;
theorem Th35:
for R being RelStr st R is empty holds R is Dickson
proof
let R be RelStr such that
A1: R is empty;
now
let N be Subset of R;
take B = {};
N = {} the carrier of R by A1;
hence B is_Dickson-basis_of N,R;
thus B is finite;
end;
hence thesis;
end;
theorem Th36: :: Theorem 4.46
for M, N be RelStr
st M is Dickson & N is Dickson & M is quasi_ordered & N is quasi_ordered
holds [:M,N:] is quasi_ordered & [:M,N:] is Dickson
proof
let M,N be RelStr such that
A1: M is Dickson and
A2: N is Dickson and
A3: M is quasi_ordered and
A4: N is quasi_ordered;
reconsider M9 = M as reflexive transitive RelStr by A3;
reconsider N9 = N as reflexive transitive RelStr by A4;
[:M9,N9:] is reflexive;
hence
A5: [:M,N:] is quasi_ordered;
per cases;
suppose M is non empty & N is non empty;
then reconsider Me=M,Ne=N as non empty RelStr;
set CPMN = [:Me,Ne:];
for f being sequence of [:Me,Ne:]
ex i,j being Nat st i < j & f.i <= f.j
proof
let f be sequence of [:Me,Ne:];
deffunc F(Element of NAT) = (f.$1)`1;
consider a being sequence of the carrier of Me such that
A6: for x being Element of NAT holds a.x = F(x) from FUNCT_2:sch 4;
reconsider a as sequence of Me;
consider sa being sequence of Me such that
A7: sa is subsequence of a and
A8: sa is weakly-ascending by A1,Th34;
consider NS being increasing sequence of NAT such that
A9: sa = a * NS by A7,VALUED_0:def 17;
deffunc G(Element of NAT) = (f.(NS.$1))`2;
consider b being sequence of the carrier of Ne such that
A10: for x being Element of NAT holds b.x = G(x) from FUNCT_2:sch 4;
reconsider b as sequence of Ne;
consider i,j being Nat such that
A11: i < j and
A12: b.i <= b.j by A2,Th28;
A13: i in NAT by ORDINAL1:def 12;
A14: j in NAT by ORDINAL1:def 12;
take NS.i, NS.j;
dom NS = NAT by FUNCT_2:def 1;
hence NS.i < NS.j by A11,VALUED_0:def 13,A13,A14;
reconsider x = f.(NS.i), y = f.(NS.j) as Element of [:Me,Ne:];
A15: dom sa = NAT by FUNCT_2:def 1;
then
A16: sa.i = a.(NS.i) by A9,FUNCT_1:12,A13
.= (f.(NS.i))`1 by A6;
A17: sa.j = a.(NS.j) by A9,A15,FUNCT_1:12,A14
.= (f.(NS.j))`1 by A6;
M is transitive by A3;
then
A18: x`1 <= y`1 by A8,A11,A16,A17,Th3;
A19: b.i = x`2 by A10,A13;
b.j =y`2 by A10,A14;
hence thesis by A12,A18,A19,YELLOW_3:12;
end;
then for N being non empty Subset of CPMN
holds min-classes N is finite & min-classes N is non empty by A5,Th30;
hence thesis by A5,Th31;
end;
suppose
A20: not (M is non empty & N is non empty);
now per cases by A20;
suppose M is empty;
then reconsider M2 = the carrier of M as empty set;
[: M2, the carrier of N:] is empty;
hence [:the carrier of M, the carrier of N:] is empty;
end;
suppose N is empty;
then reconsider N2 = the carrier of N as empty set;
[:the carrier of M, N2 :] is empty;
hence [:the carrier of M, the carrier of N:] is empty;
end;
end;
then [:M,N:] is empty by YELLOW_3:def 2;
hence thesis by Th35;
end;
end;
theorem Th37:
for R, S being RelStr st R,S are_isomorphic & R is Dickson & R is quasi_ordered
holds S is quasi_ordered & S is Dickson
proof
let R, S be RelStr such that
A1: R,S are_isomorphic and
A2: R is Dickson and
A3: R is quasi_ordered;
set CRS = the carrier of S, IRS = the InternalRel of S;
per cases;
suppose R is not empty & S is not empty;
then reconsider Re = R, Se = S as non empty RelStr;
consider f being Function of Re,Se such that
A4: f is isomorphic by A1,WAYBEL_1:def 8;
A5: f is one-to-one by A4,WAYBEL_0:66;
A6: rng f = the carrier of Se by A4,WAYBEL_0:66;
A7: Re is reflexive by A3;
A8: Re is transitive by A3;
A9: Se is reflexive by A1,A7,WAYBEL20:15;
Se is transitive by A1,A8,WAYBEL20:16;
hence
A10: S is quasi_ordered by A9;
now
let t be sequence of Se;
reconsider fi = f" as Function of the carrier of Se,
the carrier of Re by A5,A6,FUNCT_2:25;
deffunc F(Element of NAT) = fi.(t.$1);
consider sr being sequence of the carrier of Re such that
A11: for x being Element of NAT holds sr.x = F(x) from FUNCT_2:sch 4;
reconsider sr as sequence of Re;
consider i,j being Nat such that
A12: i < j and
A13: sr.i <= sr.j by A2,Th28;
take i,j;
A14: i in NAT by ORDINAL1:def 12;
A15: j in NAT by ORDINAL1:def 12;
thus i < j by A12;
A16: f.(sr.i) = f.(f".(t.i)) by A11,A14
.= t.i by A5,A6,FUNCT_1:35;
f.(sr.j) = f.(f".(t.j)) by A11,A15
.= t.j by A5,A6,FUNCT_1:35;
hence t.i <= t.j by A4,A13,A16,WAYBEL_0:66;
end;
then for N being non empty Subset of Se
holds min-classes N is finite & min-classes N is non empty by A10,Th30;
hence thesis by A10,Th31;
end;
suppose
A17: not(R is not empty & S is not empty);
A18: now per cases by A17;
suppose
A19: R is empty;
ex f being Function of R,S st ( f is isomorphic) by A1,WAYBEL_1:def 8;
hence S is empty by A19,WAYBEL_0:def 38;
end;
suppose S is empty;
hence S is empty;
end;
end;
then for x being object st x in CRS holds [x,x] in IRS;
then
A20: IRS is_reflexive_in CRS;
for x,y,z be object
st x in CRS & y in CRS & z in CRS & [x,y] in IRS & [y,z] in IRS
holds [x,z] in IRS by A18;
then
A21: IRS is_transitive_in CRS;
A22: S is reflexive by A20;
S is transitive by A21;
hence S is quasi_ordered by A22;
thus thesis by A18,Th35;
end;
end;
theorem Th38:
for p being RelStr-yielding ManySortedSet of {0}, z being Element of {0}
holds p.z, product p are_isomorphic
proof
let p be RelStr-yielding ManySortedSet of {0}, z be Element of {0};
deffunc F(object) = 0 .--> $1;
consider f being Function such that
A1: dom f = the carrier of p.z and
A2: for x being object st x in the carrier of p.z holds f.x = F(x) from
FUNCT_1:sch 3;
A3: z = 0 by TARSKI:def 1;
A4: 0 in {0} by TARSKI:def 1;
now
let x be object;
assume
A5: x in the carrier of p.z;
then
A6: f.x = 0.-->x by A2;
set g = 0 .--> x;
A7: dom g = {0}
.= dom Carrier p by PARTFUN1:def 2;
now
let y be object;
assume y in dom Carrier p;
then
A8: y in {0};
then
A9: y = 0 by TARSKI:def 1;
ex R being 1-sorted st ( R = p.y)&( (Carrier p).y = the
carrier of R) by A8,PRALG_1:def 15;
hence g.y in (Carrier p).y by A3,A5,A9;
end;
then f.x in product Carrier p by A6,A7,CARD_3:def 5;
hence f.x in the carrier of product p by YELLOW_1:def 4;
end;
then reconsider f as Function of p.z, product p by A1,FUNCT_2:3;
now
per cases;
suppose
A10: p.z is empty;
now
assume the carrier of product p is not empty;
then
A11: product Carrier p is non empty by YELLOW_1:def 4;
set x = the Element of product Carrier p;
A12: ex g being Function st ( x = g)&( dom g = dom (Carrier p))&
( for y being object st y in dom Carrier p holds g.y in (Carrier p).y) by A11,
CARD_3:def 5;
A13: 0 in dom Carrier p by A4,PARTFUN1:def 2;
consider R being 1-sorted such that
A14: R = p.0 and
A15: (Carrier p).0 = the carrier of R by A4,PRALG_1:def 15;
R is empty by A10,A14,TARSKI:def 1;
hence contradiction by A12,A13,A15;
end;
then product p is empty;
hence f is isomorphic by A10,WAYBEL_0:def 38;
end;
suppose
A16: p.z is non empty;
then reconsider pz = p.z as non empty RelStr;
now
let i be set;
assume i in rng p;
then consider x being object such that
A17: x in dom p and
A18: i = p.x by FUNCT_1:def 3;
x in {0} by A17;
then i = p.0 by A18,TARSKI:def 1;
hence i is non empty 1-sorted by A16,TARSKI:def 1;
end;
then reconsider np = p as yielding_non-empty_carriers
RelStr-yielding ManySortedSet of {0} by YELLOW_6:def 2;
product np is non empty;
then reconsider pp = product p as non empty RelStr;
now
let x1, x2 be object such that
A19: x1 in dom f and
A20: x2 in dom f and
A21: f.x1 = f.x2;
A22: f.x1 = 0 .--> x1 by A2,A19
.= [:{0}, {x1}:];
A23: f.x2 = 0 .--> x2 by A2,A20
.= [:{0}, {x2}:];
A24: 0 in {0} by TARSKI:def 1;
x1 in {x1} by TARSKI:def 1;
then [0, x1] in f.x2 by A21,A22,A24,ZFMISC_1:def 2;
then ex xa,ya being object st ( xa in {0})&( ya in {x2})&( [0,x1] =
[xa,ya]) by A23,ZFMISC_1:def 2;
then x1 in {x2} by XTUPLE_0:1;
hence x1 = x2 by TARSKI:def 1;
end;
then
A25: f is one-to-one by FUNCT_1:def 4;
now
let y be object;
thus y in rng f implies y in the carrier of product p;
assume y in the carrier of product p;
then y in product Carrier p by YELLOW_1:def 4;
then consider g being Function such that
A26: y = g and
A27: dom g = dom (Carrier p) and
A28: for x being object st x in dom Carrier p holds g.x in (Carrier p).x
by CARD_3:def 5;
A29: dom g = {0} by A27,PARTFUN1:def 2;
A30: 0 in dom Carrier p by A4,PARTFUN1:def 2;
A31: ex R being 1-sorted st ( R = p.0)&( (Carrier p).0 = the
carrier of R) by A4,PRALG_1:def 15;
A32: g = 0 .--> g.0 by A29,Th1;
A33: f.(g.0) = 0 .--> g.0 by A2,A3,A28,A30,A31;
g.0 in dom f by A1,A3,A28,A30,A31;
hence y in rng f by A26,A32,A33,FUNCT_1:def 3;
end;
then
A34: rng f = the carrier of product p by TARSKI:2;
reconsider f9 = f as Function of pz, pp;
now
let x, y be Element of pz;
product np is non empty;
then
A35: product Carrier p is non empty by YELLOW_1:def 4;
A36: f9.x is Element of product Carrier p by YELLOW_1:def 4;
hereby
assume
A37: x <= y;
ex f1,g1 being Function st f1 = f9.x & g1 = f9.y &
for i be object st i in {0}
ex R being RelStr, xi,yi being Element of R
st R = p.i & xi = f1.i & yi = g1.i & xi <= yi
proof
set f1 = 0 .--> x;
set g1 = 0 .--> y;
reconsider f1 as Function;
reconsider g1 as Function;
take f1, g1;
thus f1 = f9.x by A2;
thus g1 = f9.y by A2;
let i be object such that
A38: i in {0};
A39: i = 0 by A38,TARSKI:def 1;
0 in dom p by A4,PARTFUN1:def 2;
then p.0 in rng p by FUNCT_1:def 3;
then reconsider p0 = p.0 as RelStr by YELLOW_1:def 3;
set R = p0;
reconsider x9=x as Element of R by TARSKI:def 1;
reconsider y9=y as Element of R by TARSKI:def 1;
take R, x9, y9;
thus R = p.i by A38,TARSKI:def 1;
thus x9 = f1.i by A39,FUNCOP_1:72;
thus y9 = g1.i by A39,FUNCOP_1:72;
thus thesis by A37,TARSKI:def 1;
end;
hence f9.x <= f9.y by A35,A36,YELLOW_1:def 4;
end;
assume f9.x <= f9.y;
then consider f1, g1 being Function such that
A40: f1 = f9.x and
A41: g1 = f9.y and
A42: for
i being object st i in {0} ex R being RelStr, xi, yi being Element of R
st R = p.i & xi = f1.i & yi = g1.i & xi <= yi
by A35,A36,YELLOW_1:def 4;
consider R being RelStr, xi, yi being Element of R such that
A43: R = p.0 and
A44: xi = f1.0 and
A45: yi = g1.0 and
A46: xi <= yi by A4,A42;
f1 = 0 .--> x by A2,A40;
then
A47: xi = x by A44,FUNCOP_1:72;
A48: g1 = 0 .--> y by A2,A41;
R = pz by A43,TARSKI:def 1;
hence x <= y by A45,A46,A47,A48,FUNCOP_1:72;
end;
hence f is isomorphic by A25,A34,WAYBEL_0:66;
end;
end;
hence thesis by WAYBEL_1:def 8;
end;
registration
let X be set, p be RelStr-yielding ManySortedSet of X, Y be Subset of X;
cluster p|Y -> RelStr-yielding;
coherence
proof
now
let v be set;
assume v in rng (p|Y);
then consider x being object such that
A1: x in dom (p|Y) and
A2: v = (p|Y).x by FUNCT_1:def 3;
A3: x in Y by A1;
then
A4: (p|Y).x = p.x by FUNCT_1:49;
x in X by A3;
then x in dom p by PARTFUN1:def 2;
then p.x in rng p by FUNCT_1:3;
hence v is RelStr by A2,A4,YELLOW_1:def 3;
end;
hence thesis by YELLOW_1:def 3;
end;
end;
theorem Th39:
for n being non zero Nat, p being RelStr-yielding ManySortedSet of n
holds product p is non empty iff p is non-Empty
proof
let n be non zero Nat, p be RelStr-yielding ManySortedSet of n;
hereby
assume product p is non empty;
then product Carrier p is non empty by YELLOW_1:def 4;
then consider z being object such that
A1: z in product Carrier p by XBOOLE_0:def 1;
A2: ex g being Function st ( z = g)&( dom g = dom (Carrier p))&
( for i being object st i in dom (Carrier p) holds g.i in (Carrier p).i)
by A1,
CARD_3:def 5;
now
let S be 1-sorted;
assume S in rng p;
then consider x being object such that
A3: x in dom p and
A4: S = p.x by FUNCT_1:def 3;
A5: x in n by A3;
then
A6: x in dom (Carrier p) by PARTFUN1:def 2;
ex R being 1-sorted st ( R = p.x)&( (Carrier p).x = the
carrier of R) by A5,PRALG_1:def 15;
hence S is non empty by A2,A4,A6;
end;
hence p is non-Empty by WAYBEL_3:def 7;
end;
assume
A7: p is non-Empty;
A8: dom Carrier p = n by PARTFUN1:def 2;
:: Funkcja Kuratowskiego !!!
deffunc F(object) = the Element of (Carrier p).$1;
consider g being Function such that
A9: dom g = dom Carrier p and
A10: for
i being object st i in dom Carrier p holds g.i = F(i) from FUNCT_1:sch 3;
set x = g;
now
take g;
thus x = g;
thus dom g = dom Carrier p by A9;
thus
for i being object st i in dom Carrier p holds g.i in (Carrier p).i
proof
let i be object such that
A11: i in dom Carrier p;
i in dom p by A8,A11,PARTFUN1:def 2;
then
A12: p.i in rng p by FUNCT_1:def 3;
then reconsider pi1 = p.i as RelStr by YELLOW_1:def 3;
pi1 is non empty by A7,A12,WAYBEL_3:def 7;
then
A13: the carrier of pi1 is non empty;
i in n by A11;
then
A14: ex R being 1-sorted st ( R = p.i)&( (Carrier p).i = the
carrier of R) by PRALG_1:def 15;
g.i = the Element of (Carrier p).i by A10,A11;
hence thesis by A13,A14;
end;
end;
then product Carrier p is non empty by CARD_3:def 5;
hence thesis by YELLOW_1:def 4;
end;
theorem Th40:
for n being non zero Nat,
p being RelStr-yielding ManySortedSet of Segm(n+1),
ns being Subset of Segm(n+1), ne being Element of Segm(n+1)
st ns = n & ne = n holds [:product(p|ns), p.ne:], product p are_isomorphic
proof
let n be non zero Nat,
p be RelStr-yielding ManySortedSet of Segm(n+1),
ns be Subset of Segm(n+1), ne be Element of Segm(n+1) such that
A1: ns = n and
A2: ne = n;
set S = [: product (p|ns), p.ne:];
set T = product p;
set CP = [: the carrier of product (p|ns), the carrier of p.ne:];
set CPP = the carrier of product p;
A3: dom Carrier (p|ns) = n by A1,PARTFUN1:def 2;
per cases;
suppose
A4: the carrier of product p is empty;
then
A5: T is empty;
not p is non-Empty by A4;
then consider r1 being 1-sorted such that
A6: r1 in rng p and
A7: r1 is empty by WAYBEL_3:def 7;
consider x being object such that
A8: x in dom p and
A9: r1 = p.x by A6,FUNCT_1:def 3;
x in Segm(n+1) by A8;
then
A10: x in Segm n \/ {n} by AFINSQ_1:2;
A11: S is empty
proof
per cases by A10,XBOOLE_0:def 3;
suppose
A12: x in n;
then
A13: (p|ns).x = p.x by A1,FUNCT_1:49;
x in dom(p|ns) by A1,A12,PARTFUN1:def 2;
then p.x in rng (p|ns) by A13,FUNCT_1:def 3;
then not (p|ns) is non-Empty by A7,A9,WAYBEL_3:def 7;
then reconsider
ptemp = the carrier of product (p|ns) as empty set by A1,Th39;
[: ptemp, the carrier of p.ne :] is empty;
hence thesis by YELLOW_3:def 2;
end;
suppose x in {n};
then p.ne is empty by A2,A7,A9,TARSKI:def 1;
then reconsider pne = the carrier of p.ne as empty set;
reconsider ptemp = the carrier of product (p|ns) as set;
[: ptemp, pne :] is empty;
hence thesis by YELLOW_3:def 2;
end;
end;
then A14: dom {} = the carrier of S;
for x being object st x in {} holds {}.x in the carrier of T;
then reconsider f = {} as Function of S, T by A14,FUNCT_2:3;
f is isomorphic by A5,A11,WAYBEL_0:def 38;
hence thesis by WAYBEL_1:def 8;
end;
suppose
A15: the carrier of product p is non empty;
then reconsider CPP as non empty set;
reconsider T as non empty RelStr by A15;
A16: p is non-Empty by A15,Th39;
reconsider p9=p as RelStr-yielding non-Empty ManySortedSet of Segm(n+1)
by A15,Th39;
p9.ne is non empty;
then reconsider pne2 = the carrier of p.ne as non empty set;
now
let S be 1-sorted;
assume S in rng (p|ns);
then consider x being object such that
A17: x in dom (p|ns) and
A18: S = (p|ns).x by FUNCT_1:def 3;
x in ns by A17;
then x in n+1;
then
A19: x in dom p by PARTFUN1:def 2;
S = p.x by A17,A18,FUNCT_1:47;
then S in rng p by A19,FUNCT_1:def 3;
hence S is non empty by A16,WAYBEL_3:def 7;
end;
then
A20: p|ns is non-Empty by WAYBEL_3:def 7;
then
A21: product (p|ns) is non empty;
reconsider ppns2 = the carrier of product (p|ns) as non empty set
by A20;
CP = [: ppns2, pne2 :];
then reconsider S as non empty RelStr by YELLOW_3:def 2;
CP = the carrier of S by YELLOW_3:def 2;
then reconsider CP9 = CP as non empty set;
defpred P[set,set] means ex a being Function, b being Element of pne2
st a in ppns2 & $1 = [a,b] & $2 = a +* (n.-->b);
A22: for x being Element of CP9 ex y being Element of CPP st P[x,y]
proof
let x be Element of CP9;
reconsider xx = x as Element of [: ppns2, pne2 :];
set a = xx`1, b = xx`2;
reconsider a as Element of ppns2 by MCART_1:10;
reconsider b as Element of pne2 by MCART_1:10;
A23: product Carrier (p|ns) is non empty by A21,YELLOW_1:def 4;
A24: a is Element of product Carrier (p|ns) by YELLOW_1:def 4;
then
A25: ex g being Function st ( a = g)&( dom g = dom Carrier (p|ns
))&( for i being object st i in dom Carrier (p|ns)
holds g.i in (Carrier (p|ns)).i
) by A23,CARD_3:def 5;
reconsider a as Function by A24;
set y = a +* (n.-->b);
now
set g1 = y;
reconsider g1 as Function;
take g1;
thus y = g1;
A26: dom a = ns by A25,PARTFUN1:def 2;
thus dom g1 = dom a \/ dom (n.-->b) by FUNCT_4:def 1
.= Segm n \/ {n} by A1,A26
.= Segm(n+1) by AFINSQ_1:2
.= dom (Carrier p) by PARTFUN1:def 2;
let x be object;
assume x in dom (Carrier p);
then
A27: x in Segm(n+1);
then
A28: x in Segm n \/ {n} by AFINSQ_1:2;
per cases by A28,XBOOLE_0:def 3;
suppose
A29: x in n;
x <> n
proof
assume
A: x = n; then
reconsider x as set;
not x in x;
hence thesis by A,A29;
end;
then not x in dom(n.-->b) by TARSKI:def 1;
then
A30: g1.x = a.x by FUNCT_4:11;
A31: x in dom(Carrier (p|ns)) by A1,A29,PARTFUN1:def 2;
A32: ex R being 1-sorted st ( R = (p|ns).x)&( (Carrier (p|ns)).x
= the carrier of R) by A1,A29,PRALG_1:def 15;
ex R2 being 1-sorted st ( R2 = p.x)&( (Carrier p).x = the
carrier of R2) by A27,PRALG_1:def 15;
then (Carrier (p|ns)).x = (Carrier p).x by A1,A29,A32,FUNCT_1:49;
hence g1.x in (Carrier p).x by A25,A30,A31;
end;
suppose
A33: x in {n};
then
A34: x = n by TARSKI:def 1;
x in dom (n.-->b) by A33;
then
A35: g1.x = (n.-->b).n by A34,FUNCT_4:13
.= b by FUNCOP_1:72;
ex R being 1-sorted st ( R = p.ne)&( (Carrier p).ne = the
carrier of R) by PRALG_1:def 15;
hence g1.x in (Carrier p).x by A2,A34,A35;
end;
end;
then y in product Carrier p by CARD_3:def 5;
then reconsider y as Element of CPP by YELLOW_1:def 4;
take y,a,b;
thus a in ppns2;
thus x = [a,b] by MCART_1:21;
thus thesis;
end;
consider f being Function of CP9, CPP such that
A36: for x being Element of CP9 holds P[x,f.x] from FUNCT_2:sch 3(A22);
now
the carrier of [:product(p|ns), p.ne :] =
[:the carrier of product(p|ns),the carrier of p.ne:] by YELLOW_3:def 2;
then reconsider f as Function of [:product (p|ns), p.ne:], product p;
reconsider f9=f as Function of S, T;
take f;
now
let x1,x2 be object such that
A37: x1 in dom f and
A38: x2 in dom f and
A39: f.x1 = f.x2;
x1 is Element of [:the carrier of product (p|ns),
the carrier of p.ne :] by A37,YELLOW_3:def 2;
then consider a1 being Function, b1 being Element of pne2 such that
A40: a1 in ppns2 and
A41: x1 = [a1, b1] and
A42: f.x1 = a1 +* (n.-->b1) by A36;
x2 is Element of [: the carrier of product (p|ns),
the carrier of p.ne :] by A38,YELLOW_3:def 2;
then consider a2 being Function, b2 being Element of pne2 such that
A43: a2 in ppns2 and
A44: x2 = [a2, b2] and
A45: f.x2 = a2 +* (n.-->b2) by A36;
a1 in product Carrier (p|ns) by A40,YELLOW_1:def 4;
then
A46: ex g1 being Function st ( a1 = g1)&( dom g1 = dom Carrier (
p|ns))&( for x being object st x in dom Carrier (p|ns)
holds g1.x in (Carrier (p|
ns)).x) by CARD_3:def 5;
a2 in product Carrier (p|ns) by A43,YELLOW_1:def 4;
then
A47: ex g2 being Function st ( a2 = g2)&( dom g2 = dom Carrier (
p|ns))&( for x being object st x in dom Carrier (p|ns)
holds g2.x in (Carrier (p|
ns)).x) by CARD_3:def 5;
A50: dom a1 = n by A1,A46,PARTFUN1:def 2;
A51: now
assume not n misses {n};
then n /\ {n} <> {} by XBOOLE_0:def 7;
then consider x being object such that
A52: x in n /\ {n} by XBOOLE_0:def 1;
A53: x in n by A52,XBOOLE_0:def 4;
x in {n} by A52,XBOOLE_0:def 4;
then B: x = n by TARSKI:def 1; then
reconsider x as set;
not x in n by B;
hence contradiction by A53;
end;
then
A54: dom a1 misses dom (n.-->b1) by A50;
A55: dom a2 misses dom (n.-->b2) by A46,A47,A50,A51;
A56: now
let a, b be object;
hereby
assume
A57: [a,b] in a1;
then
A58: a in dom a1 by FUNCT_1:1;
A59: b = a1.a by A57,FUNCT_1:1;
A60: a in dom a1 \/ dom (n.-->b1) by A58,XBOOLE_0:def 3;
then not a in dom (n.-->b1) by A54,A58,XBOOLE_0:5;
then
A61: (a2+*(n.-->b2)).a = a1.a by A39,A42,A45,A60,FUNCT_4:def 1;
A62: a in dom a2 \/ dom (n.-->b2) by A46,A47,A58,XBOOLE_0:def 3;
A63: a in dom a2 by A46,A47,A57,FUNCT_1:1;
then not a in dom (n.-->b2) by A55,A62,XBOOLE_0:5;
then b = a2.a by A59,A61,A62,FUNCT_4:def 1;
hence [a,b] in a2 by A63,FUNCT_1:1;
end;
assume
A64: [a,b] in a2;
then
A65: a in dom a2 by FUNCT_1:1;
A66: b = a2.a by A64,FUNCT_1:1;
A67: a in dom a2 \/ dom (n.-->b2) by A65,XBOOLE_0:def 3;
then not a in dom (n.-->b2) by A55,A65,XBOOLE_0:5;
then
A68: (a1 +* (n.-->b1)).a = a2.a by A39,A42,A45,A67,FUNCT_4:def 1;
A69: a in dom a1 \/ dom (n.-->b1) by A46,A47,A65,XBOOLE_0:def 3;
A70: a in dom a1 by A46,A47,A64,FUNCT_1:1;
then not a in dom (n.-->b1) by A54,A69,XBOOLE_0:5;
then b = a1.a by A66,A68,A69,FUNCT_4:def 1;
hence [a,b] in a1 by A70,FUNCT_1:1;
end;
A71: n in dom (n.-->b1) by TARSKI:def 1;
then
A72: n in dom a1 \/ dom (n.-->b1) by XBOOLE_0:def 3;
A73: n in dom (n.-->b2) by TARSKI:def 1;
then n in dom a2 \/ dom (n.-->b2) by XBOOLE_0:def 3;
then (a1 +* (n.-->b1)).n = (n.-->b2).n by A39,A42,A45,A73,FUNCT_4:def 1
.= b2 by FUNCOP_1:72;
then b2 = (n.-->b1).n by A71,A72,FUNCT_4:def 1
.= b1 by FUNCOP_1:72;
hence x1 = x2 by A41,A44,A56,RELAT_1:def 2;
end;
then
A74: f is one-to-one by FUNCT_1:def 4;
now
let y be object;
thus y in rng f implies y in the carrier of product p;
assume y in the carrier of product p;
then y in product Carrier p by YELLOW_1:def 4;
then consider g being Function such that
A75: y = g and
A76: dom g = dom (Carrier p) and
A77: for x being object st x in dom Carrier p holds g.x in (Carrier p).x
by CARD_3:def 5;
A78: dom Carrier p = n+1 by PARTFUN1:def 2;
A79: n+1 = {i where i is Nat : i < n+1} by AXIOMS:4;
n < n+1 by NAT_1:13;
then
A80: n in n+1 by A79;
set a = g|n, b = g.n;
set x = [a,b];
A81: dom (Carrier (p|ns)) = ns by PARTFUN1:def 2;
A82: dom a = dom g /\ Segm n by RELAT_1:61
.= Segm(n+1) /\ Segm n by A76,PARTFUN1:def 2;
then
A83: dom a = Segm n by NAT_1:63,XBOOLE_1:28;
A84: dom a = dom (Carrier (p|ns)) by A1,A81,A82,XBOOLE_1:28;
now
let x be object;
assume x in dom (Carrier (p|ns));
then
A85: x in n by A1;
A86: Segm n c= Segm(n+1) by NAT_1:63;
A87: a.x = g.x by A85,FUNCT_1:49;
A88: g.x in (Carrier p).x by A77,A78,A85,A86;
A89: ex R1 being 1-sorted st ( R1 = p.x)&( (Carrier p).x = the
carrier of R1) by A85,A86,PRALG_1:def 15;
ex R2 being 1-sorted st ( R2 = (p|ns).x)&( (Carrier (p|ns))
.x = the carrier of R2) by A1,A85,PRALG_1:def 15;
hence a.x in (Carrier (p|ns)).x by A1,A85,A87,A88,A89,FUNCT_1:49;
end;
then a in product (Carrier (p|ns)) by A84,CARD_3:9;
then
A90: a in the carrier of product(p|ns) by YELLOW_1:def 4;
ex R1 being 1-sorted st ( R1 = p.n)&( (Carrier p).n = the
carrier of R1) by A80,PRALG_1:def 15;
then
A91: b in the carrier of p.ne by A2,A77,A78;
then [a,b] in [:the carrier of product(p|ns), the carrier of p.ne :]
by A90,ZFMISC_1:87;
then
A92: x in dom f by FUNCT_2:def 1;
x is Element of CP9 by A90,A91,ZFMISC_1:87;
then consider ta being Function, tb being Element of pne2 such that
ta in ppns2 and
A93: x = [ta, tb] and
A94: f.x = ta +* (n.-->tb) by A36;
A95: ta = a by A93,XTUPLE_0:1;
A96: tb = b by A93,XTUPLE_0:1;
now
let i, j be object;
hereby
assume
A97: [i,j] in (a+*(n.-->b));
then i in dom (a +* (n.-->b)) by FUNCT_1:1;
then
A98: i in ((dom a) \/ dom ((n.-->b))) by FUNCT_4:def 1;
then
A99: i in Segm n \/ {n} by A83;
A100: (a+*(n.-->b)).i = j by A97,FUNCT_1:1;
per cases;
suppose
A101: i in dom ((n.-->b));
then i in {n};
then
A102: i = n by TARSKI:def 1;
(a+*(n.-->b)).i = (n.-->b).i by A98,A101,FUNCT_4:def 1
.= b by A102,FUNCOP_1:72;
then
A103: g.i = j by A97,A102,FUNCT_1:1;
i in dom g by A76,A78,A99,AFINSQ_1:2;
hence [i,j] in g by A103,FUNCT_1:1;
end;
suppose
A104: not i in dom ((n.-->b));
then not i in {n};
then
A105: i in n by A99,XBOOLE_0:def 3;
(a +* (n.-->b)).i = a.i by A98,A104,FUNCT_4:def 1;
then
A106: g.i = j by A100,A105,FUNCT_1:49;
i in dom g by A76,A78,A99,AFINSQ_1:2;
hence [i,j] in g by A106,FUNCT_1:1;
end;
end;
assume
A107: [i,j] in g;
then
A108: i in Segm(n+1) by A76,A78,FUNCT_1:1;
then
A109: i in Segm n \/ {n} by AFINSQ_1:2;
dom (a+* (n.-->b)) = dom a \/ dom (n.-->b) by FUNCT_4:def 1
.= Segm n \/ {n} by A83;
then
A110: i in dom (a+*(n.-->b)) by A108,AFINSQ_1:2;
then
A111: i in dom a \/ dom (n.-->b) by FUNCT_4:def 1;
per cases;
suppose
A112: i in dom (n.-->b);
then i in {n};
then
A113: i = n by TARSKI:def 1;
(a+* (n.-->b)).i = (n.-->b).i by A111,A112,FUNCT_4:def 1
.= b by A113,FUNCOP_1:72
.= j by A107,A113,FUNCT_1:1;
hence [i,j] in (a+*(n.-->b)) by A110,FUNCT_1:1;
end;
suppose
A114: not i in dom (n.-->b);
then not i in {n};
then
A115: i in n by A109,XBOOLE_0:def 3;
(a+*(n.-->b)).i = a.i by A111,A114,FUNCT_4:def 1
.= g.i by A115,FUNCT_1:49
.= j by A107,FUNCT_1:1;
hence [i,j] in (a+*(n.-->b)) by A110,FUNCT_1:1;
end;
end;
then f.x = y by A75,A94,A95,A96,RELAT_1:def 2;
hence y in rng f by A92,FUNCT_1:def 3;
end;
then
A116: rng f = the carrier of product p by TARSKI:2;
now
let x, y be Element of S;
A117: x is Element of CP by YELLOW_3:def 2;
then consider xa being Function, xb being Element of pne2 such that
A118: xa in ppns2 and
A119: x = [xa,xb] and
A120: f.x = xa +* (n.-->xb) by A36;
dom f = CP9 by FUNCT_2:def 1;
then f.x in the carrier of product p by A116,A117,FUNCT_1:def 3;
then
A121: f9.x in product Carrier p by YELLOW_1:def 4;
y is Element of CP by YELLOW_3:def 2;
then consider ya being Function, yb being Element of pne2 such that
A122: ya in ppns2 and
A123: y = [ya,yb] and
A124: f.y = ya +* (n.-->yb) by A36;
A125: xa in product Carrier (p|ns) by A118,YELLOW_1:def 4;
then
A126: ex gx being Function st ( xa = gx)&( dom gx = dom Carrier (
p|ns))&( for x being object st x in dom Carrier (p|ns)
holds gx.x in (Carrier (p|
ns)).x) by CARD_3:def 5;
then
A127: dom xa = n by A1,PARTFUN1:def 2;
then
A128: dom xa \/ dom (n.-->xb) = Segm n \/ {n};
ya in product Carrier(p|ns) by A122,YELLOW_1:def 4;
then
A129: ex gy being Function st ( ya = gy)&( dom gy = dom Carrier (
p|ns))&( for x being object st x in dom Carrier (p|ns)
holds gy.x in (Carrier (p|
ns)).x) by CARD_3:def 5;
then
A130: dom ya = n by A1,PARTFUN1:def 2;
then
A131: dom ya \/ dom (n.-->yb) = Segm n \/ {n};
reconsider xa9=xa as Element of product(p|ns) by A118;
reconsider ya9=ya as Element of product(p|ns) by A122;
hereby
assume x <= y;
then [x,y] in the InternalRel of S;
then
A132: [x,y] in ["the InternalRel of product(p|ns),
the InternalRel of p.ne"] by YELLOW_3:def 2;
then
A133: [[x,y]`1`1,[x,y]`2`1] in the InternalRel of product(p| ns ) by
YELLOW_3:10;
A134: [[x,y]`1`2,[x,y]`2`2] in the InternalRel of p.ne by A132,YELLOW_3:10;
A135: [xa,ya] in the InternalRel of product(p|ns)
by A123,A133,A119;
A136: xa in product Carrier(p|ns) by A118,YELLOW_1:def 4;
xa9 <= ya9 by A135;
then consider ffx,ggx being Function such that
A137: ffx = xa and
A138: ggx = ya and
A139: for i being object st i in n
ex RR being RelStr, xxi, yyi being Element of RR
st RR = (p|ns).i & xxi = ffx.i & yyi = ggx.i & xxi <= yyi
by A1,A136,YELLOW_1:def 4;
A140: [xb,yb] in the InternalRel of p.ne
by A123,A134,A119;
reconsider xb9=xb as Element of p.ne;
reconsider yb9=yb as Element of p.ne;
A141: xb9 <= yb9 by A140;
ex f1,g1 being Function st f1 = f.x & g1 = f.y &
for i being object st i in Segm(n+1)
ex R being RelStr, xi, yi being Element of R
st R = p.i & xi = f1.i & yi = g1.i & xi <= yi
proof
set f1 = xa +* (n.-->xb), g1 = ya +* (n.-->yb);
take f1, g1;
thus f1 = f.x by A120;
thus g1 = f.y by A124;
let i be object such that
A142: i in Segm(n+1);
A143: i in Segm n \/ {n} by A142,AFINSQ_1:2;
set R = p.i;
set xi = f1.i;
set yi = g1.i;
i in dom p by A142,PARTFUN1:def 2;
then p.i in rng p by FUNCT_1:def 3;
then reconsider R as RelStr by YELLOW_1:def 3;
A144: i in dom xa \/ dom (n.-->xb) by A128,A142,AFINSQ_1:2;
now per cases;
suppose
A145: i in dom(n.-->xb);
then i in {n};
then
A146: i = n by TARSKI:def 1;
f1.i = (n.-->xb).i by A144,A145,FUNCT_4:def 1;
hence xi is Element of R by A2,A146,FUNCOP_1:72;
end;
suppose
A147: not i in dom(n.-->xb);
then
A148: not i in {n};
then
A149: i in n by A143,XBOOLE_0:def 3;
A150: i in dom Carrier (p|ns) by A3,A143,A148,XBOOLE_0:def 3;
f1.i = xa.i by A144,A147,FUNCT_4:def 1;
then
A151: xi in (Carrier (p|ns)).i by A126,A150;
ex R2 being 1-sorted st ( R2 = (p|ns).i)&( (Carrier(p|ns)).
i =the carrier of R2) by A1,A149,PRALG_1:def 15;
hence xi is Element of R by A1,A149,A151,FUNCT_1:49;
end;
end;
then reconsider xi as Element of R;
A152: i in dom ya \/ dom (n.-->yb) by A131,A142,AFINSQ_1:2;
now per cases;
suppose
A153: i in dom(n.-->yb);
then i in {n};
then
A154: i = n by TARSKI:def 1;
g1.i = (n.-->yb).i by A152,A153,FUNCT_4:def 1;
hence yi is Element of R by A2,A154,FUNCOP_1:72;
end;
suppose
A155: not i in dom(n.-->yb);
then
A156: not i in {n};
then
A157: i in n by A143,XBOOLE_0:def 3;
A158: i in dom Carrier (p|ns) by A3,A143,A156,XBOOLE_0:def 3;
g1.i = ya.i by A152,A155,FUNCT_4:def 1;
then
A159: yi in (Carrier (p|ns)).i by A129,A158;
ex R2 being 1-sorted st ( R2 = (p|ns).i)&( (Carrier(p|ns)).
i=the carrier of R2) by A1,A157,PRALG_1:def 15;
hence yi is Element of R by A1,A157,A159,FUNCT_1:49;
end;
end;
then reconsider yi as Element of R;
take R,xi,yi;
thus R = p.i;
thus xi = f1.i;
thus yi = g1.i;
per cases by A143,XBOOLE_0:def 3;
suppose
A160: i in n;
A161: not i in {n}
proof
assume i in {n};
then n in n by A160,TARSKI:def 1;
hence contradiction;
end;
then
A162: not i in dom (n.-->xb);
not i in dom (n.-->yb) by A161;
then
A163: yi = ya.i by A152,FUNCT_4:def 1;
consider RR being RelStr, xxi, yyi being Element of RR such that
A164: RR = (p|ns).i and
A165: xxi = ffx.i and
A166: yyi = ggx.i and
A167: xxi <= yyi by A139,A160;
RR = R by A1,A160,A164,FUNCT_1:49;
hence thesis by A137,A138,A144,A162,A163,A165,A166,A167,
FUNCT_4:def 1;
end;
suppose
A168: i in {n};
then
A169: i = n by TARSKI:def 1;
A170: i in dom (n.-->xb) by A168;
A171: i in dom (n.-->yb) by A168;
A172: xi = (n.-->xb).i by A144,A170,FUNCT_4:def 1
.= xb by A169,FUNCOP_1:72;
yi = (n.-->yb).i by A152,A171,FUNCT_4:def 1
.= yb by A169,FUNCOP_1:72;
hence thesis by A2,A141,A168,A172,TARSKI:def 1;
end;
end;
hence f9.x <= f9.y by A121,YELLOW_1:def 4;
end;
assume f9.x <= f9.y;
then consider f1, g1 being Function such that
A173: f1 = f.x and
A174: g1 = f.y and
A175: for i be object st i in n+1 ex R being RelStr,
xi,yi being Element of R
st R = p.i & xi = f1.i & yi = g1.i & xi <= yi by A121,YELLOW_1:def 4;
now
set f2 = xa9, g2 = ya9;
reconsider f2, g2 as Function;
take f2, g2;
thus f2 = xa9 & g2 = ya9;
let i be object such that
A176: i in ns;
A177: not i in {n}
proof
assume i in {n};
then A: i = n by TARSKI:def 1; then
reconsider i as set;
not i in i;
hence contradiction by A,A1,A176;
end;
then
A178: not i in dom (n.-->yb);
A179: not i in dom (n.-->xb) by A177;
set R = (p|ns).i;
i in dom (p|ns) by A176,PARTFUN1:def 2;
then (p|ns).i in rng (p|ns) by FUNCT_1:def 3;
then reconsider R as RelStr by YELLOW_1:def 3;
take R;
set xi = xa.i, yi = ya.i;
A180: i in dom xa \/ dom (n.-->xb) by A1,A127,A176,XBOOLE_0:def 3;
A181: i in dom Carrier(p|ns) by A176,PARTFUN1:def 2;
ex R2 being 1-sorted st ( R2 = (p|ns).i)&( (Carrier(p|ns)).
i = the carrier of R2) by A176,PRALG_1:def 15;
then reconsider xi as Element of R by A126,A181;
A182: i in dom ya \/ dom (n.-->yb) by A1,A130,A176,XBOOLE_0:def 3;
ex R2 being 1-sorted st ( R2 = (p|ns).i)&( (Carrier(p|ns)).
i = the carrier of R2) by A176,PRALG_1:def 15;
then reconsider yi as Element of R by A129,A181;
take xi, yi;
thus R = (p|ns).i & xi = f2.i & yi = g2.i;
consider R2 being RelStr, xi2, yi2 being Element of R2 such that
A183: R2 = p.i and
A184: xi2 = f1.i and
A185: yi2 = g1.i and
A186: xi2 <= yi2 by A175,A176;
A187: R2 = R by A176,A183,FUNCT_1:49;
(xa +* (n.-->xb)).i = xi by A179,A180,FUNCT_4:def 1;
hence xi <= yi by A120,A124,A173,A174,A178,A182,A184,A185,A186,A187,
FUNCT_4:def 1;
end;
then xa9 <= ya9 by A125,YELLOW_1:def 4;
then
A188: [xa,ya] in the InternalRel of product(p|ns);
A189: [[x,y]`1`1, [x,y]`2`1] in the InternalRel of product(p|ns)
by A123,A119,A188;
consider Rn being RelStr, xni, yni being Element of Rn such that
A190: Rn = p.ne and
A191: xni = f1.n and
A192: yni = g1.n and
A193: xni <= yni by A2,A175;
A194: [xni, yni] in the InternalRel of p.ne by A190,A193;
A195: n in dom (n.-->xb) by TARSKI:def 1;
then n in dom xa \/ dom (n.-->xb) by XBOOLE_0:def 3;
then
A196: (xa +* (n.-->xb)).n = (n.-->xb).n by A195,FUNCT_4:def 1
.= xb by FUNCOP_1:72;
A197: n in dom (n.-->yb) by TARSKI:def 1;
then n in dom ya \/ dom (n.-->yb) by XBOOLE_0:def 3;
then
A198: (ya +* (n.-->yb)).n = (n.-->yb).n by A197,FUNCT_4:def 1
.= yb by FUNCOP_1:72;
A199: [[x,y]`1`2, [x,y]`2`2] in the InternalRel of p.ne
by A120,A123,A124,A173,A174,A191,A192,A194,A196,A198,A119;
A200: [x,y]`1 = [xa,xb] by A119;
[x,y]`2 = [ya,yb] by A123;
then [x,y] in ["the InternalRel of product (p|ns),
the InternalRel of p.ne"] by A189,A199,A200,YELLOW_3:10;
then [x,y] in the InternalRel of S by YELLOW_3:def 2;
hence x <= y;
end;
hence f is isomorphic by A74,A116,WAYBEL_0:66;
end;
hence thesis by WAYBEL_1:def 8;
end;
end;
theorem Th41: :: Corollary 4.47
for n being non zero Nat, p being RelStr-yielding ManySortedSet of Segm n
st for i being Element of Segm n holds p.i is Dickson & p.i is quasi_ordered
holds product p is quasi_ordered & product p is Dickson
proof
defpred P[non zero Nat] means
for p being RelStr-yielding ManySortedSet of Segm $1
st for i being Element of Segm $1
holds p.i is Dickson & p.i is quasi_ordered
holds product p is quasi_ordered & product p is Dickson;
A1: P[1]
proof
let p be RelStr-yielding ManySortedSet of Segm 1 such that
A2: for i being Element of Segm 1 holds p.i is Dickson & p.i is quasi_ordered;
reconsider z = 0 as Element of Segm 1 by CARD_1:49,TARSKI:def 1;
A3: p.z is Dickson by A2;
A4: p.z is quasi_ordered by A2;
Segm 1 = {0} by CARD_1:49;
then p.z,product p are_isomorphic by Th38;
hence thesis by A3,A4,Th37;
end;
A5: now
let n be non zero Nat;
assume
A6: P[n];
thus P[n+1]
proof
let p be RelStr-yielding ManySortedSet of Segm(n+1);
assume
A7: for i being Element of Segm(n+1)
holds p.i is Dickson & p.i is quasi_ordered;
n <= n+1 by NAT_1:11;
then reconsider ns = Segm n as Subset of Segm(n+1) by NAT_1:39;
A8: n+1 = {k where k is Nat : k < n+1} by AXIOMS:4;
n < n+1 by NAT_1:13;
then n in n+1 by A8;
then reconsider ne = n as Element of Segm(n+1);
reconsider pns = p|ns as RelStr-yielding ManySortedSet of Segm n;
A9: for i being Element of Segm n
holds pns.i is Dickson & pns.i is quasi_ordered
proof
let i be Element of Segm n;
A10: (pns.i) = p.i by FUNCT_1:49;
A11: n = {k where k is Nat : k < n} by AXIOMS:4;
i in n;
then consider k being Nat such that
A12: k = i and
A13: k < n by A11;
k < n+1 by A13,NAT_1:13;
then i in n+1 by A8,A12;
then reconsider i9=i as Element of n+1;
i9 = i;
hence thesis by A7,A10;
end;
then
A14: product(pns) is Dickson by A6;
A15: product(pns) is quasi_ordered by A6,A9;
A16: p.ne is Dickson by A7;
A17: p.ne is quasi_ordered by A7;
then
A18: [:product(p|ns), p.ne:] is Dickson by A14,A15,A16,Th36;
A19: [:product(p|ns), p.ne:] is quasi_ordered by A15,A17;
[:product(p|ns),p.ne:], product p are_isomorphic by Th40;
hence thesis by A18,A19,Th37;
end;
end;
thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A1,
A5);
end;
Lm1: for p being RelStr-yielding ManySortedSet of {}
holds product p is non empty &
product p is quasi_ordered & product p is Dickson & product p is antisymmetric
proof
let p be RelStr-yielding ManySortedSet of {};
A1: product p = RelStr (# {{}}, id {{}} #) by YELLOW_1:26;
set pp = product p, cpp = the carrier of pp, ipp = the InternalRel of pp;
A2: ipp = id {{}} by YELLOW_1:26;
thus pp is non empty by YELLOW_1:26;
thus pp is quasi_ordered
by YELLOW_1:26;
thus pp is Dickson
proof
let N be Subset of cpp;
per cases by A1,ZFMISC_1:33;
suppose
A3: N = {};
take B = {};
N = {} cpp by A3;
hence B is_Dickson-basis_of N,pp;
thus thesis;
end;
suppose
A4: N = {{}};
take B = {{}};
thus B is_Dickson-basis_of N,pp
proof
thus B c= N by A4;
let a be Element of pp;
assume
A5: a in N;
take b = a;
thus b in B by A4,A5;
[b,a] in id {{}} by A4,A5,RELAT_1:def 10;
hence thesis by A2;
end;
thus thesis;
end;
end;
thus thesis by YELLOW_1:26;
end;
registration
let p be RelStr-yielding ManySortedSet of {};
cluster product p -> non empty;
coherence by Lm1;
cluster product p -> antisymmetric;
coherence by Lm1;
cluster product p -> quasi_ordered;
coherence by Lm1;
::$N Dickson Lemma
cluster product p -> Dickson;
coherence by Lm1;
end;
definition
func NATOrd -> Relation of NAT equals
::: RelIncl omega;
{[x,y] where x, y is Element of NAT : x <= y};
correctness
proof
set NO = {[x,y] where x, y is Element of NAT : x <= y};
now
let z be object;
assume z in NO;
then ex x, y being Element of NAT st z = [x,y] & x <= y;
hence z in [:NAT, NAT:];
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th42:
NATOrd is_reflexive_in NAT;
theorem Th43:
NATOrd is_antisymmetric_in NAT
proof
let x, y be object such that x in NAT and y in NAT and
A1: [x,y] in NATOrd and
A2: [y,x] in NATOrd;
consider x9, y9 being Element of NAT such that
A3: [x,y] = [x9,y9] and
A4: x9 <= y9 by A1;
A5: x = x9 by A3,XTUPLE_0:1;
A6: y = y9 by A3,XTUPLE_0:1;
consider y2, x2 being Element of NAT such that
A7: [y,x] = [y2,x2] and
A8: y2 <= x2 by A2;
A9: y2 = y9 by A6,A7,XTUPLE_0:1;
x2 = x9 by A5,A7,XTUPLE_0:1;
hence thesis by A4,A5,A6,A8,A9,XXREAL_0:1;
end;
theorem Th44:
NATOrd is_strongly_connected_in NAT
proof
now
let x, y be object such that
A1: x in NAT and
A2: y in NAT;
thus [x,y] in NATOrd or [y,x] in NATOrd
proof
assume that
A3: not [x,y] in NATOrd and
A4: not [y,x] in NATOrd;
reconsider x,y as Element of NAT by A1,A2;
per cases;
suppose x <= y;
hence contradiction by A3;
end;
suppose y <= x;
hence contradiction by A4;
end;
end;
end;
hence thesis;
end;
theorem Th45:
NATOrd is_transitive_in NAT
proof
let x, y, z be object such that x in NAT and y in NAT
and z in NAT and
A1: [x,y] in NATOrd and
A2: [y,z] in NATOrd;
consider x1,y1 being Element of NAT such that
A3: [x,y] = [x1,y1] and
A4: x1 <= y1 by A1;
A5: x = x1 by A3,XTUPLE_0:1;
A6: y = y1 by A3,XTUPLE_0:1;
consider y2, z2 being Element of NAT such that
A7: [y,z] = [y2,z2] and
A8: y2 <= z2 by A2;
A9: y = y2 by A7,XTUPLE_0:1;
A10: z = z2 by A7,XTUPLE_0:1;
x1 <= z2 by A4,A6,A8,A9,XXREAL_0:2;
hence thesis by A5,A10;
end;
definition
func OrderedNAT -> non empty RelStr equals
RelStr(# NAT, NATOrd #);
coherence;
end;
Lm2: now
for x, y be Element of OrderedNAT st not x <= y holds y <= x by Th44;
hence OrderedNAT is connected by WAYBEL_0:def 29;
end;
registration
cluster OrderedNAT -> connected;
coherence by Lm2;
cluster OrderedNAT -> Dickson;
coherence
proof
set IR9 = the InternalRel of OrderedNAT\~,CR9 =the carrier of OrderedNAT\~;
now
let N be set such that
A1: N c= CR9 and
A2: N <> {};
A3: ex k being object st k in N by A2,XBOOLE_0:def 1;
defpred P[Nat] means $1 in N;
A4: ex k being Nat st P[k] by A1,A3;
consider m being Nat such that
A5: P[m] and
A6: for n being Nat st P[n] holds m <= n from NAT_1:sch 5(A4);
reconsider m as Element of OrderedNAT by ORDINAL1:def 12;
thus ex m being object st m in N & IR9-Seg(m) misses N
proof
take m;
thus m in N by A5;
now
assume IR9-Seg(m) /\ N <> {};
then consider z being object such that
A7: z in IR9-Seg(m) /\ N by XBOOLE_0:def 1;
A8: z in IR9-Seg(m) by A7,XBOOLE_0:def 4;
A9: z in N by A7,XBOOLE_0:def 4;
A10: z <> m by A8,WELLORD1:1;
A11: [z,m] in IR9 by A8,WELLORD1:1;
then [z,m] in NATOrd;
then consider x,y being Element of NAT such that
A12: [z,m] = [x,y] and x <= y;
A13: z = x by A12,XTUPLE_0:1;
A14: m = y by A12,XTUPLE_0:1;
then y <= x by A6,A9,A13;
then [y,x] in NATOrd;
hence contradiction by A10,A11,A13,A14,Th43;
end;
hence thesis by XBOOLE_0:def 7;
end;
end;
then IR9 is_well_founded_in CR9 by WELLORD1:def 3;
then OrderedNAT\~ is well_founded by WELLFND1:def 2;
hence thesis by Th26;
end;
cluster OrderedNAT -> quasi_ordered;
coherence
proof
A15: OrderedNAT is reflexive by Th42;
OrderedNAT is transitive by Th45;
hence thesis by A15;
end;
cluster OrderedNAT -> antisymmetric;
coherence by Th43;
cluster OrderedNAT -> transitive;
coherence by Th45;
cluster OrderedNAT -> well_founded;
coherence
proof
set ir = the InternalRel of OrderedNAT;
now
given f being sequence of OrderedNAT such that
A16: f is descending;
A17: dom f = NAT by FUNCT_2:def 1;
reconsider rf = rng f as non empty Subset of NAT;
set m = min rf;
m in rng f by XXREAL_2:def 7;
then consider d being object such that
A18: d in dom f and
A19: m = f.d by FUNCT_1:def 3;
reconsider d as Element of NAT by A18;
A20: f.(d+1) <> f.d by A16,WELLFND1:def 6;
[f.(d+1),f.d] in ir by A16,WELLFND1:def 6;
then consider x, y being Element of NAT such that
A21: [f.(d+1),f.d] = [x,y] and
A22: x <= y;
reconsider fd1 = f.(d+1), fd = f.d as Element of NAT;
A23: f.(d+1) = x by A21,XTUPLE_0:1;
f.d = y by A21,XTUPLE_0:1;
then
A24: fd1 < fd by A20,A22,A23,XXREAL_0:1;
f.(d+1) in rf by A17,FUNCT_1:3;
hence contradiction by A19,A24,XXREAL_2:def 7;
end;
hence thesis by WELLFND1:14;
end;
end;
Lm3: now
let n be Element of NAT;
set pp = product (n --> OrderedNAT);
per cases;
suppose n is zero;
then n = 0;
hence pp is non empty & pp is Dickson & pp is quasi_ordered &
pp is antisymmetric;
end;
suppose n is non zero;
then reconsider n9 = n as non zero Element of NAT;
reconsider p = (n9 --> OrderedNAT) as
RelStr-yielding ManySortedSet of Segm n9;
thus product (n --> OrderedNAT) is non empty;
for i being Element of Segm n9
holds p.i is Dickson & p.i is quasi_ordered;
hence product (n --> OrderedNAT) is Dickson &
product (n --> OrderedNAT) is quasi_ordered by Th41;
product p is antisymmetric;
hence product (n --> OrderedNAT) is antisymmetric;
end;
end;
registration :: 4.48 Dickson's Lemma
let n be Element of NAT;
cluster product (n --> OrderedNAT) -> non empty;
coherence;
cluster product (n --> OrderedNAT) -> Dickson;
coherence by Lm3;
cluster product (n --> OrderedNAT) -> quasi_ordered;
coherence by Lm3;
cluster product (n --> OrderedNAT) -> antisymmetric;
coherence by Lm3;
end;
theorem :: Proposition 4.49, in B&W proven without axiom of choice (4.46)
for M be RelStr st M is Dickson & M is quasi_ordered
holds [:M,OrderedNAT:] is quasi_ordered & [:M,OrderedNAT:] is Dickson
by Th36;
:: Omitting Exercise 4.50
theorem Th47: :: Lemma 4.51
for R, S being non empty RelStr st R is Dickson & S is quasi_ordered &
the InternalRel of R c= the InternalRel of S &
(the carrier of R) = (the carrier of S) holds S\~ is well_founded
proof
let R, S be non empty RelStr such that
A1: R is Dickson and
A2: S is quasi_ordered and
A3: the InternalRel of R c= the InternalRel of S and
A4: the carrier of R = the carrier of S;
S is Dickson by A1,A3,A4,Th27;
hence thesis by A2,Th32;
end;
theorem :: Lemma 4.52
for R being non empty RelStr st R is quasi_ordered holds R is Dickson iff
for S being non empty RelStr
st S is quasi_ordered & the InternalRel of R c= the InternalRel of S &
the carrier of R = the carrier of S holds S\~ is well_founded
proof
let R be non empty RelStr such that
A1: R is quasi_ordered;
A2: R is reflexive by A1;
A3: R is transitive by A1;
set IR = the InternalRel of R, CR = the carrier of R;
thus R is Dickson implies for S being non empty RelStr st
S is quasi_ordered & IR c= the InternalRel of S & CR = the carrier of S
holds S\~ is well_founded by Th47;
assume
A4: for S being non empty RelStr st S is quasi_ordered &
IR c= the InternalRel of S & CR = the carrier of S
holds S\~ is well_founded;
now
assume not R is Dickson;
then not (for N being non empty Subset of R
holds min-classes N is finite & min-classes N is non empty) by A1,Th31;
then consider f being sequence of R such that
A5: for i,j being Nat st i < j holds not f.i <= f.j by A1,Th30;
defpred P[object,object] means
[$1,$2] in IR or ex i,j being Element of NAT st i < j &
[$1, f.j] in IR & [f.i, $2] in IR;
consider QOE being Relation of CR,CR such that
A6: for x,y being object holds [x,y] in QOE iff x in CR & y in CR & P[x,y]
from RELSET_1:sch 1;
set S = RelStr(# CR, QOE #);
now
let x,y be object such that
A7: [x,y] in IR;
A8: x in dom IR by A7,XTUPLE_0:def 12;
y in rng IR by A7,XTUPLE_0:def 13;
hence [x,y] in QOE by A6,A7,A8;
end;
then
A9: IR c= the InternalRel of S by RELAT_1:def 3;
A10: IR is_reflexive_in CR by A2;
then for x being object st x in CR holds [x,x] in QOE by A6;
then QOE is_reflexive_in CR;
then
A11: S is reflexive;
A12: IR is_transitive_in CR by A3;
now
let x,y,z be object such that
A13: x in CR and
A14: y in CR and
A15: z in CR and
A16: [x,y] in QOE and
A17: [y,z] in QOE;
now per cases by A6,A16;
suppose
A18: [x,y] in IR;
now per cases by A6,A17;
suppose [y,z] in IR;
then [x,z] in IR by A12,A13,A14,A15,A18;
hence [x,z] in QOE by A6,A13,A15;
end;
suppose ex i,j being Element of NAT
st i<j & [y,f.j] in IR & [f.i, z] in IR;
then consider i,j being Element of NAT such that
A19: i < j and
A20: [y,f.j] in IR and
A21: [f.i, z] in IR;
[x,f.j] in IR by A12,A13,A14,A18,A20;
hence [x,z] in QOE by A6,A13,A15,A19,A21;
end;
end;
hence [x,z] in QOE;
end;
suppose ex i,j being Element of NAT
st i < j & [x, f.j] in IR & [f.i, y] in IR;
then consider i, j being Element of NAT such that
A22: i < j and
A23: [x, f.j] in IR and
A24: [f.i, y] in IR;
now per cases by A6,A17;
suppose [y,z] in IR;
then [f.i, z] in IR by A12,A14,A15,A24;
hence [x,z] in QOE by A6,A13,A15,A22,A23;
end;
suppose ex a,b being Element of NAT
st a<b & [y,f.b] in IR & [f.a,z] in IR;
then consider a,b being Element of NAT such that
A25: a < b and
A26: [y,f.b] in IR and
A27: [f.a, z] in IR;
[f.i, f.b] in IR by A12,A14,A24,A26;
then f.i <= f.b;
then not i < b by A5;
then a <= i by A25,XXREAL_0:2;
then a < j by A22,XXREAL_0:2;
hence [x,z] in QOE by A6,A13,A15,A23,A27;
end;
end;
hence [x,z] in QOE;
end;
end;
hence [x,z] in QOE;
end;
then QOE is_transitive_in CR;
then S is transitive;
then S is quasi_ordered by A11;
then
A28: S\~ is well_founded by A4,A9;
reconsider f9=f as sequence of S\~;
now
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A29: n < n+1 by NAT_1:13;
then not f.n1 <= f.(n1+1) by A5;
then
A30: not [f.n, f.(n+1)] in IR;
hence f9.(n+1) <> f9.n by A10;
A31: [f9.(n+1), f9.(n+1)] in IR by A10;
A32: [f9.n, f9.n] in IR by A10;
A33: now
assume [f9.n, f9.(n+1)] in QOE;
then ex i,j being Element of NAT st i < j &
[f9.n, f.j] in IR & [f.i, f9.(n+1)] in IR by A6,A30;
then consider l,k being Element of NAT such that
A34: k < l and
A35: [f9.n, f.l] in IR and
A36: [f.k, f9.(n+1)] in IR;
A37: f.n <= f.l by A35;
A38: f.k <= f.(n+1) by A36;
A39: l <= n1 by A5,A37;
A40: n+1 <= k by A5,A38;
l < n+1 by A39,NAT_1:13;
hence contradiction by A34,A40,XXREAL_0:2;
end;
A41: [f9.(n1+1),f9.n1] in QOE by A6,A29,A31,A32;
not [f9.(n+1),f9.n] in QOE~ by A33,RELAT_1:def 7;
hence [f9.(n+1), f9.n] in the InternalRel of S\~ by A41,XBOOLE_0:def 5;
end;
then f9 is descending by WELLFND1:def 6;
hence contradiction by A28,WELLFND1:14;
end;
hence thesis;
end;
theorem
NATOrd = RelIncl omega
proof
set f = NATOrd, g = RelIncl omega;
for a,b being object holds [a,b] in f iff [a,b] in g
proof
let a,b be object;
hereby assume [a,b] in f; then
consider x,y being Element of NAT such that
A1: [a,b] = [x,y] & x <= y;
x = Segm x & y = Segm y; then
x c= y by A1,NAT_1:39;
hence [a,b] in g by A1,WELLORD2:def 1;
end;
assume
A2: [a,b] in g; then
reconsider aa = a, bb = b as Element of NAT by ZFMISC_1:87;
A4: aa c= bb by A2,WELLORD2:def 1;
aa = Segm aa & bb = Segm bb; then
aa <= bb by A4,NAT_1:39;
hence thesis;
end;
hence thesis by RELAT_1:def 2;
end;