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 𝐵 ∈ 𝐴 ) )