let x, y be set ; for O being non empty connected Poset
for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
let O be non empty connected Poset; for R being array of O st [x,y] in inversions R holds
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
let R be array of O; ( [x,y] in inversions R implies ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R )
assume A1:
[x,y] in inversions R
; ((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
then A2:
( x in dom R & y in dom R & x in y & R /. x > R /. y )
by Th46;
reconsider T = R as non empty array of O by A1;
reconsider p = x, q = y as Element of dom T by A1, Th46;
set j = (R,x,y) incl ;
set k = (T,p,q) incl ;
set s = Swap (R,x,y);
set t = Swap (T,p,q);
set ws = inversions (Swap (R,x,y));
set w = inversions R;
A3:
dom (Swap (T,p,q)) = dom T
by FUNCT_7:99;
thus
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= inversions R
XBOOLE_0:def 8 not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions Rproof
let z,
t be
object ;
RELAT_1:def 3 ( not [z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) or [z,t] in inversions R )
assume
[z,t] in ((R,x,y) incl) .: (inversions (Swap (R,x,y)))
;
[z,t] in inversions R
then consider a,
b being
object such that A4:
(
[a,b] in inversions (Swap (R,x,y)) &
[a,b] in dom ((R,x,y) incl) &
[z,t] = ((R,x,y) incl) . (
a,
b) )
by Th5;
reconsider a =
a,
b =
b as
set by TARSKI:1;
(
[a,b] in inversions (Swap (R,x,y)) implies (
a in dom (Swap (R,x,y)) &
b in dom (Swap (R,x,y)) &
a in b ) )
by Th46;
then A5:
(
a in b &
a in dom T &
b in dom T )
by A4, A3;
then reconsider a =
a,
b =
b as
Element of
dom T ;
per cases
( ( a <> p & a <> q & b <> p & b <> q ) or ( a in p & b = p ) or ( a in p & b = q ) or ( a = p & b in q ) or ( a = p & b = q ) or ( a = p & q in b ) or ( a = q & q in b ) or ( p in a & q = b ) )
by A2, A5, Th2;
end;
end;
now ( [x,y] in ((R,x,y) incl) .: (inversions (Swap (R,x,y))) implies [x,y] in inversions (Swap (R,x,y)) )assume
[x,y] in ((R,x,y) incl) .: (inversions (Swap (R,x,y)))
;
[x,y] in inversions (Swap (R,x,y))then consider a,
b being
object such that A13:
(
[a,b] in inversions (Swap (R,x,y)) &
[a,b] in dom ((R,x,y) incl) &
[x,y] = ((R,x,y) incl) . (
a,
b) )
by Th5;
A14:
((R,x,y) incl) . (
p,
q)
= [p,q]
by A2, Th66;
reconsider a =
a,
b =
b as
set by TARSKI:1;
(
[a,b] in inversions (Swap (R,x,y)) implies (
a in dom (Swap (R,x,y)) &
b in dom (Swap (R,x,y)) &
a in b ) )
by Th46;
then A15:
(
a in b &
a in dom T &
b in dom T )
by A13, A3;
then reconsider a =
a,
b =
b as
Element of
dom T ;
(
a = p &
b = q )
by A2, A13, A14, A15, Lm1;
hence
[x,y] in inversions (Swap (R,x,y))
by A13;
verum end;
hence
not ((R,x,y) incl) .: (inversions (Swap (R,x,y))) = inversions R
by A1, Th51; verum