Metamath Proof Explorer

Theorem oaabsb

Description: The right addend absorbs the sum with an ordinal iff that ordinal times omega is less than or equal to the right addend. (Contributed by RP, 19-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om e. On
2 omcl 
 |-  ( ( A e. On /\ _om e. On ) -> ( A .o _om ) e. On )
3 1 2 mpan2 
 |-  ( A e. On -> ( A .o _om ) e. On )
4 oawordex 
 |-  ( ( ( A .o _om ) e. On /\ B e. On ) -> ( ( A .o _om ) C_ B <-> E. x e. On ( ( A .o _om ) +o x ) = B ) )
5 3 4 sylan 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o _om ) C_ B <-> E. x e. On ( ( A .o _om ) +o x ) = B ) )
6 simpl 
 |-  ( ( A e. On /\ B e. On ) -> A e. On )
7 6 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ x e. On ) -> A e. On )
8 3 ad2antrr 
 |-  ( ( ( A e. On /\ B e. On ) /\ x e. On ) -> ( A .o _om ) e. On )
9 simpr 
 |-  ( ( ( A e. On /\ B e. On ) /\ x e. On ) -> x e. On )
10 oaass 
 |-  ( ( A e. On /\ ( A .o _om ) e. On /\ x e. On ) -> ( ( A +o ( A .o _om ) ) +o x ) = ( A +o ( ( A .o _om ) +o x ) ) )
11 7 8 9 10 syl3anc 
 |-  ( ( ( A e. On /\ B e. On ) /\ x e. On ) -> ( ( A +o ( A .o _om ) ) +o x ) = ( A +o ( ( A .o _om ) +o x ) ) )
12 1on 
 |-  1o e. On
13 odi 
 |-  ( ( A e. On /\ 1o e. On /\ _om e. On ) -> ( A .o ( 1o +o _om ) ) = ( ( A .o 1o ) +o ( A .o _om ) ) )
14 12 1 13 mp3an23 
 |-  ( A e. On -> ( A .o ( 1o +o _om ) ) = ( ( A .o 1o ) +o ( A .o _om ) ) )
15 1oaomeqom 
 |-  ( 1o +o _om ) = _om
16 15 oveq2i 
 |-  ( A .o ( 1o +o _om ) ) = ( A .o _om )
17 16 a1i 
 |-  ( A e. On -> ( A .o ( 1o +o _om ) ) = ( A .o _om ) )
18 om1 
 |-  ( A e. On -> ( A .o 1o ) = A )
19 18 oveq1d 
 |-  ( A e. On -> ( ( A .o 1o ) +o ( A .o _om ) ) = ( A +o ( A .o _om ) ) )
20 14 17 19 3eqtr3rd 
 |-  ( A e. On -> ( A +o ( A .o _om ) ) = ( A .o _om ) )
21 20 oveq1d 
 |-  ( A e. On -> ( ( A +o ( A .o _om ) ) +o x ) = ( ( A .o _om ) +o x ) )
22 21 ad2antrr 
 |-  ( ( ( A e. On /\ B e. On ) /\ x e. On ) -> ( ( A +o ( A .o _om ) ) +o x ) = ( ( A .o _om ) +o x ) )
23 11 22 eqtr3d 
 |-  ( ( ( A e. On /\ B e. On ) /\ x e. On ) -> ( A +o ( ( A .o _om ) +o x ) ) = ( ( A .o _om ) +o x ) )
24 oveq2 
 |-  ( ( ( A .o _om ) +o x ) = B -> ( A +o ( ( A .o _om ) +o x ) ) = ( A +o B ) )
25 id 
 |-  ( ( ( A .o _om ) +o x ) = B -> ( ( A .o _om ) +o x ) = B )
26 24 25 eqeq12d 
 |-  ( ( ( A .o _om ) +o x ) = B -> ( ( A +o ( ( A .o _om ) +o x ) ) = ( ( A .o _om ) +o x ) <-> ( A +o B ) = B ) )
