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 𝐴 ∧ 𝐴 = ∪ 𝐴 ) → ( 𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ordunisuc2 ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ) )
2 1 biimpa ⊢ ( ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 )
3 suceq ⊢ ( 𝑥 = 𝐵 → suc 𝑥 = suc 𝐵 )
4 3 eleq1d ⊢ ( 𝑥 = 𝐵 → ( suc 𝑥 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴 ) )
5 4 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → suc 𝐵 ∈ 𝐴 )
6 2 5 sylan ⊢ ( ( ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) ∧ 𝐵 ∈ 𝐴 ) → suc 𝐵 ∈ 𝐴 )
7 6 ex ⊢ ( ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) → ( 𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴 ) )
8 ordtr ⊢ ( Ord 𝐴 → Tr 𝐴 )
9 trsuc ⊢ ( ( Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 )
10 9 ex ⊢ ( Tr 𝐴 → ( suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) )
11 8 10 syl ⊢ ( Ord 𝐴 → ( suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) )
12 11 adantr ⊢ ( ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) → ( suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴 ) )
13 7 12 impbid ⊢ ( ( Ord 𝐴 ∧ 𝐴 = ∪ 𝐴 ) → ( 𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴 ) )