Metamath Proof Explorer

Theorem oacl2g

Description: Closure law for ordinal addition. Here we show that ordinal addition is closed within the empty set or any ordinal power of omega. (Contributed by RP, 5-Jan-2025)

Ref Expression
Assertion oacl2g 
|- ( ( ( A e. C /\ B e. C ) /\ ( C = (/) \/ ( C = ( _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 biimtrdi 
 |-  ( 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 
 |-  ( ( A e. C /\ B e. C ) -> A e. C )
8 simpl 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> C = ( _om ^o D ) )
9 simpr 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> D e. On )
10 omelon 
 |-  _om e. On
11 9 10 jctil 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> ( _om e. On /\ D e. On ) )
12 oecl 
 |-  ( ( _om e. On /\ D e. On ) -> ( _om ^o D ) e. On )
13 11 12 syl 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> ( _om ^o D ) e. On )
14 8 13 eqeltrd 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> C e. On )
15 14 adantl 
 |-  ( ( ( A e. C /\ B e. C ) /\ ( C = ( _om ^o D ) /\ D e. On ) ) -> C e. On )
16 onelon 
 |-  ( ( C e. On /\ A e. C ) -> A e. On )
17 16 expcom 
 |-  ( A e. C -> ( C e. On -> A e. On ) )
18 17 adantr 
 |-  ( ( A e. C /\ B e. C ) -> ( C e. On -> A e. On ) )
19 18 adantr 
 |-  ( ( ( A e. C /\ B e. C ) /\ ( C = ( _om ^o D ) /\ D e. On ) ) -> ( C e. On -> A e. On ) )
20 15 19 jcai 
 |-  ( ( ( A e. C /\ B e. C ) /\ ( C = ( _om ^o D ) /\ D e. On ) ) -> ( C e. On /\ A e. On ) )
21 simpr 
 |-  ( ( A e. C /\ B e. C ) -> B e. C )
22 21 adantr 
 |-  ( ( ( A e. C /\ B e. C ) /\ ( C = ( _om ^o D ) /\ D e. On ) ) -> B e. C )
23 oaordi 
 |-  ( ( C e. On /\ A e. On ) -> ( B e. C -> ( A +o B ) e. ( A +o C ) ) )
24 20 22 23 sylc 
 |-  ( ( ( A e. C /\ B e. C ) /\ ( C = ( _om ^o D ) /\ D e. On ) ) -> ( A +o B ) e. ( A +o C ) )
25 oveq1 
 |-  ( x = A -> ( x +o C ) = ( A +o C ) )
26 25 eliuni 
 |-  ( ( A e. C /\ ( A +o B ) e. ( A +o C ) ) -> ( A +o B ) e. U_ x e. C ( x +o C ) )
27 7 24 26 syl2an2r 
 |-  ( ( ( A e. C /\ B e. C ) /\ ( C = ( _om ^o D ) /\ D e. On ) ) -> ( A +o B ) e. U_ x e. C ( x +o C ) )
28 simpr 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x e. C ) -> x e. C )
29 8 adantr 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x e. C ) -> C = ( _om ^o D ) )
30 28 29 eleqtrd 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x e. C ) -> x e. ( _om ^o D ) )
31 14 adantr 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x e. C ) -> C e. On )
32 8 eqcomd 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> ( _om ^o D ) = C )
33 ssid 
 |-  C C_ C
34 32 33 eqsstrdi 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> ( _om ^o D ) C_ C )
35 34 adantr 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x e. C ) -> ( _om ^o D ) C_ C )
36 oaabs2 
 |-  ( ( ( x e. ( _om ^o D ) /\ C e. On ) /\ ( _om ^o D ) C_ C ) -> ( x +o C ) = C )
37 30 31 35 36 syl21anc 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x e. C ) -> ( x +o C ) = C )
38 37 33 eqsstrdi 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x e. C ) -> ( x +o C ) C_ C )
39 38 iunssd 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> U_ x e. C ( x +o C ) C_ C )
40 peano1 
 |-  (/) e. _om
41 oen0 
 |-  ( ( ( _om e. On /\ D e. On ) /\ (/) e. _om ) -> (/) e. ( _om ^o D ) )
42 11 40 41 sylancl 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> (/) e. ( _om ^o D ) )
43 42 32 eleqtrd 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> (/) e. C )
44 simpr 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x = (/) ) -> x = (/) )
45 44 oveq1d 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x = (/) ) -> ( x +o C ) = ( (/) +o C ) )
46 oa0r 
 |-  ( C e. On -> ( (/) +o C ) = C )
47 14 46 syl 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> ( (/) +o C ) = C )
48 47 adantr 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x = (/) ) -> ( (/) +o C ) = C )
49 45 48 eqtrd 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x = (/) ) -> ( x +o C ) = C )
50 49 sseq2d 
 |-  ( ( ( C = ( _om ^o D ) /\ D e. On ) /\ x = (/) ) -> ( C C_ ( x +o C ) <-> C C_ C ) )
51 ssidd 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> C C_ C )
52 43 50 51 rspcedvd 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> E. x e. C C C_ ( x +o C ) )
53 ssiun 
 |-  ( E. x e. C C C_ ( x +o C ) -> C C_ U_ x e. C ( x +o C ) )
54 52 53 syl 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> C C_ U_ x e. C ( x +o C ) )
55 39 54 eqssd 
 |-  ( ( C = ( _om ^o D ) /\ D e. On ) -> U_ x e. C ( x +o C ) = C )
56 55 adantl 
 |-  ( ( ( A e. C /\ B e. C ) /\ ( C = ( _om ^o D ) /\ D e. On ) ) -> U_ x e. C ( x +o C ) = C )
57 27 56 eleqtrd 
 |-  ( ( ( A e. C /\ B e. C ) /\ ( C = ( _om ^o D ) /\ D e. On ) ) -> ( A +o B ) e. C )
58 57 ex 
 |-  ( ( A e. C /\ B e. C ) -> ( ( C = ( _om ^o D ) /\ D e. On ) -> ( A +o B ) e. C ) )
59 6 58 jaod 
 |-  ( ( A e. C /\ B e. C ) -> ( ( C = (/) \/ ( C = ( _om ^o D ) /\ D e. On ) ) -> ( A +o B ) e. C ) )
60 59 imp 
 |-  ( ( ( A e. C /\ B e. C ) /\ ( C = (/) \/ ( C = ( _om ^o D ) /\ D e. On ) ) ) -> ( A +o B ) e. C )