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 ∈ On ∧ B ∈ On → A ⋅ 𝑜 ω ⊆ B ↔ A + 𝑜 B = B

Proof

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