Theorem succlg

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

	Ref	Expression
Assertion	succlg	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ( 𝐵 = ∅ ∨ ( 𝐵 = ( ω ·o 𝐶 ) ∧ 𝐶 ∈ ( On ∖ 1o ) ) ) ) → suc 𝐴 ∈ 𝐵 )

Proof

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