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 )