Metamath Proof Explorer

Theorem oaordi

Description: Ordering property of ordinal addition. Proposition 8.4 of TakeutiZaring p. 58. (Contributed by NM, 5-Dec-2004)

Ref Expression
Assertion oaordi 
|- ( ( B e. On /\ C e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )

Proof

Step Hyp Ref Expression
1 onelon 
 |-  ( ( B e. On /\ A e. B ) -> A e. On )
2 1 adantll 
 |-  ( ( ( C e. On /\ B e. On ) /\ A e. B ) -> A e. On )
3 eloni 
 |-  ( B e. On -> Ord B )
4 ordsucss 
 |-  ( Ord B -> ( A e. B -> suc A C_ B ) )
5 3 4 syl 
 |-  ( B e. On -> ( A e. B -> suc A C_ B ) )
6 5 ad2antlr 
 |-  ( ( ( C e. On /\ B e. On ) /\ A e. On ) -> ( A e. B -> suc A C_ B ) )
7 sucelon 
 |-  ( A e. On <-> suc A e. On )
8 oveq2 
 |-  ( x = suc A -> ( C +o x ) = ( C +o suc A ) )
9 8 sseq2d 
 |-  ( x = suc A -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o suc A ) ) )
10 9 imbi2d 
 |-  ( x = suc A -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. On -> ( C +o suc A ) C_ ( C +o suc A ) ) ) )
11 oveq2 
 |-  ( x = y -> ( C +o x ) = ( C +o y ) )
12 11 sseq2d 
 |-  ( x = y -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o y ) ) )
13 12 imbi2d 
 |-  ( x = y -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. On -> ( C +o suc A ) C_ ( C +o y ) ) ) )
14 oveq2 
 |-  ( x = suc y -> ( C +o x ) = ( C +o suc y ) )
15 14 sseq2d 
 |-  ( x = suc y -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o suc y ) ) )
16 15 imbi2d 
 |-  ( x = suc y -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. On -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
17 oveq2 
 |-  ( x = B -> ( C +o x ) = ( C +o B ) )
18 17 sseq2d 
 |-  ( x = B -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o B ) ) )
19 18 imbi2d 
 |-  ( x = B -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. On -> ( C +o suc A ) C_ ( C +o B ) ) ) )
20 ssid 
 |-  ( C +o suc A ) C_ ( C +o suc A )
21 20 2a1i 
 |-  ( suc A e. On -> ( C e. On -> ( C +o suc A ) C_ ( C +o suc A ) ) )
22 sssucid 
 |-  ( C +o y ) C_ suc ( C +o y )
23 sstr2 
 |-  ( ( C +o suc A ) C_ ( C +o y ) -> ( ( C +o y ) C_ suc ( C +o y ) -> ( C +o suc A ) C_ suc ( C +o y ) ) )
24 22 23 mpi 
 |-  ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ suc ( C +o y ) )
25 oasuc 
 |-  ( ( C e. On /\ y e. On ) -> ( C +o suc y ) = suc ( C +o y ) )
26 25 ancoms 
 |-  ( ( y e. On /\ C e. On ) -> ( C +o suc y ) = suc ( C +o y ) )
27 26 sseq2d 
 |-  ( ( y e. On /\ C e. On ) -> ( ( C +o suc A ) C_ ( C +o suc y ) <-> ( C +o suc A ) C_ suc ( C +o y ) ) )
28 24 27 syl5ibr 
 |-  ( ( y e. On /\ C e. On ) -> ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ ( C +o suc y ) ) )
