let x, y be set ; for O being non empty connected Poset
for R being array of O st [x,y] in inversions R & inversions R is finite holds
card (inversions (Swap (R,x,y))) in card (inversions R)
let O be non empty connected Poset; for R being array of O st [x,y] in inversions R & inversions R is finite holds
card (inversions (Swap (R,x,y))) in card (inversions R)
let R be array of O; ( [x,y] in inversions R & inversions R is finite implies card (inversions (Swap (R,x,y))) in card (inversions R) )
set s = Swap (R,x,y);
set h = (R,x,y) incl ;
set ws = inversions (Swap (R,x,y));
assume A1:
( [x,y] in inversions R & inversions R is finite )
; card (inversions (Swap (R,x,y))) in card (inversions R)
then reconsider w = inversions R as finite set ;
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c< inversions R
by A1, Th72;
then
((R,x,y) incl) .: (inversions (Swap (R,x,y))) c= w
;
then reconsider hws = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) as finite set ;
card hws < card w
by A1, Th72, TREES_1:6;
then A2:
card hws in Segm (card w)
by NAT_1:44;
A3:
( x in dom R & y in dom R & x in y )
by A1, Th46;
A4:
not R is empty
by A1;
inversions (Swap (R,x,y)),((R,x,y) incl) .: (inversions (Swap (R,x,y))) are_equipotent
proof
take hw =
((R,x,y) incl) | (inversions (Swap (R,x,y)));
WELLORD2:def 4 ( hw is one-to-one & proj1 hw = inversions (Swap (R,x,y)) & proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) )
thus
hw is
one-to-one
by A3, A4, Th71;
( proj1 hw = inversions (Swap (R,x,y)) & proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y))) )
dom (Swap (R,x,y)) = dom R
by FUNCT_7:99;
then
inversions (Swap (R,x,y)) c= [:(dom R),(dom R):]
by Th47;
then
inversions (Swap (R,x,y)) c= dom ((R,x,y) incl)
by A3, A4, Th61;
hence
dom hw = inversions (Swap (R,x,y))
by RELAT_1:62;
proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y)))
thus
proj2 hw = ((R,x,y) incl) .: (inversions (Swap (R,x,y)))
by RELAT_1:115;
verum
end;
hence
card (inversions (Swap (R,x,y))) in card (inversions R)
by A2, CARD_1:5; verum