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 A -> -. A e. { a e. On | E. b e. On a = suc b } )

Proof

Step	Hyp	Ref	Expression
1		dflim6	|- ( Lim A <-> ( Ord A /\ A =/= (/) /\ -. E. b e. On A = suc b ) )
2		simp3	|- ( ( Ord A /\ A =/= (/) /\ -. E. b e. On A = suc b ) -> -. E. b e. On A = suc b )
3		eqeq1	|- ( a = A -> ( a = suc b <-> A = suc b ) )
4	3	rexbidv	|- ( a = A -> ( E. b e. On a = suc b <-> E. b e. On A = suc b ) )
5	4	elrab	|- ( A e. { a e. On | E. b e. On a = suc b } <-> ( A e. On /\ E. b e. On A = suc b ) )
6	5	simprbi	|- ( A e. { a e. On | E. b e. On a = suc b } -> E. b e. On A = suc b )
7	2 6	nsyl	|- ( ( Ord A /\ A =/= (/) /\ -. E. b e. On A = suc b ) -> -. A e. { a e. On | E. b e. On a = suc b } )
8	1 7	sylbi	|- ( Lim A -> -. A e. { a e. On | E. b e. On a = suc b } )