Metamath Proof Explorer

Theorem omcl3g

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

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

Proof

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