Metamath Proof Explorer


Theorem limsuc

Description: The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003)

Ref Expression
Assertion limsuc Lim A B A suc B A

Proof

Step Hyp Ref Expression
1 dflim4 Lim A Ord A A x A suc x A
2 suceq x = B suc x = suc B
3 2 eleq1d x = B suc x A suc B A
4 3 rspccv x A suc x A B A suc B A
5 4 3ad2ant3 Ord A A x A suc x A B A suc B A
6 1 5 sylbi Lim A B A suc B A
7 limord Lim A Ord A
8 ordtr Ord A Tr A
9 trsuc Tr A suc B A B A
10 9 ex Tr A suc B A B A
11 7 8 10 3syl Lim A suc B A B A
12 6 11 impbid Lim A B A suc B A