omcl2

Description: Closure law for ordinal multiplication. (Contributed by RP, 12-Jan-2025)

		Ref	Expression
	Assertion	omcl2	$⊢ ((A \in C \land B \in C) \land (C = \emptyset \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On))) \to A \cdot_{𝑜} 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 \cdot_{𝑜} B \in C$
4	1 3	biimtrdi	$⊢ C = \emptyset \to (A \in C \to A \cdot_{𝑜} B \in C)$
5	4	com12	$⊢ A \in C \to (C = \emptyset \to A \cdot_{𝑜} B \in C)$
6	5	adantr	$⊢ (A \in C \land B \in C) \to (C = \emptyset \to A \cdot_{𝑜} B \in C)$
7		simpl	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to C = ω ↑_{𝑜} (ω ↑_{𝑜} D)$
8		omelon	$⊢ ω \in On$
9		oecl	$⊢ (ω \in On \land D \in On) \to ω ↑_{𝑜} D \in On$
10	8 9	mpan	$⊢ D \in On \to ω ↑_{𝑜} D \in On$
11	10 8	jctil	$⊢ 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	$⊢ D \in On \to ω ↑_{𝑜} (ω ↑_{𝑜} D) \in On$
14	13	adantl	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to ω ↑_{𝑜} (ω ↑_{𝑜} D) \in On$
15	7 14	eqeltrd	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to C \in On$
16		simpll	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to A \in C$
17		onelon	$⊢ (C \in On \land A \in C) \to A \in On$
18	15 16 17	syl2an2	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to A \in On$
19		on0eqel	$⊢ A \in On \to (A = \emptyset \lor \emptyset \in A)$
20	18 19	syl	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to (A = \emptyset \lor \emptyset \in A)$
21		oveq1	$⊢ A = \emptyset \to A \cdot_{𝑜} B = \emptyset \cdot_{𝑜} B$
22		simpr	$⊢ (A \in C \land B \in C) \to B \in C$
23	22	adantr	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to B \in C$
24		onelon	$⊢ (C \in On \land B \in C) \to B \in On$
25	15 23 24	syl2an2	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to B \in On$
26		om0r	$⊢ B \in On \to \emptyset \cdot_{𝑜} B = \emptyset$
27	25 26	syl	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to \emptyset \cdot_{𝑜} B = \emptyset$
28	21 27	sylan9eqr	$⊢ (((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \land A = \emptyset) \to A \cdot_{𝑜} B = \emptyset$
29		peano1	$⊢ \emptyset \in ω$
30		oen0	$⊢ ((ω \in On \land ω ↑_{𝑜} D \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} (ω ↑_{𝑜} D))$
31	11 29 30	sylancl	$⊢ D \in On \to \emptyset \in (ω ↑_{𝑜} (ω ↑_{𝑜} D))$
32	31	adantl	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to \emptyset \in (ω ↑_{𝑜} (ω ↑_{𝑜} D))$
33	32 7	eleqtrrd	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to \emptyset \in C$
34	33	adantl	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to \emptyset \in C$
35	34	adantr	$⊢ (((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \land A = \emptyset) \to \emptyset \in C$
36	28 35	eqeltrd	$⊢ (((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \land A = \emptyset) \to A \cdot_{𝑜} B \in C$
37	36	ex	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to (A = \emptyset \to A \cdot_{𝑜} B \in C)$
38		simp1	$⊢ (A \in C \land B \in C \land \emptyset \in A) \to A \in C$
39	15	adantl	$⊢ ((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to C \in On$
40		simpr	$⊢ (((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \land C \in On) \to C \in On$
41	38	ad2antrr	$⊢ (((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \land C \in On) \to A \in C$
42	40 41 17	syl2anc	$⊢ (((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \land C \in On) \to A \in On$
43	42	ex	$⊢ ((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to (C \in On \to A \in On)$
44	39 43	jcai	$⊢ ((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to (C \in On \land A \in On)$
45		simpl3	$⊢ ((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to \emptyset \in A$
46		simpl2	$⊢ ((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to B \in C$
47		omordi	$⊢ ((C \in On \land A \in On) \land \emptyset \in A) \to (B \in C \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} C))$
48	47	imp	$⊢ (((C \in On \land A \in On) \land \emptyset \in A) \land B \in C) \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} C)$
49	44 45 46 48	syl21anc	$⊢ ((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} C)$
50		oveq1	$⊢ x = A \to x \cdot_{𝑜} C = A \cdot_{𝑜} C$
51	50	eliuni	$⊢ (A \in C \land A \cdot_{𝑜} B \in (A \cdot_{𝑜} C)) \to A \cdot_{𝑜} B \in ⋃_{x \in C} (x \cdot_{𝑜} C)$
52	38 49 51	syl2an2r	$⊢ ((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to A \cdot_{𝑜} B \in ⋃_{x \in C} (x \cdot_{𝑜} C)$
53		simpr	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land x = \emptyset) \to x = \emptyset$
54	53	oveq1d	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land x = \emptyset) \to x \cdot_{𝑜} C = \emptyset \cdot_{𝑜} C$
55		om0r	$⊢ C \in On \to \emptyset \cdot_{𝑜} C = \emptyset$
56	15 55	syl	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to \emptyset \cdot_{𝑜} C = \emptyset$
57	56	ad2antrr	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land x = \emptyset) \to \emptyset \cdot_{𝑜} C = \emptyset$
58	54 57	eqtrd	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land x = \emptyset) \to x \cdot_{𝑜} C = \emptyset$
59		0ss	$⊢ \emptyset \subseteq C$
60	59	a1i	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land x = \emptyset) \to \emptyset \subseteq C$
61	58 60	eqsstrd	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land x = \emptyset) \to x \cdot_{𝑜} C \subseteq C$
62		id	$⊢ (x \in C \land \emptyset \in x) \to (x \in C \land \emptyset \in x)$
63	62	adantll	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land \emptyset \in x) \to (x \in C \land \emptyset \in x)$
64		simpll	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land \emptyset \in x) \to (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)$
65	64	3mix3d	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land \emptyset \in x) \to (C = \emptyset \lor C = 2_{𝑜} \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On))$
66		omabs2	$⊢ ((x \in C \land \emptyset \in x) \land (C = \emptyset \lor C = 2_{𝑜} \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On))) \to x \cdot_{𝑜} C = C$
67	63 65 66	syl2anc	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land \emptyset \in x) \to x \cdot_{𝑜} C = C$
68		ssidd	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land \emptyset \in x) \to C \subseteq C$
69	67 68	eqsstrd	$⊢ (((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \land \emptyset \in x) \to x \cdot_{𝑜} C \subseteq C$
70		onelon	$⊢ (C \in On \land x \in C) \to x \in On$
71	15 70	sylan	$⊢ ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \to x \in On$
72		on0eqel	$⊢ x \in On \to (x = \emptyset \lor \emptyset \in x)$
73	71 72	syl	$⊢ ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \to (x = \emptyset \lor \emptyset \in x)$
74	61 69 73	mpjaodan	$⊢ ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x \in C) \to x \cdot_{𝑜} C \subseteq C$
75	74	iunssd	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to ⋃_{x \in C} (x \cdot_{𝑜} C) \subseteq C$
76		simpr	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to D \in On$
77	76 8	jctil	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to (ω \in On \land D \in On)$
78		oen0	$⊢ ((ω \in On \land D \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} D)$
79	77 29 78	sylancl	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to \emptyset \in (ω ↑_{𝑜} D)$
80	77 9	syl	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to ω ↑_{𝑜} D \in On$
81		1onn	$⊢ 1_{𝑜} \in ω$
82		ondif2	$⊢ ω \in (On ∖ 2_{𝑜}) \leftrightarrow (ω \in On \land 1_{𝑜} \in ω)$
83	8 81 82	mpbir2an	$⊢ ω \in (On ∖ 2_{𝑜})$
84		oeordi	$⊢ (ω ↑_{𝑜} D \in On \land ω \in (On ∖ 2_{𝑜})) \to (\emptyset \in (ω ↑_{𝑜} D) \to ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} (ω ↑_{𝑜} D)))$
85	80 83 84	sylancl	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to (\emptyset \in (ω ↑_{𝑜} D) \to ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} (ω ↑_{𝑜} D)))$
86	79 85	mpd	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to ω ↑_{𝑜} \emptyset \in (ω ↑_{𝑜} (ω ↑_{𝑜} D))$
87		oe0	$⊢ ω \in On \to ω ↑_{𝑜} \emptyset = 1_{𝑜}$
88	8 87	ax-mp	$⊢ ω ↑_{𝑜} \emptyset = 1_{𝑜}$
89	88	eqcomi	$⊢ 1_{𝑜} = ω ↑_{𝑜} \emptyset$
90	89	a1i	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to 1_{𝑜} = ω ↑_{𝑜} \emptyset$
91	86 90 7	3eltr4d	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to 1_{𝑜} \in C$
92		oveq1	$⊢ x = 1_{𝑜} \to x \cdot_{𝑜} C = 1_{𝑜} \cdot_{𝑜} C$
93		om1r	$⊢ C \in On \to 1_{𝑜} \cdot_{𝑜} C = C$
94	15 93	syl	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to 1_{𝑜} \cdot_{𝑜} C = C$
95	92 94	sylan9eqr	$⊢ ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x = 1_{𝑜}) \to x \cdot_{𝑜} C = C$
96	95	sseq2d	$⊢ ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \land x = 1_{𝑜}) \to (C \subseteq x \cdot_{𝑜} C \leftrightarrow C \subseteq C)$
97		ssidd	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to C \subseteq C$
98	91 96 97	rspcedvd	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to \exists x \in C C \subseteq x \cdot_{𝑜} C$
99		ssiun	$⊢ \exists x \in C C \subseteq x \cdot_{𝑜} C \to C \subseteq ⋃_{x \in C} (x \cdot_{𝑜} C)$
100	98 99	syl	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to C \subseteq ⋃_{x \in C} (x \cdot_{𝑜} C)$
101	75 100	eqssd	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to ⋃_{x \in C} (x \cdot_{𝑜} C) = C$
102	101	adantl	$⊢ ((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to ⋃_{x \in C} (x \cdot_{𝑜} C) = C$
103	52 102	eleqtrd	$⊢ ((A \in C \land B \in C \land \emptyset \in A) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to A \cdot_{𝑜} B \in C$
104	103	ex	$⊢ (A \in C \land B \in C \land \emptyset \in A) \to ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to A \cdot_{𝑜} B \in C)$
105	104	3expia	$⊢ (A \in C \land B \in C) \to (\emptyset \in A \to ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to A \cdot_{𝑜} B \in C))$
106	105	com23	$⊢ (A \in C \land B \in C) \to ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to (\emptyset \in A \to A \cdot_{𝑜} B \in C))$
107	106	imp	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to (\emptyset \in A \to A \cdot_{𝑜} B \in C)$
108	37 107	jaod	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to ((A = \emptyset \lor \emptyset \in A) \to A \cdot_{𝑜} B \in C)$
109	20 108	mpd	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to A \cdot_{𝑜} B \in C$
110	109	ex	$⊢ (A \in C \land B \in C) \to ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to A \cdot_{𝑜} B \in C)$
111	6 110	jaod	$⊢ (A \in C \land B \in C) \to ((C = \emptyset \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to A \cdot_{𝑜} B \in C)$
112	111	imp	$⊢ ((A \in C \land B \in C) \land (C = \emptyset \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On))) \to A \cdot_{𝑜} B \in C$

Metamath Proof Explorer

Theorem omcl2

Proof