Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝐶 = ∅ → ( 𝐴 ∈ 𝐶 → ( 𝐴 ·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 𝐵 ) ∈ 𝐶 )