27 23 26 syl5ibcom 
 |-  ( ( ( A e. On /\ B e. On ) /\ x e. On ) -> ( ( ( A .o _om ) +o x ) = B -> ( A +o B ) = B ) )
28 27 rexlimdva 
 |-  ( ( A e. On /\ B e. On ) -> ( E. x e. On ( ( A .o _om ) +o x ) = B -> ( A +o B ) = B ) )
29 5 28 sylbid 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o _om ) C_ B -> ( A +o B ) = B ) )
30 limom 
 |-  Lim _om
31 omlim 
 |-  ( ( A e. On /\ ( _om e. On /\ Lim _om ) ) -> ( A .o _om ) = U_ x e. _om ( A .o x ) )
32 1 30 31 mpanr12 
 |-  ( A e. On -> ( A .o _om ) = U_ x e. _om ( A .o x ) )
33 32 ad2antrr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> ( A .o _om ) = U_ x e. _om ( A .o x ) )
34 oveq2 
 |-  ( x = (/) -> ( A .o x ) = ( A .o (/) ) )
35 34 sseq1d 
 |-  ( x = (/) -> ( ( A .o x ) C_ B <-> ( A .o (/) ) C_ B ) )
36 oveq2 
 |-  ( x = y -> ( A .o x ) = ( A .o y ) )
37 36 sseq1d 
 |-  ( x = y -> ( ( A .o x ) C_ B <-> ( A .o y ) C_ B ) )
38 oveq2 
 |-  ( x = suc y -> ( A .o x ) = ( A .o suc y ) )
39 38 sseq1d 
 |-  ( x = suc y -> ( ( A .o x ) C_ B <-> ( A .o suc y ) C_ B ) )
40 om0 
 |-  ( A e. On -> ( A .o (/) ) = (/) )
41 0ss 
 |-  (/) C_ B
42 40 41 eqsstrdi 
 |-  ( A e. On -> ( A .o (/) ) C_ B )
43 42 ad2antrr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> ( A .o (/) ) C_ B )
44 nnon 
 |-  ( y e. _om -> y e. On )
45 omcl 
 |-  ( ( A e. On /\ y e. On ) -> ( A .o y ) e. On )
46 6 44 45 syl2an 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. _om ) -> ( A .o y ) e. On )
47 simpr 
 |-  ( ( A e. On /\ B e. On ) -> B e. On )
48 47 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. _om ) -> B e. On )
49 6 adantr 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. _om ) -> A e. On )
50 46 48 49 3jca 
 |-  ( ( ( A e. On /\ B e. On ) /\ y e. _om ) -> ( ( A .o y ) e. On /\ B e. On /\ A e. On ) )
51 50 expcom 
 |-  ( y e. _om -> ( ( A e. On /\ B e. On ) -> ( ( A .o y ) e. On /\ B e. On /\ A e. On ) ) )
52 51 adantrd 
 |-  ( y e. _om -> ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> ( ( A .o y ) e. On /\ B e. On /\ A e. On ) ) )
53 52 imp 
 |-  ( ( y e. _om /\ ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) ) -> ( ( A .o y ) e. On /\ B e. On /\ A e. On ) )
54 oaword 
 |-  ( ( ( A .o y ) e. On /\ B e. On /\ A e. On ) -> ( ( A .o y ) C_ B <-> ( A +o ( A .o y ) ) C_ ( A +o B ) ) )
55 53 54 syl 
 |-  ( ( y e. _om /\ ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) ) -> ( ( A .o y ) C_ B <-> ( A +o ( A .o y ) ) C_ ( A +o B ) ) )
56 55 biimpa 
 |-  ( ( ( y e. _om /\ ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) ) /\ ( A .o y ) C_ B ) -> ( A +o ( A .o y ) ) C_ ( A +o B ) )
57 simpl 
 |-  ( ( A e. On /\ y e. _om ) -> A e. On )
58 12 a1i 
 |-  ( ( A e. On /\ y e. _om ) -> 1o e. On )
59 44 adantl 
 |-  ( ( A e. On /\ y e. _om ) -> y e. On )
