let o be Ordinal; :: thesis: GrInvLexOrder o is well-ordering

set gilo = GrInvLexOrder o;

set ilo = InvLexOrder o;

A1: GrInvLexOrder o is_strongly_connected_in Bags o by Def5;

A2: field (GrInvLexOrder o) = Bags o by ORDERS_1:12;

then A3: GrInvLexOrder o is_reflexive_in Bags o by RELAT_2:def 9;

A4: GrInvLexOrder o is_transitive_in Bags o by A2, RELAT_2:def 16;

A5: GrInvLexOrder o is_antisymmetric_in Bags o by A2, RELAT_2:def 12;

A6: GrInvLexOrder o is_connected_in field (GrInvLexOrder o) by A1, A2;

A7: for a, b, c being bag of o st [a,b] in InvLexOrder o holds

[(a + c),(b + c)] in InvLexOrder o by Def5;

then GrInvLexOrder o well_orders field (GrInvLexOrder o) by A2, A3, A4, A5, A6, WELLORD1:def 5;

hence GrInvLexOrder o is well-ordering by WELLORD1:4; :: thesis: verum

set gilo = GrInvLexOrder o;

set ilo = InvLexOrder o;

A1: GrInvLexOrder o is_strongly_connected_in Bags o by Def5;

A2: field (GrInvLexOrder o) = Bags o by ORDERS_1:12;

then A3: GrInvLexOrder o is_reflexive_in Bags o by RELAT_2:def 9;

A4: GrInvLexOrder o is_transitive_in Bags o by A2, RELAT_2:def 16;

A5: GrInvLexOrder o is_antisymmetric_in Bags o by A2, RELAT_2:def 12;

A6: GrInvLexOrder o is_connected_in field (GrInvLexOrder o) by A1, A2;

A7: for a, b, c being bag of o st [a,b] in InvLexOrder o holds

[(a + c),(b + c)] in InvLexOrder o by Def5;

now :: thesis: for Y being set st Y c= field (GrInvLexOrder o) & Y <> {} holds

ex a being object st

( a in Y & (GrInvLexOrder o) -Seg a misses Y )

then
GrInvLexOrder o is_well_founded_in field (GrInvLexOrder o)
by WELLORD1:def 3;ex a being object st

( a in Y & (GrInvLexOrder o) -Seg a misses Y )

let Y be set ; :: thesis: ( Y c= field (GrInvLexOrder o) & Y <> {} implies ex a being object st

( a in Y & (GrInvLexOrder o) -Seg a misses Y ) )

assume that

A8: Y c= field (GrInvLexOrder o) and

A9: Y <> {} ; :: thesis: ex a being object st

( a in Y & (GrInvLexOrder o) -Seg a misses Y )

set TD = { (TotDegree y) where y is Element of Bags o : y in Y } ;

consider x being object such that

A10: x in Y by A9, XBOOLE_0:def 1;

reconsider x = x as Element of Bags o by A8, A10, ORDERS_1:12;

A11: TotDegree x in { (TotDegree y) where y is Element of Bags o : y in Y } by A10;

{ (TotDegree y) where y is Element of Bags o : y in Y } c= NAT

set mTD = { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } ;

A12: { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } c= field (GrInvLexOrder o)

then consider y being Element of Bags o such that

A13: TotDegree y = min TD and

A14: y in Y ;

A15: y in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } by A13, A14;

A16: field (InvLexOrder o) = Bags o by ORDERS_1:12;

InvLexOrder o is well-ordering by Th22;

then InvLexOrder o well_orders field (InvLexOrder o) by WELLORD1:4;

then InvLexOrder o is_well_founded_in field (InvLexOrder o) by WELLORD1:def 5;

then consider a being object such that

A17: a in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } and

A18: (InvLexOrder o) -Seg a misses { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } by A2, A12, A15, A16, WELLORD1:def 3;

A19: ((InvLexOrder o) -Seg a) /\ { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } = {} by A18, XBOOLE_0:def 7;

A20: ex a9 being Element of Bags o st

( a9 = a & a9 in Y & TotDegree a9 = min TD ) by A17;

take a = a; :: thesis: ( a in Y & (GrInvLexOrder o) -Seg a misses Y )

thus a in Y by A20; :: thesis: (GrInvLexOrder o) -Seg a misses Y

end;( a in Y & (GrInvLexOrder o) -Seg a misses Y ) )

assume that

A8: Y c= field (GrInvLexOrder o) and

A9: Y <> {} ; :: thesis: ex a being object st

( a in Y & (GrInvLexOrder o) -Seg a misses Y )

set TD = { (TotDegree y) where y is Element of Bags o : y in Y } ;

consider x being object such that

A10: x in Y by A9, XBOOLE_0:def 1;

reconsider x = x as Element of Bags o by A8, A10, ORDERS_1:12;

A11: TotDegree x in { (TotDegree y) where y is Element of Bags o : y in Y } by A10;

