Theorem omcl2

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

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

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝐶 = ∅ → ( 𝐴 ∈ 𝐶 ↔ 𝐴 ∈ ∅ ) )
2		noel	⊢ ¬ 𝐴 ∈ ∅
3	2	pm2.21i	⊢ ( 𝐴 ∈ ∅ → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 )
4	1 3	syl6bi	⊢ ( 𝐶 = ∅ → ( 𝐴 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) )
5	4	com12	⊢ ( 𝐴 ∈ 𝐶 → ( 𝐶 = ∅ → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) )
6	5	adantr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐶 = ∅ → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) )
7		simpl	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) )
8		omelon	⊢ ω ∈ On
9		oecl	⊢ ( ( ω ∈ On ∧ 𝐷 ∈ On ) → ( ω ↑o 𝐷 ) ∈ On )
10	8 9	mpan	⊢ ( 𝐷 ∈ On → ( ω ↑o 𝐷 ) ∈ On )
11	10 8	jctil	⊢ ( 𝐷 ∈ On → ( ω ∈ On ∧ ( ω ↑o 𝐷 ) ∈ On ) )
12		oecl	⊢ ( ( ω ∈ On ∧ ( ω ↑o 𝐷 ) ∈ On ) → ( ω ↑o ( ω ↑o 𝐷 ) ) ∈ On )
13	11 12	syl	⊢ ( 𝐷 ∈ On → ( ω ↑o ( ω ↑o 𝐷 ) ) ∈ On )
14	13	adantl	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( ω ↑o ( ω ↑o 𝐷 ) ) ∈ On )
15	7 14	eqeltrd	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → 𝐶 ∈ On )
16		simpll	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → 𝐴 ∈ 𝐶 )
17		onelon	⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ 𝐶 ) → 𝐴 ∈ On )
18	15 16 17	syl2an2	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → 𝐴 ∈ On )
19		on0eqel	⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
20	18 19	syl	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
21		oveq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ·o 𝐵 ) = ( ∅ ·o 𝐵 ) )
22		simpr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → 𝐵 ∈ 𝐶 )
23	22	adantr	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → 𝐵 ∈ 𝐶 )
24		onelon	⊢ ( ( 𝐶 ∈ On ∧ 𝐵 ∈ 𝐶 ) → 𝐵 ∈ On )
25	15 23 24	syl2an2	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → 𝐵 ∈ On )
26		om0r	⊢ ( 𝐵 ∈ On → ( ∅ ·o 𝐵 ) = ∅ )
27	25 26	syl	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( ∅ ·o 𝐵 ) = ∅ )
28	21 27	sylan9eqr	⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → ( 𝐴 ·o 𝐵 ) = ∅ )
29		peano1	⊢ ∅ ∈ ω
30		oen0	⊢ ( ( ( ω ∈ On ∧ ( ω ↑o 𝐷 ) ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o ( ω ↑o 𝐷 ) ) )
31	11 29 30	sylancl	⊢ ( 𝐷 ∈ On → ∅ ∈ ( ω ↑o ( ω ↑o 𝐷 ) ) )
32	31	adantl	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ∅ ∈ ( ω ↑o ( ω ↑o 𝐷 ) ) )
33	32 7	eleqtrrd	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ∅ ∈ 𝐶 )
34	33	adantl	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ∅ ∈ 𝐶 )
35	34	adantr	⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → ∅ ∈ 𝐶 )
36	28 35	eqeltrd	⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) ∧ 𝐴 = ∅ ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 )
37	36	ex	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 = ∅ → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) )
38		simp1	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) → 𝐴 ∈ 𝐶 )
39	15	adantl	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → 𝐶 ∈ On )
40		simpr	⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ On ) → 𝐶 ∈ On )
41	38	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ On ) → 𝐴 ∈ 𝐶 )
42	40 41 17	syl2anc	⊢ ( ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) ∧ 𝐶 ∈ On ) → 𝐴 ∈ On )
43	42	ex	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( 𝐶 ∈ On → 𝐴 ∈ On ) )
44	39 43	jcai	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) )
45		simpl3	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ∅ ∈ 𝐴 )
46		simpl2	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → 𝐵 ∈ 𝐶 )
47		omordi	⊢ ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )
48	47	imp	⊢ ( ( ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) )
49	44 45 46 48	syl21anc	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) )
50		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ·o 𝐶 ) = ( 𝐴 ·o 𝐶 ) )
51	50	eliuni	⊢ ( ( 𝐴 ∈ 𝐶 ∧ ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) → ( 𝐴 ·o 𝐵 ) ∈ ∪ 𝑥 ∈ 𝐶 ( 𝑥 ·o 𝐶 ) )
52	38 49 51	syl2an2r	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) ∈ ∪ 𝑥 ∈ 𝐶 ( 𝑥 ·o 𝐶 ) )
53		simpr	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 = ∅ ) → 𝑥 = ∅ )
54	53	oveq1d	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 = ∅ ) → ( 𝑥 ·o 𝐶 ) = ( ∅ ·o 𝐶 ) )
55		om0r	⊢ ( 𝐶 ∈ On → ( ∅ ·o 𝐶 ) = ∅ )
56	15 55	syl	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( ∅ ·o 𝐶 ) = ∅ )
57	56	ad2antrr	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 = ∅ ) → ( ∅ ·o 𝐶 ) = ∅ )
58	54 57	eqtrd	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 = ∅ ) → ( 𝑥 ·o 𝐶 ) = ∅ )
59		0ss	⊢ ∅ ⊆ 𝐶
60	59	a1i	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 = ∅ ) → ∅ ⊆ 𝐶 )
61	58 60	eqsstrd	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑥 = ∅ ) → ( 𝑥 ·o 𝐶 ) ⊆ 𝐶 )
62		id	⊢ ( ( 𝑥 ∈ 𝐶 ∧ ∅ ∈ 𝑥 ) → ( 𝑥 ∈ 𝐶 ∧ ∅ ∈ 𝑥 ) )
63	62	adantll	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ ∅ ∈ 𝑥 ) → ( 𝑥 ∈ 𝐶 ∧ ∅ ∈ 𝑥 ) )
64		simpll	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ ∅ ∈ 𝑥 ) → ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) )
65	64	3mix3d	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ ∅ ∈ 𝑥 ) → ( 𝐶 = ∅ ∨ 𝐶 = 2o ∨ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) )
66		omabs2	⊢ ( ( ( 𝑥 ∈ 𝐶 ∧ ∅ ∈ 𝑥 ) ∧ ( 𝐶 = ∅ ∨ 𝐶 = 2o ∨ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) ) → ( 𝑥 ·o 𝐶 ) = 𝐶 )
67	63 65 66	syl2anc	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ ∅ ∈ 𝑥 ) → ( 𝑥 ·o 𝐶 ) = 𝐶 )
68		ssidd	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ ∅ ∈ 𝑥 ) → 𝐶 ⊆ 𝐶 )
69	67 68	eqsstrd	⊢ ( ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) ∧ ∅ ∈ 𝑥 ) → ( 𝑥 ·o 𝐶 ) ⊆ 𝐶 )
70		onelon	⊢ ( ( 𝐶 ∈ On ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ On )
71	15 70	sylan	⊢ ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ On )
72		on0eqel	⊢ ( 𝑥 ∈ On → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
73	71 72	syl	⊢ ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 = ∅ ∨ ∅ ∈ 𝑥 ) )
74	61 69 73	mpjaodan	⊢ ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 ·o 𝐶 ) ⊆ 𝐶 )
75	74	iunssd	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ∪ 𝑥 ∈ 𝐶 ( 𝑥 ·o 𝐶 ) ⊆ 𝐶 )
76		simpr	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → 𝐷 ∈ On )
77	76 8	jctil	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( ω ∈ On ∧ 𝐷 ∈ On ) )
78		oen0	⊢ ( ( ( ω ∈ On ∧ 𝐷 ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 𝐷 ) )
79	77 29 78	sylancl	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ∅ ∈ ( ω ↑o 𝐷 ) )
80	77 9	syl	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( ω ↑o 𝐷 ) ∈ On )
81		1onn	⊢ 1o ∈ ω
82		ondif2	⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
83	8 81 82	mpbir2an	⊢ ω ∈ ( On ∖ 2o )
84		oeordi	⊢ ( ( ( ω ↑o 𝐷 ) ∈ On ∧ ω ∈ ( On ∖ 2o ) ) → ( ∅ ∈ ( ω ↑o 𝐷 ) → ( ω ↑o ∅ ) ∈ ( ω ↑o ( ω ↑o 𝐷 ) ) ) )
85	80 83 84	sylancl	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( ∅ ∈ ( ω ↑o 𝐷 ) → ( ω ↑o ∅ ) ∈ ( ω ↑o ( ω ↑o 𝐷 ) ) ) )
86	79 85	mpd	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( ω ↑o ∅ ) ∈ ( ω ↑o ( ω ↑o 𝐷 ) ) )
87		oe0	⊢ ( ω ∈ On → ( ω ↑o ∅ ) = 1o )
88	8 87	ax-mp	⊢ ( ω ↑o ∅ ) = 1o
89	88	eqcomi	⊢ 1o = ( ω ↑o ∅ )
90	89	a1i	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → 1o = ( ω ↑o ∅ ) )
91	86 90 7	3eltr4d	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → 1o ∈ 𝐶 )
92		oveq1	⊢ ( 𝑥 = 1o → ( 𝑥 ·o 𝐶 ) = ( 1o ·o 𝐶 ) )
93		om1r	⊢ ( 𝐶 ∈ On → ( 1o ·o 𝐶 ) = 𝐶 )
94	15 93	syl	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( 1o ·o 𝐶 ) = 𝐶 )
95	92 94	sylan9eqr	⊢ ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 = 1o ) → ( 𝑥 ·o 𝐶 ) = 𝐶 )
96	95	sseq2d	⊢ ( ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ∧ 𝑥 = 1o ) → ( 𝐶 ⊆ ( 𝑥 ·o 𝐶 ) ↔ 𝐶 ⊆ 𝐶 ) )
97		ssidd	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → 𝐶 ⊆ 𝐶 )
98	91 96 97	rspcedvd	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ∃ 𝑥 ∈ 𝐶 𝐶 ⊆ ( 𝑥 ·o 𝐶 ) )
99		ssiun	⊢ ( ∃ 𝑥 ∈ 𝐶 𝐶 ⊆ ( 𝑥 ·o 𝐶 ) → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐶 ( 𝑥 ·o 𝐶 ) )
100	98 99	syl	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐶 ( 𝑥 ·o 𝐶 ) )
101	75 100	eqssd	⊢ ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ∪ 𝑥 ∈ 𝐶 ( 𝑥 ·o 𝐶 ) = 𝐶 )
102	101	adantl	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ∪ 𝑥 ∈ 𝐶 ( 𝑥 ·o 𝐶 ) = 𝐶 )
103	52 102	eleqtrd	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 )
104	103	ex	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) → ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) )
105	104	3expia	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ∅ ∈ 𝐴 → ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) ) )
106	105	com23	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( ∅ ∈ 𝐴 → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) ) )
107	106	imp	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( ∅ ∈ 𝐴 → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) )
108	37 107	jaod	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) )
109	20 108	mpd	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 )
110	109	ex	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) )
111	6 110	jaod	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐶 = ∅ ∨ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 ) )
112	111	imp	⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ∅ ∨ ( 𝐶 = ( ω ↑o ( ω ↑o 𝐷 ) ) ∧ 𝐷 ∈ On ) ) ) → ( 𝐴 ·o 𝐵 ) ∈ 𝐶 )