Theorem onsucuni3

Description: If an ordinal number has a predecessor, then it is successor of that predecessor. (Contributed by ML, 17-Oct-2020)

	Ref	Expression
Assertion	onsucuni3	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → 𝐵 = suc ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐵 ∈ On → Ord 𝐵 )
2	1	3ad2ant1	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → Ord 𝐵 )
3		orduniorsuc	⊢ ( Ord 𝐵 → ( 𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵 ) )
4	2 3	syl	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ( 𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵 ) )
5	4	orcomd	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ( 𝐵 = suc ∪ 𝐵 ∨ 𝐵 = ∪ 𝐵 ) )
6		simp2	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → 𝐵 ≠ ∅ )
7		df-lim	⊢ ( Lim 𝐵 ↔ ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵 ) )
8	7	biimpri	⊢ ( ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵 ) → Lim 𝐵 )
9	8	3expb	⊢ ( ( Ord 𝐵 ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵 ) ) → Lim 𝐵 )
10	9	con3i	⊢ ( ¬ Lim 𝐵 → ¬ ( Ord 𝐵 ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵 ) ) )
11	10	3ad2ant3	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ¬ ( Ord 𝐵 ∧ ( 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵 ) ) )
12	2 11	mpnanrd	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ¬ ( 𝐵 ≠ ∅ ∧ 𝐵 = ∪ 𝐵 ) )
13	6 12	mpnanrd	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → ¬ 𝐵 = ∪ 𝐵 )
14		orcom	⊢ ( ( 𝐵 = suc ∪ 𝐵 ∨ 𝐵 = ∪ 𝐵 ) ↔ ( 𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵 ) )
15		df-or	⊢ ( ( 𝐵 = ∪ 𝐵 ∨ 𝐵 = suc ∪ 𝐵 ) ↔ ( ¬ 𝐵 = ∪ 𝐵 → 𝐵 = suc ∪ 𝐵 ) )
16	14 15	sylbb	⊢ ( ( 𝐵 = suc ∪ 𝐵 ∨ 𝐵 = ∪ 𝐵 ) → ( ¬ 𝐵 = ∪ 𝐵 → 𝐵 = suc ∪ 𝐵 ) )
17	5 13 16	sylc	⊢ ( ( 𝐵 ∈ On ∧ 𝐵 ≠ ∅ ∧ ¬ Lim 𝐵 ) → 𝐵 = suc ∪ 𝐵 )