Theorem onsucuni3

Description: If an ordinal number has a predecessor, then it is successor of that predecessor. (Contributed by ML, 17-Oct-2020)

	Ref	Expression
Assertion	onsucuni3	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> B = suc U. B )

Proof

Step	Hyp	Ref	Expression
1		eloni	|- ( B e. On -> Ord B )
2	1	3ad2ant1	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> Ord B )
3		orduniorsuc	|- ( Ord B -> ( B = U. B \/ B = suc U. B ) )
4	2 3	syl	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> ( B = U. B \/ B = suc U. B ) )
5	4	orcomd	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> ( B = suc U. B \/ B = U. B ) )
6		simp2	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> B =/= (/) )
7		df-lim	|- ( Lim B <-> ( Ord B /\ B =/= (/) /\ B = U. B ) )
8	7	biimpri	|- ( ( Ord B /\ B =/= (/) /\ B = U. B ) -> Lim B )
9	8	3expb	|- ( ( Ord B /\ ( B =/= (/) /\ B = U. B ) ) -> Lim B )
10	9	con3i	|- ( -. Lim B -> -. ( Ord B /\ ( B =/= (/) /\ B = U. B ) ) )
11	10	3ad2ant3	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> -. ( Ord B /\ ( B =/= (/) /\ B = U. B ) ) )
12	2 11	mpnanrd	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> -. ( B =/= (/) /\ B = U. B ) )
13	6 12	mpnanrd	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> -. B = U. B )
14		orcom	|- ( ( B = suc U. B \/ B = U. B ) <-> ( B = U. B \/ B = suc U. B ) )
15		df-or	|- ( ( B = U. B \/ B = suc U. B ) <-> ( -. B = U. B -> B = suc U. B ) )
16	14 15	sylbb	|- ( ( B = suc U. B \/ B = U. B ) -> ( -. B = U. B -> B = suc U. B ) )
17	5 13 16	sylc	|- ( ( B e. On /\ B =/= (/) /\ -. Lim B ) -> B = suc U. B )