Metamath Proof Explorer


Theorem oaabs

Description: Ordinal addition absorbs a natural number added to the left of a transfinite number. Proposition 8.10 of TakeutiZaring p. 59. (Contributed by NM, 9-Dec-2004) (Proof shortened by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion oaabs
|- ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> ( A +o B ) = B )

Proof

Step Hyp Ref Expression
1 ssexg
 |-  ( ( _om C_ B /\ B e. On ) -> _om e. _V )
2 1 ex
 |-  ( _om C_ B -> ( B e. On -> _om e. _V ) )
3 omelon2
 |-  ( _om e. _V -> _om e. On )
4 2 3 syl6com
 |-  ( B e. On -> ( _om C_ B -> _om e. On ) )
5 4 imp
 |-  ( ( B e. On /\ _om C_ B ) -> _om e. On )
6 5 adantll
 |-  ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> _om e. On )
7 simplr
 |-  ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> B e. On )
8 6 7 jca
 |-  ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> ( _om e. On /\ B e. On ) )
9 oawordeu
 |-  ( ( ( _om e. On /\ B e. On ) /\ _om C_ B ) -> E! x e. On ( _om +o x ) = B )
10 8 9 sylancom
 |-  ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> E! x e. On ( _om +o x ) = B )
11 reurex
 |-  ( E! x e. On ( _om +o x ) = B -> E. x e. On ( _om +o x ) = B )
12 10 11 syl
 |-  ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> E. x e. On ( _om +o x ) = B )
13 nnon
 |-  ( A e. _om -> A e. On )
14 13 ad3antrrr
 |-  ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> A e. On )
15 6 adantr
 |-  ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> _om e. On )
16 simpr
 |-  ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> x e. On )
17 oaass
 |-  ( ( A e. On /\ _om e. On /\ x e. On ) -> ( ( A +o _om ) +o x ) = ( A +o ( _om +o x ) ) )
18 14 15 16 17 syl3anc
 |-  ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( ( A +o _om ) +o x ) = ( A +o ( _om +o x ) ) )
19 simpll
 |-  ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> A e. _om )
20 oaabslem
 |-  ( ( _om e. On /\ A e. _om ) -> ( A +o _om ) = _om )
21 6 19 20 syl2anc
 |-  ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> ( A +o _om ) = _om )
22 21 adantr
 |-  ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( A +o _om ) = _om )
23 22 oveq1d
 |-  ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( ( A +o _om ) +o x ) = ( _om +o x ) )
24 18 23 eqtr3d
 |-  ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( A +o ( _om +o x ) ) = ( _om +o x ) )
25 oveq2
 |-  ( ( _om +o x ) = B -> ( A +o ( _om +o x ) ) = ( A +o B ) )
26 id
 |-  ( ( _om +o x ) = B -> ( _om +o x ) = B )
27 25 26 eqeq12d
 |-  ( ( _om +o x ) = B -> ( ( A +o ( _om +o x ) ) = ( _om +o x ) <-> ( A +o B ) = B ) )
28 24 27 syl5ibcom
 |-  ( ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) /\ x e. On ) -> ( ( _om +o x ) = B -> ( A +o B ) = B ) )
29 28 rexlimdva
 |-  ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> ( E. x e. On ( _om +o x ) = B -> ( A +o B ) = B ) )
30 12 29 mpd
 |-  ( ( ( A e. _om /\ B e. On ) /\ _om C_ B ) -> ( A +o B ) = B )