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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·o ω ) ⊆ 𝐵 ↔ ( 𝐴 +o 𝐵 ) = 𝐵 ) )

Proof

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