Metamath Proof Explorer

Theorem succlg

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

Ref Expression
Assertion succlg ⊢ A ∈ B ∧ B = ∅ ∨ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → suc ⁡ A ∈ B

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ B = ∅ → A ∈ B ↔ A ∈ ∅
2 noel ⊢ ¬ A ∈ ∅
3 2 pm2.21i ⊢ A ∈ ∅ → suc ⁡ A ∈ B
4 1 3 biimtrdi ⊢ B = ∅ → A ∈ B → suc ⁡ A ∈ B
5 4 com12 ⊢ A ∈ B → B = ∅ → suc ⁡ A ∈ B
6 simpl ⊢ A ∈ B ∧ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → A ∈ B
7 eldifi ⊢ C ∈ On ∖ 1 𝑜 → C ∈ On
8 7 ad2antll ⊢ A ∈ B ∧ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → C ∈ On
9 omex ⊢ ω ∈ V
10 limom ⊢ Lim ⁡ ω
11 9 10 pm3.2i ⊢ ω ∈ V ∧ Lim ⁡ ω
12 11 a1i ⊢ A ∈ B ∧ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → ω ∈ V ∧ Lim ⁡ ω
13 ondif1 ⊢ C ∈ On ∖ 1 𝑜 ↔ C ∈ On ∧ ∅ ∈ C
14 13 simprbi ⊢ C ∈ On ∖ 1 𝑜 → ∅ ∈ C
15 14 ad2antll ⊢ A ∈ B ∧ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → ∅ ∈ C
16 omlimcl2 ⊢ C ∈ On ∧ ω ∈ V ∧ Lim ⁡ ω ∧ ∅ ∈ C → Lim ⁡ ω ⋅ 𝑜 C
17 8 12 15 16 syl21anc ⊢ A ∈ B ∧ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → Lim ⁡ ω ⋅ 𝑜 C
18 limeq ⊢ B = ω ⋅ 𝑜 C → Lim ⁡ B ↔ Lim ⁡ ω ⋅ 𝑜 C
19 18 ad2antrl ⊢ A ∈ B ∧ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → Lim ⁡ B ↔ Lim ⁡ ω ⋅ 𝑜 C
20 17 19 mpbird ⊢ A ∈ B ∧ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → Lim ⁡ B
21 limsuc ⊢ Lim ⁡ B → A ∈ B ↔ suc ⁡ A ∈ B
22 20 21 syl ⊢ A ∈ B ∧ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → A ∈ B ↔ suc ⁡ A ∈ B
23 6 22 mpbid ⊢ A ∈ B ∧ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → suc ⁡ A ∈ B
24 23 ex ⊢ A ∈ B → B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → suc ⁡ A ∈ B
25 5 24 jaod ⊢ A ∈ B → B = ∅ ∨ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → suc ⁡ A ∈ B
26 25 imp ⊢ A ∈ B ∧ B = ∅ ∨ B = ω ⋅ 𝑜 C ∧ C ∈ On ∖ 1 𝑜 → suc ⁡ A ∈ B