# 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 ${⊢}\mathrm{Lim}{A}\to \left({A}\subseteq {B}↔{A}\subseteq \mathrm{suc}{B}\right)$

### Proof

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