defpred S1[ object , object ] means ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = $1 & p . (len p) = $2 & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) );
set P = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } ;
{ [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } c= [: the carrier of R, the carrier of R:]
proof
let z be
object ;
TARSKI:def 3 ( not z in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } or z in [: the carrier of R, the carrier of R:] )
assume
z in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) }
;
z in [: the carrier of R, the carrier of R:]
then
ex
x,
y being
Element of
R st
(
z = [x,y] &
x in the
carrier of
R &
y in the
carrier of
R &
S1[
x,
y] )
;
hence
z in [: the carrier of R, the carrier of R:]
by ZFMISC_1:87;
verum
end;
then reconsider P1 = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } as Relation of the carrier of R ;
A1:
for x, y being object holds
( [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } iff ( x in the carrier of R & y in the carrier of R & S1[x,y] ) )
proof
let x,
y be
object ;
( [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } iff ( x in the carrier of R & y in the carrier of R & S1[x,y] ) )
hereby ( x in the carrier of R & y in the carrier of R & S1[x,y] implies [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } )
assume
[x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) }
;
( x in the carrier of R & y in the carrier of R & S1[x,y] )then consider x1,
y1 being
Element of
R such that A2:
[x,y] = [x1,y1]
and
x1 in the
carrier of
R
and
y1 in the
carrier of
R
and A3:
S1[
x1,
y1]
;
(
x = x1 &
y = y1 )
by A2, XTUPLE_0:1;
hence
(
x in the
carrier of
R &
y in the
carrier of
R &
S1[
x,
y] )
by A3;
verum
end;
thus
(
x in the
carrier of
R &
y in the
carrier of
R &
S1[
x,
y] implies
[x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } )
;
verum
end;
now for x, y being object st x in the carrier of R & y in the carrier of R & [x,y] in P1 holds
[y,x] in P1let x,
y be
object ;
( x in the carrier of R & y in the carrier of R & [x,y] in P1 implies [y,x] in P1 )assume that A4:
(
x in the
carrier of
R &
y in the
carrier of
R )
and A5:
[x,y] in P1
;
[y,x] in P1consider p being
FinSequence of the
carrier of
R such that A6:
1
< len p
and A7:
(
p . 1
= x &
p . (len p) = y )
and A8:
for
n being
Nat st 2
<= n &
n <= len p & not
[(p . n),(p . (n - 1))] in the
InternalRel of
R holds
[(p . (n - 1)),(p . n)] in the
InternalRel of
R
by A1, A5;
S1[
y,
x]
proof
take F =
Rev p;
( 1 < len F & F . 1 = y & F . (len F) = x & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
thus
1
< len F
by A6, FINSEQ_5:def 3;
( F . 1 = y & F . (len F) = x & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
A9:
len F = len p
by FINSEQ_5:def 3;
hence
(
F . 1
= y &
F . (len F) = x )
by A7, FINSEQ_5:62;
for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R
let n1 be
Nat;
( 2 <= n1 & n1 <= len F & not [(F . n1),(F . (n1 - 1))] in the InternalRel of R implies [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
assume that A10:
2
<= n1
and A11:
n1 <= len F
;
( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
1
<= n1
by A10, XXREAL_0:2;
then A12:
n1 in dom p
by A9, A11, FINSEQ_3:25;
set n2 =
((len p) - n1) + 2;
0 <= (len p) - n1
by A9, A11, XREAL_1:48;
then A13:
2
+ 0 <= ((len p) - n1) + 2
by XREAL_1:6;
A14:
2
- 1
<= n1 - 1
by A10, XREAL_1:9;
then reconsider n11 =
n1 - 1 as
Element of
NAT by INT_1:3, XXREAL_0:2;
n1 - 1
<= (len F) - 0
by A11, XREAL_1:13;
then
n11 in dom p
by A9, A14, FINSEQ_3:25;
then A15:
F . (n1 - 1) =
p . (((len p) - (n1 - 1)) + 1)
by FINSEQ_5:58
.=
p . (((len p) - n1) + 2)
;
reconsider n2 =
((len p) - n1) + 2 as
Element of
NAT by A13, INT_1:3, XXREAL_0:2;
(len p) - n1 <= (len p) - 2
by A10, XREAL_1:13;
then A16:
((len p) - n1) + 2
<= ((len p) - 2) + 2
by XREAL_1:6;
p . (n2 - 1) =
p . (((len p) - n1) + (2 - 1))
.=
F . n1
by A12, FINSEQ_5:58
;
hence
(
[(F . n1),(F . (n1 - 1))] in the
InternalRel of
R or
[(F . (n1 - 1)),(F . n1)] in the
InternalRel of
R )
by A8, A15, A13, A16;
verum
end; hence
[y,x] in P1
by A4;
verum end;
then A17:
P1 is_symmetric_in the carrier of R
by RELAT_2:def 3;
A18:
the InternalRel of R is_reflexive_in the carrier of R
by ORDERS_2:def 2;
now for x being object st x in the carrier of R holds
[x,x] in P1let x be
object ;
( x in the carrier of R implies [x,x] in P1 )assume A19:
x in the
carrier of
R
;
[x,x] in P1
S1[
x,
x]
proof
set F =
<*x,x*>;
rng <*x,x*> =
{x,x}
by FINSEQ_2:127
.=
{x}
by ENUMSET1:29
;
then
rng <*x,x*> c= the
carrier of
R
by A19, ZFMISC_1:31;
then reconsider F1 =
<*x,x*> as
FinSequence of the
carrier of
R by FINSEQ_1:def 4;
take
F1
;
( 1 < len F1 & F1 . 1 = x & F1 . (len F1) = x & ( for n being Nat st 2 <= n & n <= len F1 & not [(F1 . n),(F1 . (n - 1))] in the InternalRel of R holds
[(F1 . (n - 1)),(F1 . n)] in the InternalRel of R ) )
A20:
len <*x,x*> = 2
by FINSEQ_1:44;
hence
1
< len F1
;
( F1 . 1 = x & F1 . (len F1) = x & ( for n being Nat st 2 <= n & n <= len F1 & not [(F1 . n),(F1 . (n - 1))] in the InternalRel of R holds
[(F1 . (n - 1)),(F1 . n)] in the InternalRel of R ) )
thus
(
F1 . 1
= x &
F1 . (len F1) = x )
by A20, FINSEQ_1:44;
for n being Nat st 2 <= n & n <= len F1 & not [(F1 . n),(F1 . (n - 1))] in the InternalRel of R holds
[(F1 . (n - 1)),(F1 . n)] in the InternalRel of R
let n1 be
Nat;
( 2 <= n1 & n1 <= len F1 & not [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R implies [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R )
assume
( 2
<= n1 &
n1 <= len F1 )
;
( [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R or [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R )
then A21:
n1 = 2
by A20, XXREAL_0:1;
(
<*x,x*> . 1
= x &
<*x,x*> . 2
= x )
by FINSEQ_1:44;
hence
(
[(F1 . n1),(F1 . (n1 - 1))] in the
InternalRel of
R or
[(F1 . (n1 - 1)),(F1 . n1)] in the
InternalRel of
R )
by A18, A19, A21, RELAT_2:def 1;
verum
end; hence
[x,x] in P1
by A19;
verum end;
then
P1 is_reflexive_in the carrier of R
by RELAT_2:def 1;
then A22:
( dom P1 = the carrier of R & field P1 = the carrier of R )
by ORDERS_1:13;
now for x, y, z being object st x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in P1 & [y,z] in P1 holds
[x,z] in P1let x,
y,
z be
object ;
( x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in P1 & [y,z] in P1 implies [x,z] in P1 )assume that A23:
x in the
carrier of
R
and A24:
y in the
carrier of
R
and A25:
z in the
carrier of
R
and A26:
(
[x,y] in P1 &
[y,z] in P1 )
;
[x,z] in P1
(
S1[
x,
y] &
S1[
y,
z] )
by A1, A26;
then consider p1,
p2 being
FinSequence of the
carrier of
R such that A27:
1
< len p1
and A28:
p1 . 1
= x
and A29:
p1 . (len p1) = y
and A30:
for
n being
Nat st 2
<= n &
n <= len p1 & not
[(p1 . n),(p1 . (n - 1))] in the
InternalRel of
R holds
[(p1 . (n - 1)),(p1 . n)] in the
InternalRel of
R
and A31:
1
< len p2
and A32:
p2 . 1
= y
and A33:
p2 . (len p2) = z
and A34:
for
n being
Nat st 2
<= n &
n <= len p2 & not
[(p2 . n),(p2 . (n - 1))] in the
InternalRel of
R holds
[(p2 . (n - 1)),(p2 . n)] in the
InternalRel of
R
;
S1[
x,
z]
proof
take F =
p1 ^ p2;
( 1 < len F & F . 1 = x & F . (len F) = z & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
A35:
len F = (len p1) + (len p2)
by FINSEQ_1:22;
1
+ 1
< (len p1) + (len p2)
by A27, A31, XREAL_1:8;
hence
1
< len F
by A35, XXREAL_0:2;
( F . 1 = x & F . (len F) = z & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
1
in dom p1
by A27, FINSEQ_3:25;
hence
F . 1
= x
by A28, FINSEQ_1:def 7;
( F . (len F) = z & ( for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R ) )
len p2 in dom p2
by A31, FINSEQ_3:25;
hence
F . (len F) = z
by A33, A35, FINSEQ_1:def 7;
for n being Nat st 2 <= n & n <= len F & not [(F . n),(F . (n - 1))] in the InternalRel of R holds
[(F . (n - 1)),(F . n)] in the InternalRel of R
let n1 be
Nat;
( 2 <= n1 & n1 <= len F & not [(F . n1),(F . (n1 - 1))] in the InternalRel of R implies [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
assume that A36:
2
<= n1
and A37:
n1 <= len F
;
( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
A38:
1
<= n1
by A36, XXREAL_0:2;
A39:
2
- 1
<= n1 - 1
by A36, XREAL_1:9;
then reconsider n11 =
n1 - 1 as
Element of
NAT by INT_1:3, XXREAL_0:2;
A40:
( not
(len p1) + 1
<= n1 or
(len p1) + 1
= n1 or
(len p1) + 1
< n1 )
by XXREAL_0:1;
A41:
n1 - 1
<= (len F) - 0
by A37, XREAL_1:13;
per cases
( n1 <= len p1 or (len p1) + 1 < n1 or (len p1) + 1 = n1 )
by A40, INT_1:7;
suppose A44:
(len p1) + 1
< n1
;
( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
len p1 < (len p1) + 1
by XREAL_1:29;
then A45:
len p1 < n1
by A44, XXREAL_0:2;
then reconsider k =
n1 - (len p1) as
Element of
NAT by INT_1:3, XREAL_1:48;
((len p1) + 1) - 1
< n1 - 1
by A44, XREAL_1:9;
then
F . n11 = p2 . (n11 - (len p1))
by A41, FINSEQ_1:24;
then A46:
F . (n1 - 1) = p2 . (k - 1)
;
1
< n1 - (len p1)
by A44, XREAL_1:20;
then A47:
1
+ 1
<= n1 - (len p1)
by INT_1:7;
n1 <= (len p1) + (len p2)
by A37, FINSEQ_1:22;
then A48:
k <= len p2
by XREAL_1:20;
F . n1 = p2 . k
by A37, A45, FINSEQ_1:24;
hence
(
[(F . n1),(F . (n1 - 1))] in the
InternalRel of
R or
[(F . (n1 - 1)),(F . n1)] in the
InternalRel of
R )
by A34, A46, A47, A48;
verum end; suppose A49:
(len p1) + 1
= n1
;
( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R )
(
(len p1) + 1
<= (len p1) + (len p2) &
((len p1) + 1) - (len p1) = 1 )
by A31, XREAL_1:8;
then A50:
F . n1 = y
by A32, A49, FINSEQ_1:23;
len p1 in dom p1
by A27, FINSEQ_3:25;
then
F . (n1 - 1) = y
by A29, A49, FINSEQ_1:def 7;
hence
(
[(F . n1),(F . (n1 - 1))] in the
InternalRel of
R or
[(F . (n1 - 1)),(F . n1)] in the
InternalRel of
R )
by A18, A24, A50, RELAT_2:def 1;
verum
end; hence
[x,z] in P1
by A23, A25;
verum end;
then
P1 is_transitive_in the carrier of R
by RELAT_2:def 8;
then reconsider P1 = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S1[x,y] ) } as Equivalence_Relation of the carrier of R by A22, A17, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
take
P1
; for x, y being object holds
( [x,y] in P1 iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) )
thus
for x, y being object holds
( [x,y] in P1 iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) )
by A1; verum