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