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