Theorem omcl3g

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

	Ref	Expression
Assertion	omcl3g	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 ∈ 3o ∨ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 )

Proof

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