Metamath Proof Explorer


Theorem limsssuc

Description: A class includes a limit ordinal iff the successor of the class includes it. (Contributed by NM, 30-Oct-2003)

Ref Expression
Assertion limsssuc Lim A A B A suc B

Proof

Step Hyp Ref Expression
1 sssucid B suc B
2 sstr2 A B B suc B A suc B
3 1 2 mpi A B A suc B
4 eleq1 x = B x A B A
5 4 biimpcd x A x = B B A
6 limsuc Lim A B A suc B A
7 6 biimpa Lim A B A suc B A
8 limord Lim A Ord A
9 ordelord Ord A B A Ord B
10 8 9 sylan Lim A B A Ord B
11 ordsuc Ord B Ord suc B
12 10 11 sylib Lim A B A Ord suc B
13 ordtri1 Ord A Ord suc B A suc B ¬ suc B A
14 8 12 13 syl2an2r Lim A B A A suc B ¬ suc B A
15 14 con2bid Lim A B A suc B A ¬ A suc B
16 7 15 mpbid Lim A B A ¬ A suc B
17 16 ex Lim A B A ¬ A suc B
18 5 17 sylan9r Lim A x A x = B ¬ A suc B
19 18 con2d Lim A x A A suc B ¬ x = B
20 19 ex Lim A x A A suc B ¬ x = B
21 20 com23 Lim A A suc B x A ¬ x = B
22 21 imp31 Lim A A suc B x A ¬ x = B
23 ssel2 A suc B x A x suc B
24 vex x V
25 24 elsuc x suc B x B x = B
26 23 25 sylib A suc B x A x B x = B
27 26 ord A suc B x A ¬ x B x = B
28 27 con1d A suc B x A ¬ x = B x B
29 28 adantll Lim A A suc B x A ¬ x = B x B
30 22 29 mpd Lim A A suc B x A x B
31 30 ex Lim A A suc B x A x B
32 31 ssrdv Lim A A suc B A B
33 32 ex Lim A A suc B A B
34 3 33 impbid2 Lim A A B A suc B