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 ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ∅ ∨ ( 𝐶 = ( ω ↑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 ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 )
8 simpl ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → 𝐶 = ( ω ↑o 𝐷 ) )
9 simpr ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → 𝐷 ∈ On )
10 omelon ⊢ ω ∈ On
11 9 10 jctil ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ( ω ∈ On ∧ 𝐷 ∈ On ) )
12 oecl ⊢ ( ( ω ∈ On ∧ 𝐷 ∈ On ) → ( ω ↑o 𝐷 ) ∈ On )
13 11 12 syl ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ( ω ↑o 𝐷 ) ∈ On )
14 8 13 eqeltrd ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → 𝐶 ∈ On )
15 14 adantl ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) → 𝐶 ∈ On )
16 onelon ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ 𝐶 ) → 𝐴 ∈ On )
17 16 expcom ⊢ ( 𝐴 ∈ 𝐶 → ( 𝐶 ∈ On → 𝐴 ∈ On ) )
18 17 adantr ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐶 ∈ On → 𝐴 ∈ On ) )
19 18 adantr ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) → ( 𝐶 ∈ On → 𝐴 ∈ On ) )
20 15 19 jcai ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) → ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) )
21 simpr ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → 𝐵 ∈ 𝐶 )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) → 𝐵 ∈ 𝐶 )
23 oaordi ⊢ ( ( 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o 𝐶 ) ) )
24 20 22 23 sylc ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o 𝐶 ) )
25 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 +o 𝐶 ) = ( 𝐴 +o 𝐶 ) )
26 25 eliuni ⊢ ( ( 𝐴 ∈ 𝐶 ∧ ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o 𝐶 ) ) → ( 𝐴 +o 𝐵 ) ∈ ∪ 𝑥 ∈ 𝐶 ( 𝑥 +o 𝐶 ) )
27 7 24 26 syl2an2r ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 +o 𝐵 ) ∈ ∪ 𝑥 ∈ 𝐶 ( 𝑥 +o 𝐶 ) )
28 simpr ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐶 )
29 8 adantr ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → 𝐶 = ( ω ↑o 𝐷 ) )
30 28 29 eleqtrd ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ( ω ↑o 𝐷 ) )
31 14 adantr ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → 𝐶 ∈ On )
32 8 eqcomd ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ( ω ↑o 𝐷 ) = 𝐶 )
33 ssid ⊢ 𝐶 ⊆ 𝐶
34 32 33 eqsstrdi ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ( ω ↑o 𝐷 ) ⊆ 𝐶 )
35 34 adantr ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → ( ω ↑o 𝐷 ) ⊆ 𝐶 )
36 oaabs2 ⊢ ( ( ( 𝑥 ∈ ( ω ↑o 𝐷 ) ∧ 𝐶 ∈ On ) ∧ ( ω ↑o 𝐷 ) ⊆ 𝐶 ) → ( 𝑥 +o 𝐶 ) = 𝐶 )
37 30 31 35 36 syl21anc ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 +o 𝐶 ) = 𝐶 )
38 37 33 eqsstrdi ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 ∈ 𝐶 ) → ( 𝑥 +o 𝐶 ) ⊆ 𝐶 )
39 38 iunssd ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ∪ 𝑥 ∈ 𝐶 ( 𝑥 +o 𝐶 ) ⊆ 𝐶 )
40 peano1 ⊢ ∅ ∈ ω
41 oen0 ⊢ ( ( ( ω ∈ On ∧ 𝐷 ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 𝐷 ) )
42 11 40 41 sylancl ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ∅ ∈ ( ω ↑o 𝐷 ) )
43 42 32 eleqtrd ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ∅ ∈ 𝐶 )
44 simpr ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 = ∅ ) → 𝑥 = ∅ )
45 44 oveq1d ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 = ∅ ) → ( 𝑥 +o 𝐶 ) = ( ∅ +o 𝐶 ) )
46 oa0r ⊢ ( 𝐶 ∈ On → ( ∅ +o 𝐶 ) = 𝐶 )
47 14 46 syl ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ( ∅ +o 𝐶 ) = 𝐶 )
48 47 adantr ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 = ∅ ) → ( ∅ +o 𝐶 ) = 𝐶 )
49 45 48 eqtrd ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 = ∅ ) → ( 𝑥 +o 𝐶 ) = 𝐶 )
50 49 sseq2d ⊢ ( ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ∧ 𝑥 = ∅ ) → ( 𝐶 ⊆ ( 𝑥 +o 𝐶 ) ↔ 𝐶 ⊆ 𝐶 ) )
51 ssidd ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → 𝐶 ⊆ 𝐶 )
52 43 50 51 rspcedvd ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ∃ 𝑥 ∈ 𝐶 𝐶 ⊆ ( 𝑥 +o 𝐶 ) )
53 ssiun ⊢ ( ∃ 𝑥 ∈ 𝐶 𝐶 ⊆ ( 𝑥 +o 𝐶 ) → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐶 ( 𝑥 +o 𝐶 ) )
54 52 53 syl ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → 𝐶 ⊆ ∪ 𝑥 ∈ 𝐶 ( 𝑥 +o 𝐶 ) )
55 39 54 eqssd ⊢ ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ∪ 𝑥 ∈ 𝐶 ( 𝑥 +o 𝐶 ) = 𝐶 )
56 55 adantl ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) → ∪ 𝑥 ∈ 𝐶 ( 𝑥 +o 𝐶 ) = 𝐶 )
57 27 56 eleqtrd ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 +o 𝐵 ) ∈ 𝐶 )
58 57 ex ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ 𝐶 ) )
59 6 58 jaod ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( ( 𝐶 = ∅ ∨ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) → ( 𝐴 +o 𝐵 ) ∈ 𝐶 ) )
60 59 imp ⊢ ( ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) ∧ ( 𝐶 = ∅ ∨ ( 𝐶 = ( ω ↑o 𝐷 ) ∧ 𝐷 ∈ On ) ) ) → ( 𝐴 +o 𝐵 ) ∈ 𝐶 )