oacl2g

Description: Closure law for ordinal addition. Here we show that ordinal addition is closed within the empty set or any ordinal power of omega. (Contributed by RP, 5-Jan-2025)

		Ref	Expression
	Assertion	oacl2g	$⊢ ((A \in C \land B \in C) \land (C = \emptyset \lor (C = ω ↑_{𝑜} D \land D \in On))) \to A +_{𝑜} B \in C$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$⊢ C = \emptyset \to (A \in C \leftrightarrow A \in \emptyset)$
2		noel	$⊢ \neg A \in \emptyset$
3	2	pm2.21i	$⊢ A \in \emptyset \to A +_{𝑜} B \in C$
4	1 3	biimtrdi	$⊢ C = \emptyset \to (A \in C \to A +_{𝑜} B \in C)$
5	4	com12	$⊢ A \in C \to (C = \emptyset \to A +_{𝑜} B \in C)$
6	5	adantr	$⊢ (A \in C \land B \in C) \to (C = \emptyset \to A +_{𝑜} B \in C)$
7		simpl	$⊢ (A \in C \land B \in C) \to A \in C$
8		simpl	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to C = ω ↑_{𝑜} D$
9		simpr	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to D \in On$
10		omelon	$⊢ ω \in On$
11	9 10	jctil	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to (ω \in On \land D \in On)$
12		oecl	$⊢ (ω \in On \land D \in On) \to ω ↑_{𝑜} D \in On$
13	11 12	syl	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to ω ↑_{𝑜} D \in On$
14	8 13	eqeltrd	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to C \in On$
15	14	adantl	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} D \land D \in On)) \to C \in On$
16		onelon	$⊢ (C \in On \land A \in C) \to A \in On$
17	16	expcom	$⊢ A \in C \to (C \in On \to A \in On)$
18	17	adantr	$⊢ (A \in C \land B \in C) \to (C \in On \to A \in On)$
19	18	adantr	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} D \land D \in On)) \to (C \in On \to A \in On)$
20	15 19	jcai	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} D \land D \in On)) \to (C \in On \land A \in On)$
21		simpr	$⊢ (A \in C \land B \in C) \to B \in C$
22	21	adantr	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} D \land D \in On)) \to B \in C$
23		oaordi	$⊢ (C \in On \land A \in On) \to (B \in C \to A +_{𝑜} B \in (A +_{𝑜} C))$
24	20 22 23	sylc	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} D \land D \in On)) \to A +_{𝑜} B \in (A +_{𝑜} C)$
25		oveq1	$⊢ x = A \to x +_{𝑜} C = A +_{𝑜} C$
26	25	eliuni	$⊢ (A \in C \land A +_{𝑜} B \in (A +_{𝑜} C)) \to A +_{𝑜} B \in ⋃_{x \in C} (x +_{𝑜} C)$
27	7 24 26	syl2an2r	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} D \land D \in On)) \to A +_{𝑜} B \in ⋃_{x \in C} (x +_{𝑜} C)$
28		simpr	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x \in C) \to x \in C$
29	8	adantr	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x \in C) \to C = ω ↑_{𝑜} D$
30	28 29	eleqtrd	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x \in C) \to x \in (ω ↑_{𝑜} D)$
31	14	adantr	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x \in C) \to C \in On$
32	8	eqcomd	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to ω ↑_{𝑜} D = C$
33		ssid	$⊢ C \subseteq C$
34	32 33	eqsstrdi	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to ω ↑_{𝑜} D \subseteq C$
35	34	adantr	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x \in C) \to ω ↑_{𝑜} D \subseteq C$
36		oaabs2	$⊢ ((x \in (ω ↑_{𝑜} D) \land C \in On) \land ω ↑_{𝑜} D \subseteq C) \to x +_{𝑜} C = C$
37	30 31 35 36	syl21anc	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x \in C) \to x +_{𝑜} C = C$
38	37 33	eqsstrdi	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x \in C) \to x +_{𝑜} C \subseteq C$
39	38	iunssd	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to ⋃_{x \in C} (x +_{𝑜} C) \subseteq C$
40		peano1	$⊢ \emptyset \in ω$
41		oen0	$⊢ ((ω \in On \land D \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} D)$
42	11 40 41	sylancl	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to \emptyset \in (ω ↑_{𝑜} D)$
43	42 32	eleqtrd	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to \emptyset \in C$
44		simpr	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x = \emptyset) \to x = \emptyset$
45	44	oveq1d	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x = \emptyset) \to x +_{𝑜} C = \emptyset +_{𝑜} C$
46		oa0r	$⊢ C \in On \to \emptyset +_{𝑜} C = C$
47	14 46	syl	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to \emptyset +_{𝑜} C = C$
48	47	adantr	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x = \emptyset) \to \emptyset +_{𝑜} C = C$
49	45 48	eqtrd	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x = \emptyset) \to x +_{𝑜} C = C$
50	49	sseq2d	$⊢ ((C = ω ↑_{𝑜} D \land D \in On) \land x = \emptyset) \to (C \subseteq x +_{𝑜} C \leftrightarrow C \subseteq C)$
51		ssidd	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to C \subseteq C$
52	43 50 51	rspcedvd	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to \exists x \in C C \subseteq x +_{𝑜} C$
53		ssiun	$⊢ \exists x \in C C \subseteq x +_{𝑜} C \to C \subseteq ⋃_{x \in C} (x +_{𝑜} C)$
54	52 53	syl	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to C \subseteq ⋃_{x \in C} (x +_{𝑜} C)$
55	39 54	eqssd	$⊢ (C = ω ↑_{𝑜} D \land D \in On) \to ⋃_{x \in C} (x +_{𝑜} C) = C$
56	55	adantl	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} D \land D \in On)) \to ⋃_{x \in C} (x +_{𝑜} C) = C$
57	27 56	eleqtrd	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} D \land D \in On)) \to A +_{𝑜} B \in C$
58	57	ex	$⊢ (A \in C \land B \in C) \to ((C = ω ↑_{𝑜} D \land D \in On) \to A +_{𝑜} B \in C)$
59	6 58	jaod	$⊢ (A \in C \land B \in C) \to ((C = \emptyset \lor (C = ω ↑_{𝑜} D \land D \in On)) \to A +_{𝑜} B \in C)$
60	59	imp	$⊢ ((A \in C \land B \in C) \land (C = \emptyset \lor (C = ω ↑_{𝑜} D \land D \in On))) \to A +_{𝑜} B \in C$

Metamath Proof Explorer

Theorem oacl2g

Proof