omcl3g

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

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

Proof

Step	Hyp	Ref	Expression
1		eltpi	$⊢ C \in \{\emptyset, 1_{𝑜}, 2_{𝑜}\} \to (C = \emptyset \lor C = 1_{𝑜} \lor C = 2_{𝑜})$
2		df-3o	$⊢ 3_{𝑜} = suc 2_{𝑜}$
3		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
4	3	uneq1i	$⊢ 2_{𝑜} \cup \{2_{𝑜}\} = \{\emptyset, 1_{𝑜}\} \cup \{2_{𝑜}\}$
5		df-suc	$⊢ suc 2_{𝑜} = 2_{𝑜} \cup \{2_{𝑜}\}$
6		df-tp	$⊢ \{\emptyset, 1_{𝑜}, 2_{𝑜}\} = \{\emptyset, 1_{𝑜}\} \cup \{2_{𝑜}\}$
7	4 5 6	3eqtr4i	$⊢ suc 2_{𝑜} = \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
8	2 7	eqtri	$⊢ 3_{𝑜} = \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
9	1 8	eleq2s	$⊢ C \in 3_{𝑜} \to (C = \emptyset \lor C = 1_{𝑜} \lor C = 2_{𝑜})$
10		orc	$⊢ C = \emptyset \to (C = \emptyset \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On))$
11		omcl2	$⊢ ((A \in C \land B \in C) \land (C = \emptyset \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} C) \land C \in On))) \to A \cdot_{𝑜} B \in C$
12	10 11	sylan2	$⊢ ((A \in C \land B \in C) \land C = \emptyset) \to A \cdot_{𝑜} B \in C$
13	12	ex	$⊢ (A \in C \land B \in C) \to (C = \emptyset \to A \cdot_{𝑜} B \in C)$
14		el1o	$⊢ A \in 1_{𝑜} \leftrightarrow A = \emptyset$
15		el1o	$⊢ B \in 1_{𝑜} \leftrightarrow B = \emptyset$
16		oveq12	$⊢ (A = \emptyset \land B = \emptyset) \to A \cdot_{𝑜} B = \emptyset \cdot_{𝑜} \emptyset$
17		0elon	$⊢ \emptyset \in On$
18		om0	$⊢ \emptyset \in On \to \emptyset \cdot_{𝑜} \emptyset = \emptyset$
19	17 18	ax-mp	$⊢ \emptyset \cdot_{𝑜} \emptyset = \emptyset$
20		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
21	19 20	eqeltri	$⊢ \emptyset \cdot_{𝑜} \emptyset \in 1_{𝑜}$
22	16 21	eqeltrdi	$⊢ (A = \emptyset \land B = \emptyset) \to A \cdot_{𝑜} B \in 1_{𝑜}$
23	14 15 22	syl2anb	$⊢ (A \in 1_{𝑜} \land B \in 1_{𝑜}) \to A \cdot_{𝑜} B \in 1_{𝑜}$
24	23	a1i	$⊢ C = 1_{𝑜} \to ((A \in 1_{𝑜} \land B \in 1_{𝑜}) \to A \cdot_{𝑜} B \in 1_{𝑜})$
25		eleq2	$⊢ C = 1_{𝑜} \to (A \in C \leftrightarrow A \in 1_{𝑜})$
26		eleq2	$⊢ C = 1_{𝑜} \to (B \in C \leftrightarrow B \in 1_{𝑜})$
27	25 26	anbi12d	$⊢ C = 1_{𝑜} \to ((A \in C \land B \in C) \leftrightarrow (A \in 1_{𝑜} \land B \in 1_{𝑜}))$
28		eleq2	$⊢ C = 1_{𝑜} \to (A \cdot_{𝑜} B \in C \leftrightarrow A \cdot_{𝑜} B \in 1_{𝑜})$
29	24 27 28	3imtr4d	$⊢ C = 1_{𝑜} \to ((A \in C \land B \in C) \to A \cdot_{𝑜} B \in C)$
30	29	com12	$⊢ (A \in C \land B \in C) \to (C = 1_{𝑜} \to A \cdot_{𝑜} B \in C)$
31		elpri	$⊢ A \in \{\emptyset, 1_{𝑜}\} \to (A = \emptyset \lor A = 1_{𝑜})$
32	31 3	eleq2s	$⊢ A \in 2_{𝑜} \to (A = \emptyset \lor A = 1_{𝑜})$
33		elpri	$⊢ B \in \{\emptyset, 1_{𝑜}\} \to (B = \emptyset \lor B = 1_{𝑜})$
34	33 3	eleq2s	$⊢ B \in 2_{𝑜} \to (B = \emptyset \lor B = 1_{𝑜})$
35		0ex	$⊢ \emptyset \in V$
36	35	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
37	36 19 3	3eltr4i	$⊢ \emptyset \cdot_{𝑜} \emptyset \in 2_{𝑜}$
38	16 37	eqeltrdi	$⊢ (A = \emptyset \land B = \emptyset) \to A \cdot_{𝑜} B \in 2_{𝑜}$
39		oveq12	$⊢ (A = 1_{𝑜} \land B = \emptyset) \to A \cdot_{𝑜} B = 1_{𝑜} \cdot_{𝑜} \emptyset$
40		1on	$⊢ 1_{𝑜} \in On$
41		om0	$⊢ 1_{𝑜} \in On \to 1_{𝑜} \cdot_{𝑜} \emptyset = \emptyset$
42	40 41	ax-mp	$⊢ 1_{𝑜} \cdot_{𝑜} \emptyset = \emptyset$
43	36 42 3	3eltr4i	$⊢ 1_{𝑜} \cdot_{𝑜} \emptyset \in 2_{𝑜}$
44	39 43	eqeltrdi	$⊢ (A = 1_{𝑜} \land B = \emptyset) \to A \cdot_{𝑜} B \in 2_{𝑜}$
45		oveq12	$⊢ (A = \emptyset \land B = 1_{𝑜}) \to A \cdot_{𝑜} B = \emptyset \cdot_{𝑜} 1_{𝑜}$
46		om0r	$⊢ 1_{𝑜} \in On \to \emptyset \cdot_{𝑜} 1_{𝑜} = \emptyset$
47	40 46	ax-mp	$⊢ \emptyset \cdot_{𝑜} 1_{𝑜} = \emptyset$
48	36 47 3	3eltr4i	$⊢ \emptyset \cdot_{𝑜} 1_{𝑜} \in 2_{𝑜}$
49	45 48	eqeltrdi	$⊢ (A = \emptyset \land B = 1_{𝑜}) \to A \cdot_{𝑜} B \in 2_{𝑜}$
50		oveq12	$⊢ (A = 1_{𝑜} \land B = 1_{𝑜}) \to A \cdot_{𝑜} B = 1_{𝑜} \cdot_{𝑜} 1_{𝑜}$
51		1oex	$⊢ 1_{𝑜} \in V$
52	51	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
53		om1	$⊢ 1_{𝑜} \in On \to 1_{𝑜} \cdot_{𝑜} 1_{𝑜} = 1_{𝑜}$
54	40 53	ax-mp	$⊢ 1_{𝑜} \cdot_{𝑜} 1_{𝑜} = 1_{𝑜}$
55	52 54 3	3eltr4i	$⊢ 1_{𝑜} \cdot_{𝑜} 1_{𝑜} \in 2_{𝑜}$
56	50 55	eqeltrdi	$⊢ (A = 1_{𝑜} \land B = 1_{𝑜}) \to A \cdot_{𝑜} B \in 2_{𝑜}$
57	38 44 49 56	ccase	$⊢ ((A = \emptyset \lor A = 1_{𝑜}) \land (B = \emptyset \lor B = 1_{𝑜})) \to A \cdot_{𝑜} B \in 2_{𝑜}$
58	32 34 57	syl2an	$⊢ (A \in 2_{𝑜} \land B \in 2_{𝑜}) \to A \cdot_{𝑜} B \in 2_{𝑜}$
59	58	a1i	$⊢ C = 2_{𝑜} \to ((A \in 2_{𝑜} \land B \in 2_{𝑜}) \to A \cdot_{𝑜} B \in 2_{𝑜})$
60		eleq2	$⊢ C = 2_{𝑜} \to (A \in C \leftrightarrow A \in 2_{𝑜})$
61		eleq2	$⊢ C = 2_{𝑜} \to (B \in C \leftrightarrow B \in 2_{𝑜})$
62	60 61	anbi12d	$⊢ C = 2_{𝑜} \to ((A \in C \land B \in C) \leftrightarrow (A \in 2_{𝑜} \land B \in 2_{𝑜}))$
63		eleq2	$⊢ C = 2_{𝑜} \to (A \cdot_{𝑜} B \in C \leftrightarrow A \cdot_{𝑜} B \in 2_{𝑜})$
64	59 62 63	3imtr4d	$⊢ C = 2_{𝑜} \to ((A \in C \land B \in C) \to A \cdot_{𝑜} B \in C)$
65	64	com12	$⊢ (A \in C \land B \in C) \to (C = 2_{𝑜} \to A \cdot_{𝑜} B \in C)$
66	13 30 65	3jaod	$⊢ (A \in C \land B \in C) \to ((C = \emptyset \lor C = 1_{𝑜} \lor C = 2_{𝑜}) \to A \cdot_{𝑜} B \in C)$
67	9 66	syl5	$⊢ (A \in C \land B \in C) \to (C \in 3_{𝑜} \to A \cdot_{𝑜} B \in C)$
68		olc	$⊢ (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to (C = \emptyset \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On))$
69		omcl2	$⊢ ((A \in C \land B \in C) \land (C = \emptyset \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On))) \to A \cdot_{𝑜} B \in C$
70	68 69	sylan2	$⊢ ((A \in C \land B \in C) \land (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to A \cdot_{𝑜} B \in C$
71	70	ex	$⊢ (A \in C \land B \in C) \to ((C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On) \to A \cdot_{𝑜} B \in C)$
72	67 71	jaod	$⊢ (A \in C \land B \in C) \to ((C \in 3_{𝑜} \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On)) \to A \cdot_{𝑜} B \in C)$
73	72	imp	$⊢ ((A \in C \land B \in C) \land (C \in 3_{𝑜} \lor (C = ω ↑_{𝑜} (ω ↑_{𝑜} D) \land D \in On))) \to A \cdot_{𝑜} B \in C$

Metamath Proof Explorer

Theorem omcl3g

Proof