29 28 ex 
 |-  ( y e. On -> ( C e. On -> ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
30 29 ad2antrr 
 |-  ( ( ( y e. On /\ suc A e. On ) /\ suc A C_ y ) -> ( C e. On -> ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
31 30 a2d 
 |-  ( ( ( y e. On /\ suc A e. On ) /\ suc A C_ y ) -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o y ) ) -> ( C e. On -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
32 sucssel 
 |-  ( A e. On -> ( suc A C_ x -> A e. x ) )
33 7 32 sylbir 
 |-  ( suc A e. On -> ( suc A C_ x -> A e. x ) )
34 limsuc 
 |-  ( Lim x -> ( A e. x <-> suc A e. x ) )
35 34 biimpd 
 |-  ( Lim x -> ( A e. x -> suc A e. x ) )
36 33 35 sylan9r 
 |-  ( ( Lim x /\ suc A e. On ) -> ( suc A C_ x -> suc A e. x ) )
37 36 imp 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> suc A e. x )
38 oveq2 
 |-  ( y = suc A -> ( C +o y ) = ( C +o suc A ) )
39 38 ssiun2s 
 |-  ( suc A e. x -> ( C +o suc A ) C_ U_ y e. x ( C +o y ) )
40 37 39 syl 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> ( C +o suc A ) C_ U_ y e. x ( C +o y ) )
41 40 adantr 
 |-  ( ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) /\ C e. On ) -> ( C +o suc A ) C_ U_ y e. x ( C +o y ) )
42 vex 
 |-  x e. _V
43 oalim 
 |-  ( ( C e. On /\ ( x e. _V /\ Lim x ) ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
44 42 43 mpanr1 
 |-  ( ( C e. On /\ Lim x ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
45 44 ancoms 
 |-  ( ( Lim x /\ C e. On ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
46 45 adantlr 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ C e. On ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
47 46 adantlr 
 |-  ( ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) /\ C e. On ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
48 41 47 sseqtrrd 
 |-  ( ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) /\ C e. On ) -> ( C +o suc A ) C_ ( C +o x ) )
49 48 ex 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) )
50 49 a1d 
 |-  ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> ( A. y e. x ( suc A C_ y -> ( C e. On -> ( C +o suc A ) C_ ( C +o y ) ) ) -> ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) ) )
51 10 13 16 19 21 31 50 tfindsg 
 |-  ( ( ( B e. On /\ suc A e. On ) /\ suc A C_ B ) -> ( C e. On -> ( C +o suc A ) C_ ( C +o B ) ) )
52 51 exp31 
 |-  ( B e. On -> ( suc A e. On -> ( suc A C_ B -> ( C e. On -> ( C +o suc A ) C_ ( C +o B ) ) ) ) )
53 7 52 syl5bi 
 |-  ( B e. On -> ( A e. On -> ( suc A C_ B -> ( C e. On -> ( C +o suc A ) C_ ( C +o B ) ) ) ) )
54 53 com4r 
 |-  ( C e. On -> ( B e. On -> ( A e. On -> ( suc A C_ B -> ( C +o suc A ) C_ ( C +o B ) ) ) ) )
55 54 imp31 
 |-  ( ( ( C e. On /\ B e. On ) /\ A e. On ) -> ( suc A C_ B -> ( C +o suc A ) C_ ( C +o B ) ) )
56 oasuc 
 |-  ( ( C e. On /\ A e. On ) -> ( C +o suc A ) = suc ( C +o A ) )
57 56 sseq1d 
 |-  ( ( C e. On /\ A e. On ) -> ( ( C +o suc A ) C_ ( C +o B ) <-> suc ( C +o A ) C_ ( C +o B ) ) )
58 ovex 
 |-  ( C +o A ) e. _V
59 sucssel 
 |-  ( ( C +o A ) e. _V -> ( suc ( C +o A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) ) )
60 58 59 ax-mp 
 |-  ( suc ( C +o A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) )
61 57 60 syl6bi 
 |-  ( ( C e. On /\ A e. On ) -> ( ( C +o suc A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) ) )
62 61 adantlr 
 |-  ( ( ( C e. On /\ B e. On ) /\ A e. On ) -> ( ( C +o suc A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) ) )
63 6 55 62 3syld 
 |-  ( ( ( C e. On /\ B e. On ) /\ A e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
64 63 imp 
 |-  ( ( ( ( C e. On /\ B e. On ) /\ A e. On ) /\ A e. B ) -> ( C +o A ) e. ( C +o B ) )
65 64 an32s 
 |-  ( ( ( ( C e. On /\ B e. On ) /\ A e. B ) /\ A e. On ) -> ( C +o A ) e. ( C +o B ) )
66 2 65 mpdan 
 |-  ( ( ( C e. On /\ B e. On ) /\ A e. B ) -> ( C +o A ) e. ( C +o B ) )
67 66 ex 
 |-  ( ( C e. On /\ B e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
68 67 ancoms 
 |-  ( ( B e. On /\ C e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )