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 syl6bi ⊢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