Metamath Proof Explorer

Theorem omword2

Description: An ordinal is less than or equal to its product with another. Lemma 3.12 of Schloeder p. 9. (Contributed by NM, 21-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 om1r 
 |-  ( A e. On -> ( 1o .o A ) = A )
2 1 ad2antrr 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> ( 1o .o A ) = A )
3 eloni 
 |-  ( B e. On -> Ord B )
4 ordgt0ge1 
 |-  ( Ord B -> ( (/) e. B <-> 1o C_ B ) )
5 4 biimpa 
 |-  ( ( Ord B /\ (/) e. B ) -> 1o C_ B )
6 3 5 sylan 
 |-  ( ( B e. On /\ (/) e. B ) -> 1o C_ B )
7 6 adantll 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> 1o C_ B )
8 1on 
 |-  1o e. On
9 omwordri 
 |-  ( ( 1o e. On /\ B e. On /\ A e. On ) -> ( 1o C_ B -> ( 1o .o A ) C_ ( B .o A ) ) )
10 8 9 mp3an1 
 |-  ( ( B e. On /\ A e. On ) -> ( 1o C_ B -> ( 1o .o A ) C_ ( B .o A ) ) )
11 10 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( 1o C_ B -> ( 1o .o A ) C_ ( B .o A ) ) )
12 11 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> ( 1o C_ B -> ( 1o .o A ) C_ ( B .o A ) ) )
13 7 12 mpd 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> ( 1o .o A ) C_ ( B .o A ) )
14 2 13 eqsstrrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> A C_ ( B .o A ) )