let R be non empty connected Poset; :: thesis: union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R)
set IR = the InternalRel of R;
set CR = the carrier of R;
set X = union (rng (FinOrd-Approx R));
set FOAR = FinOrd-Approx R;
set FOAR0 = { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) } ;
A1:
(FinOrd-Approx R) . 0 = { [a,b] where a, b is Element of Fin the carrier of R : ( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) ) }
by Def16;
then
union (rng (FinOrd-Approx R)) c= [:(Fin the carrier of R),(Fin the carrier of R):]
by TARSKI:def 3;
then reconsider X = union (rng (FinOrd-Approx R)) as Relation of (Fin the carrier of R) ;
A4:
now hence
X is_reflexive_in Fin the
carrier of
R
by RELAT_2:def 1;
:: thesis: ( X is_antisymmetric_in Fin the carrier of R & X is_transitive_in Fin the carrier of R )now let x,
y be
set ;
:: thesis: ( x in Fin the carrier of R & y in Fin the carrier of R & [x,y] in X & [y,x] in X implies x = y )assume A17:
(
x in Fin the
carrier of
R &
y in Fin the
carrier of
R &
[x,y] in X &
[y,x] in X )
;
:: thesis: x = yreconsider x' =
x as
Element of
Fin the
carrier of
R by A17;
A18:
(
x c= the
carrier of
R &
x is
finite )
by A17, FINSUB_1:def 5;
defpred S1[
Element of
NAT ]
means for
x,
y being
Element of
Fin the
carrier of
R st
card x = $1 &
[x,y] in X &
[y,x] in X holds
x = y;
then A20:
S1[
0 ]
;
now let n be
Element of
NAT ;
:: thesis: ( ( for a, b being Element of Fin the carrier of R st card a = n & [a,b] in X & [b,a] in X holds
a = b ) implies for a, b being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,a] in X holds
b4 = b5 )assume A21:
for
a,
b being
Element of
Fin the
carrier of
R st
card a = n &
[a,b] in X &
[b,a] in X holds
a = b
;
:: thesis: for a, b being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,a] in X holds
b4 = b5let a,
b be
Element of
Fin the
carrier of
R;
:: thesis: ( card a = n + 1 & [a,b] in X & [b,a] in X implies b2 = b3 )assume A22:
(
card a = n + 1 &
[a,b] in X &
[b,a] in X )
;
:: thesis: b2 = b3 end; then A30:
for
n being
Element of
NAT st
S1[
n] holds
S1[
n + 1]
;
A31:
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A20, A30);
consider n being
Nat such that A32:
x,
n are_equipotent
by A18, CARD_1:74;
card x' = n
by A32, CARD_1:def 5;
hence
x = y
by A17, A31;
:: thesis: verum end; hence
X is_antisymmetric_in Fin the
carrier of
R
by RELAT_2:def 4;
:: thesis: X is_transitive_in Fin the carrier of Rnow let x,
y,
z be
set ;
:: thesis: ( x in Fin the carrier of R & y in Fin the carrier of R & z in Fin the carrier of R & [x,y] in X & [y,z] in X implies [x,z] in X )assume A34:
(
x in Fin the
carrier of
R &
y in Fin the
carrier of
R &
z in Fin the
carrier of
R &
[x,y] in X &
[y,z] in X )
;
:: thesis: [x,z] in Xdefpred S1[
Element of
NAT ]
means for
a,
b,
c being
Element of
Fin the
carrier of
R st
card a = $1 &
[a,b] in X &
[b,c] in X holds
[a,c] in X;
then A36:
S1[
0 ]
;
now let n be
Element of
NAT ;
:: thesis: ( ( for a, b, c being Element of Fin the carrier of R st card a = n & [a,b] in X & [b,c] in X holds
[a,c] in X ) implies for a, b, c being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,c] in X holds
[b5,b7] in X )assume A37:
for
a,
b,
c being
Element of
Fin the
carrier of
R st
card a = n &
[a,b] in X &
[b,c] in X holds
[a,c] in X
;
:: thesis: for a, b, c being Element of Fin the carrier of R st card a = n + 1 & [a,b] in X & [b,c] in X holds
[b5,b7] in Xlet a,
b,
c be
Element of
Fin the
carrier of
R;
:: thesis: ( card a = n + 1 & [a,b] in X & [b,c] in X implies [b2,b4] in X )assume A38:
(
card a = n + 1 &
[a,b] in X &
[b,c] in X )
;
:: thesis: [b2,b4] in Xper cases
( a = {} or ( a <> {} & b <> {} & PosetMax a <> PosetMax b & [(PosetMax a),(PosetMax b)] in the InternalRel of R ) or ( a <> {} & b <> {} & PosetMax a = PosetMax b & [(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in union (rng (FinOrd-Approx R)) ) )
by A38, Th36;
suppose A42:
(
a <> {} &
b <> {} &
PosetMax a = PosetMax b &
[(a \ {(PosetMax a)}),(b \ {(PosetMax b)})] in union (rng (FinOrd-Approx R)) )
;
:: thesis: [b2,b4] in Xnow per cases
( b = {} or ( b <> {} & c <> {} & PosetMax b <> PosetMax c & [(PosetMax b),(PosetMax c)] in the InternalRel of R ) or ( b <> {} & c <> {} & PosetMax b = PosetMax c & [(b \ {(PosetMax b)}),(c \ {(PosetMax c)})] in union (rng (FinOrd-Approx R)) ) )
by A38, Th36;
suppose A43:
(
b <> {} &
c <> {} &
PosetMax b = PosetMax c &
[(b \ {(PosetMax b)}),(c \ {(PosetMax c)})] in union (rng (FinOrd-Approx R)) )
;
:: thesis: [a,c] in Xset z =
a \ {(PosetMax a)};
reconsider z =
a \ {(PosetMax a)} as
Element of
Fin the
carrier of
R by Th38;
A44:
card z = n
by A38, Lm1;
A45:
(
c c= the
carrier of
R &
c is
finite )
by FINSUB_1:def 5;
reconsider c' =
c as
finite set ;
set zc =
c' \ {(PosetMax c)};
c' \ {(PosetMax c)} c= the
carrier of
R
by A45, XBOOLE_1:1;
then reconsider zc =
c' \ {(PosetMax c)} as
Element of
Fin the
carrier of
R by FINSUB_1:def 5;
A46:
(
b c= the
carrier of
R &
b is
finite )
by FINSUB_1:def 5;
reconsider b' =
b as
finite set ;
set zb =
b' \ {(PosetMax b)};
b' \ {(PosetMax b)} c= the
carrier of
R
by A46, XBOOLE_1:1;
then reconsider zb =
b' \ {(PosetMax b)} as
Element of
Fin the
carrier of
R by FINSUB_1:def 5;
[z,zb] in union (rng (FinOrd-Approx R))
by A42;
then
[z,zc] in union (rng (FinOrd-Approx R))
by A37, A43, A44;
hence
[a,c] in X
by A42, A43, Th36;
:: thesis: verum end; hence
[a,c] in X
;
:: thesis: verum end; then A47:
for
n being
Element of
NAT st
S1[
n] holds
S1[
n + 1]
;
A48:
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A36, A47);
reconsider x' =
x as
Element of
Fin the
carrier of
R by A34;
(
x c= the
carrier of
R &
x is
finite )
by A34, FINSUB_1:def 5;
then consider n being
Nat such that A49:
x,
n are_equipotent
by CARD_1:74;
card x' = n
by A49, CARD_1:def 5;
hence
[x,z] in X
by A34, A48;
:: thesis: verum end; hence
X is_transitive_in Fin the
carrier of
R
by RELAT_2:def 8;
:: thesis: verum end;
then reconsider R = union (rng (FinOrd-Approx R)) as Relation of (Fin the carrier of R) ;
( dom R = Fin the carrier of R & field R = Fin the carrier of R )
by A4, ORDERS_1:98;
hence
union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R)
by A4, PARTFUN1:def 4, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16; :: thesis: verum