Metamath Proof Explorer

Theorem omcl2

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

Ref Expression
Assertion omcl2 
|- ( ( ( A e. C /\ B e. C ) /\ ( C = (/) \/ ( C = ( _om ^o ( _om ^o D ) ) /\ D e. On ) ) ) -> ( A .o B ) e. C )

Proof

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