60 odi 
 |-  ( ( A e. On /\ 1o e. On /\ y e. On ) -> ( A .o ( 1o +o y ) ) = ( ( A .o 1o ) +o ( A .o y ) ) )
61 57 58 59 60 syl3anc 
 |-  ( ( A e. On /\ y e. _om ) -> ( A .o ( 1o +o y ) ) = ( ( A .o 1o ) +o ( A .o y ) ) )
62 1onn 
 |-  1o e. _om
63 nnacom 
 |-  ( ( 1o e. _om /\ y e. _om ) -> ( 1o +o y ) = ( y +o 1o ) )
64 62 63 mpan 
 |-  ( y e. _om -> ( 1o +o y ) = ( y +o 1o ) )
65 oa1suc 
 |-  ( y e. On -> ( y +o 1o ) = suc y )
66 44 65 syl 
 |-  ( y e. _om -> ( y +o 1o ) = suc y )
67 64 66 eqtrd 
 |-  ( y e. _om -> ( 1o +o y ) = suc y )
68 67 oveq2d 
 |-  ( y e. _om -> ( A .o ( 1o +o y ) ) = ( A .o suc y ) )
69 68 adantl 
 |-  ( ( A e. On /\ y e. _om ) -> ( A .o ( 1o +o y ) ) = ( A .o suc y ) )
70 18 oveq1d 
 |-  ( A e. On -> ( ( A .o 1o ) +o ( A .o y ) ) = ( A +o ( A .o y ) ) )
71 70 adantr 
 |-  ( ( A e. On /\ y e. _om ) -> ( ( A .o 1o ) +o ( A .o y ) ) = ( A +o ( A .o y ) ) )
72 61 69 71 3eqtr3rd 
 |-  ( ( A e. On /\ y e. _om ) -> ( A +o ( A .o y ) ) = ( A .o suc y ) )
73 72 expcom 
 |-  ( y e. _om -> ( A e. On -> ( A +o ( A .o y ) ) = ( A .o suc y ) ) )
74 73 adantrd 
 |-  ( y e. _om -> ( ( A e. On /\ B e. On ) -> ( A +o ( A .o y ) ) = ( A .o suc y ) ) )
75 74 adantrd 
 |-  ( y e. _om -> ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> ( A +o ( A .o y ) ) = ( A .o suc y ) ) )
76 75 imp 
 |-  ( ( y e. _om /\ ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) ) -> ( A +o ( A .o y ) ) = ( A .o suc y ) )
77 76 adantr 
 |-  ( ( ( y e. _om /\ ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) ) /\ ( A .o y ) C_ B ) -> ( A +o ( A .o y ) ) = ( A .o suc y ) )
78 simpr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> ( A +o B ) = B )
79 78 adantl 
 |-  ( ( y e. _om /\ ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) ) -> ( A +o B ) = B )
80 79 adantr 
 |-  ( ( ( y e. _om /\ ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) ) /\ ( A .o y ) C_ B ) -> ( A +o B ) = B )
81 56 77 80 3sstr3d 
 |-  ( ( ( y e. _om /\ ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) ) /\ ( A .o y ) C_ B ) -> ( A .o suc y ) C_ B )
82 81 exp31 
 |-  ( y e. _om -> ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> ( ( A .o y ) C_ B -> ( A .o suc y ) C_ B ) ) )
83 35 37 39 43 82 finds2 
 |-  ( x e. _om -> ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> ( A .o x ) C_ B ) )
84 83 com12 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> ( x e. _om -> ( A .o x ) C_ B ) )
85 84 ralrimiv 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> A. x e. _om ( A .o x ) C_ B )
86 iunss 
 |-  ( U_ x e. _om ( A .o x ) C_ B <-> A. x e. _om ( A .o x ) C_ B )
87 85 86 sylibr 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> U_ x e. _om ( A .o x ) C_ B )
88 33 87 eqsstrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A +o B ) = B ) -> ( A .o _om ) C_ B )
89 88 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = B -> ( A .o _om ) C_ B ) )
90 29 89 impbid 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o _om ) C_ B <-> ( A +o B ) = B ) )