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 𝐵 ) = 𝐵 ) )