Theorem limnsuc

Description: A limit ordinal is not an element of the class of successor ordinals. Definition 1.11 of Schloeder p. 2. (Contributed by RP, 16-Jan-2025)

	Ref	Expression
Assertion	limnsuc	⊢ ( Lim 𝐴 → ¬ 𝐴 ∈ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } )

Proof

Step	Hyp	Ref	Expression
1		dflim6	⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ ∃ 𝑏 ∈ On 𝐴 = suc 𝑏 ) )
2		simp3	⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ ∃ 𝑏 ∈ On 𝐴 = suc 𝑏 ) → ¬ ∃ 𝑏 ∈ On 𝐴 = suc 𝑏 )
3		eqeq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 = suc 𝑏 ↔ 𝐴 = suc 𝑏 ) )
4	3	rexbidv	⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 ↔ ∃ 𝑏 ∈ On 𝐴 = suc 𝑏 ) )
5	4	elrab	⊢ ( 𝐴 ∈ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } ↔ ( 𝐴 ∈ On ∧ ∃ 𝑏 ∈ On 𝐴 = suc 𝑏 ) )
6	5	simprbi	⊢ ( 𝐴 ∈ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } → ∃ 𝑏 ∈ On 𝐴 = suc 𝑏 )
7	2 6	nsyl	⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ ∃ 𝑏 ∈ On 𝐴 = suc 𝑏 ) → ¬ 𝐴 ∈ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } )
8	1 7	sylbi	⊢ ( Lim 𝐴 → ¬ 𝐴 ∈ { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ On 𝑎 = suc 𝑏 } )