Metamath Proof Explorer

Theorem omwordri

Description: Weak ordering property of ordinal multiplication. Proposition 8.21 of TakeutiZaring p. 63. (Contributed by NM, 20-Dec-2004)

Ref Expression
Assertion omwordri 
|- ( ( 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 om0 
 |-  ( A e. On -> ( A .o (/) ) = (/) )
14 0ss 
 |-  (/) C_ ( B .o (/) )
15 13 14 eqsstrdi 
 |-  ( A e. On -> ( A .o (/) ) C_ ( B .o (/) ) )
16 15 ad2antrr 
 |-  ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( A .o (/) ) C_ ( B .o (/) ) )
17 omcl 
 |-  ( ( A e. On /\ y e. On ) -> ( A .o y ) e. On )
18 17 3adant2 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( A .o y ) e. On )
19 omcl 
 |-  ( ( B e. On /\ y e. On ) -> ( B .o y ) e. On )
20 19 3adant1 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( B .o y ) e. On )
21 simp1 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> A e. On )
22 oawordri 
 |-  ( ( ( A .o y ) e. On /\ ( B .o y ) e. On /\ A e. On ) -> ( ( A .o y ) C_ ( B .o y ) -> ( ( A .o y ) +o A ) C_ ( ( B .o y ) +o A ) ) )
23 18 20 21 22 syl3anc 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( ( A .o y ) C_ ( B .o y ) -> ( ( A .o y ) +o A ) C_ ( ( B .o y ) +o A ) ) )
24 23 imp 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A .o y ) C_ ( B .o y ) ) -> ( ( A .o y ) +o A ) C_ ( ( B .o y ) +o A ) )
25 24 adantrl 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A .o y ) C_ ( B .o y ) ) ) -> ( ( A .o y ) +o A ) C_ ( ( B .o y ) +o A ) )
26 oaword 
 |-  ( ( A e. On /\ B e. On /\ ( B .o y ) e. On ) -> ( A C_ B <-> ( ( B .o y ) +o A ) C_ ( ( B .o y ) +o B ) ) )
27 20 26 syld3an3 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( A C_ B <-> ( ( B .o y ) +o A ) C_ ( ( B .o y ) +o B ) ) )
28 27 biimpa 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ A C_ B ) -> ( ( B .o y ) +o A ) C_ ( ( B .o y ) +o B ) )
29 28 adantrr 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A .o y ) C_ ( B .o y ) ) ) -> ( ( B .o y ) +o A ) C_ ( ( B .o y ) +o B ) )
30 25 29 sstrd 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A .o y ) C_ ( B .o y ) ) ) -> ( ( A .o y ) +o A ) C_ ( ( B .o y ) +o B ) )
31 omsuc 
 |-  ( ( A e. On /\ y e. On ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
32 31 3adant2 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
33 32 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A .o y ) C_ ( B .o y ) ) ) -> ( A .o suc y ) = ( ( A .o y ) +o A ) )
34 omsuc 
 |-  ( ( B e. On /\ y e. On ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
35 34 3adant1 
 |-  ( ( A e. On /\ B e. On /\ y e. On ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
36 35 adantr 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A .o y ) C_ ( B .o y ) ) ) -> ( B .o suc y ) = ( ( B .o y ) +o B ) )
37 30 33 36 3sstr4d 
 |-  ( ( ( A e. On /\ B e. On /\ y e. On ) /\ ( A C_ B /\ ( A .o y ) C_ ( B .o y ) ) ) -> ( A .o suc y ) C_ ( B .o suc y ) )
38 37 exp520 
 |-  ( A e. On -> ( B e. On -> ( y e. On -> ( A C_ B -> ( ( A .o y ) C_ ( B .o y ) -> ( A .o suc y ) C_ ( B .o suc y ) ) ) ) ) )
39 38 com3r 
 |-  ( 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 ) ) ) ) ) )
40 39 imp4c 
 |-  ( 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 ) ) ) )
41 vex 
 |-  x e. _V
42 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 ) )
43 omlim 
 |-  ( ( A e. On /\ ( x e. _V /\ Lim x ) ) -> ( A .o x ) = U_ y e. x ( A .o y ) )
44 43 ad2ant2rl 
 |-  ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ ( B e. On /\ ( x e. _V /\ Lim x ) ) ) -> ( A .o x ) = U_ y e. x ( A .o y ) )
45 omlim 
 |-  ( ( B e. On /\ ( x e. _V /\ Lim x ) ) -> ( B .o x ) = U_ y e. x ( B .o y ) )
46 45 adantl 
 |-  ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ ( B e. On /\ ( x e. _V /\ Lim x ) ) ) -> ( B .o x ) = U_ y e. x ( B .o y ) )
47 44 46 sseq12d 
 |-  ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ ( 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 ) ) )
48 42 47 imbitrrid 
 |-  ( ( ( A e. On /\ ( x e. _V /\ Lim x ) ) /\ ( 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 ) ) )
49 48 anandirs 
 |-  ( ( ( 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 ) ) )
50 41 49 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 ) ) )
51 50 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 ) ) ) )
52 51 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 ) ) ) )
53 3 6 9 12 16 40 52 tfinds3 
 |-  ( C e. On -> ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( A .o C ) C_ ( B .o C ) ) )
54 53 expd 
 |-  ( C e. On -> ( ( A e. On /\ B e. On ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) ) )
55 54 3impib 
 |-  ( ( C e. On /\ A e. On /\ B e. On ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) )
56 55 3coml 
 |-  ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) )