Metamath Proof Explorer

Theorem omword1

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

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

Proof

Step Hyp Ref Expression
1 eloni 
 |-  ( B e. On -> Ord B )
2 ordgt0ge1 
 |-  ( Ord B -> ( (/) e. B <-> 1o C_ B ) )
3 1 2 syl 
 |-  ( B e. On -> ( (/) e. B <-> 1o C_ B ) )
4 3 adantl 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. B <-> 1o C_ B ) )
5 1on 
 |-  1o e. On
6 omwordi 
 |-  ( ( 1o e. On /\ B e. On /\ A e. On ) -> ( 1o C_ B -> ( A .o 1o ) C_ ( A .o B ) ) )
7 5 6 mp3an1 
 |-  ( ( B e. On /\ A e. On ) -> ( 1o C_ B -> ( A .o 1o ) C_ ( A .o B ) ) )
8 7 ancoms 
 |-  ( ( A e. On /\ B e. On ) -> ( 1o C_ B -> ( A .o 1o ) C_ ( A .o B ) ) )
9 om1 
 |-  ( A e. On -> ( A .o 1o ) = A )
10 9 adantr 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o 1o ) = A )
11 10 sseq1d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o 1o ) C_ ( A .o B ) <-> A C_ ( A .o B ) ) )
12 8 11 sylibd 
 |-  ( ( A e. On /\ B e. On ) -> ( 1o C_ B -> A C_ ( A .o B ) ) )
13 4 12 sylbid 
 |-  ( ( A e. On /\ B e. On ) -> ( (/) e. B -> A C_ ( A .o B ) ) )
14 13 imp 
 |-  ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> A C_ ( A .o B ) )