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 \in On \land B \in On) \to (A \cdot_{𝑜} ω \subseteq B \leftrightarrow A +_{𝑜} B = B)$

Proof

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

Metamath Proof Explorer

Theorem oaabsb

Proof