Metamath Proof Explorer

Theorem omord2lim

Description: Given a limit ordinal, the product of any non-zero ordinal with an ordinal less than that limit ordinal is less than the product of the non-zero ordinal with the limit ordinal . Lemma 3.14 of Schloeder p. 9. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion omord2lim 
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) -> ( B e. C -> ( A .o B ) e. ( A .o C ) ) )

Proof

Step Hyp Ref Expression
1 limord 
 |-  ( Lim C -> Ord C )
2 1 ad2antrl 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) -> Ord C )
3 ordelon 
 |-  ( ( Ord C /\ B e. C ) -> B e. On )
4 2 3 sylan 
 |-  ( ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) /\ B e. C ) -> B e. On )
5 elex 
 |-  ( C e. V -> C e. _V )
6 1 5 anim12i 
 |-  ( ( Lim C /\ C e. V ) -> ( Ord C /\ C e. _V ) )
7 6 ad2antlr 
 |-  ( ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) /\ B e. C ) -> ( Ord C /\ C e. _V ) )
8 elon2 
 |-  ( C e. On <-> ( Ord C /\ C e. _V ) )
9 7 8 sylibr 
 |-  ( ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) /\ B e. C ) -> C e. On )
10 simplll 
 |-  ( ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) /\ B e. C ) -> A e. On )
11 simpr 
 |-  ( ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) /\ B e. C ) -> B e. C )
12 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
13 12 biimpar 
 |-  ( ( A e. On /\ A =/= (/) ) -> (/) e. A )
14 13 ad2antrr 
 |-  ( ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) /\ B e. C ) -> (/) e. A )
15 omord 
 |-  ( ( B e. On /\ C e. On /\ A e. On ) -> ( ( B e. C /\ (/) e. A ) <-> ( A .o B ) e. ( A .o C ) ) )
16 15 biimpa 
 |-  ( ( ( B e. On /\ C e. On /\ A e. On ) /\ ( B e. C /\ (/) e. A ) ) -> ( A .o B ) e. ( A .o C ) )
17 4 9 10 11 14 16 syl32anc 
 |-  ( ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) /\ B e. C ) -> ( A .o B ) e. ( A .o C ) )
18 17 ex 
 |-  ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim C /\ C e. V ) ) -> ( B e. C -> ( A .o B ) e. ( A .o C ) ) )