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