{ (TotDegree y) where y is Element of Bags o : y in Y } c= NAT

proof

then reconsider TD = { (TotDegree y) where y is Element of Bags o : y in Y } as non empty Subset of NAT by A11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (TotDegree y) where y is Element of Bags o : y in Y } or x in NAT )

assume x in { (TotDegree y) where y is Element of Bags o : y in Y } ; :: thesis: x in NAT

then ex y being Element of Bags o st

( x = TotDegree y & y in Y ) ;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume x in { (TotDegree y) where y is Element of Bags o : y in Y } ; :: thesis: x in NAT

then ex y being Element of Bags o st

( x = TotDegree y & y in Y ) ;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

set mTD = { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } ;

A12: { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } c= field (GrInvLexOrder o)

proof

min TD in TD
by XXREAL_2:def 7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } or x in field (GrInvLexOrder o) )

assume x in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } ; :: thesis: x in field (GrInvLexOrder o)

then ex y being Element of Bags o st

( x = y & y in Y & TotDegree y = min TD ) ;

hence x in field (GrInvLexOrder o) by A2; :: thesis: verum

end;assume x in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } ; :: thesis: x in field (GrInvLexOrder o)

then ex y being Element of Bags o st

( x = y & y in Y & TotDegree y = min TD ) ;

hence x in field (GrInvLexOrder o) by A2; :: thesis: verum

then consider y being Element of Bags o such that

A13: TotDegree y = min TD and

A14: y in Y ;

A15: y in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } by A13, A14;

A16: field (InvLexOrder o) = Bags o by ORDERS_1:12;

InvLexOrder o is well-ordering by Th22;

then InvLexOrder o well_orders field (InvLexOrder o) by WELLORD1:4;

then InvLexOrder o is_well_founded_in field (InvLexOrder o) by WELLORD1:def 5;

then consider a being object such that

A17: a in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } and

A18: (InvLexOrder o) -Seg a misses { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } by A2, A12, A15, A16, WELLORD1:def 3;

A19: ((InvLexOrder o) -Seg a) /\ { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } = {} by A18, XBOOLE_0:def 7;

A20: ex a9 being Element of Bags o st

( a9 = a & a9 in Y & TotDegree a9 = min TD ) by A17;

take a = a; :: thesis: ( a in Y & (GrInvLexOrder o) -Seg a misses Y )

thus a in Y by A20; :: thesis: (GrInvLexOrder o) -Seg a misses Y

now :: thesis: not ((GrInvLexOrder o) -Seg a) /\ Y <> {}

hence
(GrInvLexOrder o) -Seg a misses Y
by XBOOLE_0:def 7; :: thesis: verumassume
((GrInvLexOrder o) -Seg a) /\ Y <> {}
; :: thesis: contradiction

then consider z being object such that

A21: z in ((GrInvLexOrder o) -Seg a) /\ Y by XBOOLE_0:def 1;

A22: z in (GrInvLexOrder o) -Seg a by A21, XBOOLE_0:def 4;

A23: z in Y by A21, XBOOLE_0:def 4;

A24: z <> a by A22, WELLORD1:1;

A25: [z,a] in GrInvLexOrder o by A22, WELLORD1:1;

reconsider a = a, z = z as Element of Bags o by A8, A20, A23, ORDERS_1:12;

end;then consider z being object such that

A21: z in ((GrInvLexOrder o) -Seg a) /\ Y by XBOOLE_0:def 1;

A22: z in (GrInvLexOrder o) -Seg a by A21, XBOOLE_0:def 4;

A23: z in Y by A21, XBOOLE_0:def 4;

A24: z <> a by A22, WELLORD1:1;

A25: [z,a] in GrInvLexOrder o by A22, WELLORD1:1;

reconsider a = a, z = z as Element of Bags o by A8, A20, A23, ORDERS_1:12;

per cases
( TotDegree z < TotDegree a or TotDegree z = TotDegree a or TotDegree z > TotDegree a )
by XXREAL_0:1;

end;

suppose A27:
TotDegree z = TotDegree a
; :: thesis: contradiction

then
[z,a] in InvLexOrder o
by A7, A25, Def7;

then A28: z in (InvLexOrder o) -Seg a by A24, WELLORD1:1;

z in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } by A20, A23, A27;

hence contradiction by A19, A28, XBOOLE_0:def 4; :: thesis: verum

end;then A28: z in (InvLexOrder o) -Seg a by A24, WELLORD1:1;

z in { y where y is Element of Bags o : ( y in Y & TotDegree y = min TD ) } by A20, A23, A27;

hence contradiction by A19, A28, XBOOLE_0:def 4; :: thesis: verum

then GrInvLexOrder o well_orders field (GrInvLexOrder o) by A2, A3, A4, A5, A6, WELLORD1:def 5;

hence GrInvLexOrder o is well-ordering by WELLORD1:4; :: thesis: verum