This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsuc2

Description: Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Assertion limsuc2 ⊢ Ord ⁡ A ∧ A = ⋃ A → B ∈ A ↔ suc ⁡ B ∈ A

Proof

Step Hyp Ref Expression
1 ordunisuc2 ⊢ Ord ⁡ A → A = ⋃ A ↔ ∀ x ∈ A suc ⁡ x ∈ A
2 1 biimpa ⊢ Ord ⁡ A ∧ A = ⋃ A → ∀ x ∈ A suc ⁡ x ∈ A
3 suceq ⊢ x = B → suc ⁡ x = suc ⁡ B
4 3 eleq1d ⊢ x = B → suc ⁡ x ∈ A ↔ suc ⁡ B ∈ A
5 4 rspccva ⊢ ∀ x ∈ A suc ⁡ x ∈ A ∧ B ∈ A → suc ⁡ B ∈ A
6 2 5 sylan ⊢ Ord ⁡ A ∧ A = ⋃ A ∧ B ∈ A → suc ⁡ B ∈ A
7 6 ex ⊢ Ord ⁡ A ∧ A = ⋃ A → B ∈ A → suc ⁡ B ∈ 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 8 10 syl ⊢ Ord ⁡ A → suc ⁡ B ∈ A → B ∈ A
12 11 adantr ⊢ Ord ⁡ A ∧ A = ⋃ A → suc ⁡ B ∈ A → B ∈ A
13 7 12 impbid ⊢ Ord ⁡ A ∧ A = ⋃ A → B ∈ A ↔ suc ⁡ B ∈ A