Metamath Proof Explorer

Theorem oawordri

Description: Weak ordering property of ordinal addition. Proposition 8.7 of TakeutiZaring p. 59. (Contributed by NM, 7-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = (/) -> ( A +o x ) = ( A +o (/) ) )
2 oveq2 
 |-  ( x = (/) -> ( B +o x ) = ( B +o (/) ) )
3 1 2 sseq12d 
 |-  ( x = (/) -> ( ( A +o x ) C_ ( B +o x ) <-> ( A +o (/) ) C_ ( B +o (/) ) ) )
4 oveq2 
 |-  ( x = y -> ( A +o x ) = ( A +o y ) )
5 oveq2 
 |-  ( x = y -> ( B +o x ) = ( B +o y ) )
6 4 5 sseq12d 
 |-  ( x = y -> ( ( A +o x ) C_ ( B +o x ) <-> ( A +o y ) C_ ( B +o y ) ) )
7 oveq2 
 |-  ( x = suc y -> ( A +o x ) = ( A +o suc y ) )
8 oveq2 
 |-  ( x = suc y -> ( B +o x ) = ( B +o suc y ) )
9 7 8 sseq12d 
 |-  ( x = suc y -> ( ( A +o x ) C_ ( B +o x ) <-> ( A +o suc y ) C_ ( B +o suc y ) ) )
10 oveq2 
 |-  ( x = C -> ( A +o x ) = ( A +o C ) )
11 oveq2 
 |-  ( x = C -> ( B +o x ) = ( B +o C ) )
12 10 11 sseq12d 
 |-  ( x = C -> ( ( A +o x ) C_ ( B +o x ) <-> ( A +o C ) C_ ( B +o C ) ) )
13 oa0 
 |-  ( A e. On -> ( A +o (/) ) = A )
14 13 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o (/) ) = A )
15 oa0 
 |-  ( B e. On -> ( B +o (/) ) = B )
16 15 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( B +o (/) ) = B )
17 14 16 sseq12d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o (/) ) C_ ( B +o (/) ) <-> A C_ B ) )
18 17 biimpar 
 |-  ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( A +o (/) ) C_ ( B +o (/) ) )
19 oacl 
 |-  ( ( A e. On /\ y e. On ) -> ( A +o y ) e. On )
20 eloni 
 |-  ( ( A +o y ) e. On -> Ord ( A +o y ) )
21 19 20 syl 
 |-  ( ( A e. On /\ y e. On ) -> Ord ( A +o y ) )
22 oacl 
 |-  ( ( B e. On /\ y e. On ) -> ( B +o y ) e. On )
23 eloni 
 |-  ( ( B +o y ) e. On -> Ord ( B +o y ) )
24 22 23 syl 
 |-  ( ( B e. On /\ y e. On ) -> Ord ( B +o y ) )
25 ordsucsssuc 
 |-  ( ( Ord ( A +o y ) /\ Ord ( B +o y ) ) -> ( ( A +o y ) C_ ( B +o y ) <-> suc ( A +o y ) C_ suc ( B +o y ) ) )
26 21 24 25 syl2an 
 |-  ( ( ( A e. On /\ y e. On ) /\ ( B e. On /\ y e. On ) ) -> ( ( A +o y ) C_ ( B +o y ) <-> suc ( A +o y ) C_ suc ( B +o y ) ) )
27 26 anandirs 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( ( A +o y ) C_ ( B +o y ) <-> suc ( A +o y ) C_ suc ( B +o y ) ) )
28 oasuc 
 |-  ( ( A e. On /\ y e. On ) -> ( A +o suc y ) = suc ( A +o y ) )
29 28 adantlr 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( A +o suc y ) = suc ( A +o y ) )
30 oasuc 
 |-  ( ( B e. On /\ y e. On ) -> ( B +o suc y ) = suc ( B +o y ) )
31 30 adantll 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( B +o suc y ) = suc ( B +o y ) )
32 29 31 sseq12d 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( ( A +o suc y ) C_ ( B +o suc y ) <-> suc ( A +o y ) C_ suc ( B +o y ) ) )
33 27 32 bitr4d 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( ( A +o y ) C_ ( B +o y ) <-> ( A +o suc y ) C_ ( B +o suc y ) ) )
34 33 biimpd 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. On ) -> ( ( A +o y ) C_ ( B +o y ) -> ( A +o suc y ) C_ ( B +o suc y ) ) )
35 34 expcom 
 |-  ( y e. On -> ( ( A e. On /\ B e. On ) -> ( ( A +o y ) C_ ( B +o y ) -> ( A +o suc y ) C_ ( B +o suc y ) ) ) )
36 35 adantrd 
 |-  ( y e. On -> ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( ( A +o y ) C_ ( B +o y ) -> ( A +o suc y ) C_ ( B +o suc y ) ) ) )
37 vex 
 |-  x e. _V
38 ss2iun 
 |-  ( A. y e. x ( A +o y ) C_ ( B +o y ) -> U_ y e. x ( A +o y ) C_ U_ y e. x ( B +o y ) )
39 oalim 
 |-  ( ( A e. On /\ ( x e. _V /\ Lim x ) ) -> ( A +o x ) = U_ y e. x ( A +o y ) )
40 39 adantlr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. _V /\ Lim x ) ) -> ( A +o x ) = U_ y e. x ( A +o y ) )
41 oalim 
 |-  ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> ( B +o x ) = U_ y e. x ( B +o y ) )
42 41 adantll 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. _V /\ Lim x ) ) -> ( B +o x ) = U_ y e. x ( B +o y ) )
43 40 42 sseq12d 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. _V /\ Lim x ) ) -> ( ( A +o x ) C_ ( B +o x ) <-> U_ y e. x ( A +o y ) C_ U_ y e. x ( B +o y ) ) )
44 38 43 imbitrrid 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( x e. _V /\ Lim x ) ) -> ( A. y e. x ( A +o y ) C_ ( B +o y ) -> ( A +o x ) C_ ( B +o x ) ) )
45 37 44 mpanr1 
 |-  ( ( ( A e. On /\ B e. On ) /\ Lim x ) -> ( A. y e. x ( A +o y ) C_ ( B +o y ) -> ( A +o x ) C_ ( B +o x ) ) )
46 45 expcom 
 |-  ( Lim x -> ( ( A e. On /\ B e. On ) -> ( A. y e. x ( A +o y ) C_ ( B +o y ) -> ( A +o x ) C_ ( B +o x ) ) ) )
47 46 adantrd 
 |-  ( Lim x -> ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( A. y e. x ( A +o y ) C_ ( B +o y ) -> ( A +o x ) C_ ( B +o x ) ) ) )
48 3 6 9 12 18 36 47 tfinds3 
 |-  ( C e. On -> ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( A +o C ) C_ ( B +o C ) ) )
49 48 exp4c 
 |-  ( C e. On -> ( A e. On -> ( B e. On -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) ) ) )
50 49 3imp231 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) )