Metamath Proof Explorer

Theorem onsucelab

Description: The successor of every ordinal is an element of the class of successor ordinals. Definition 1.11 of Schloeder p. 2. (Contributed by RP, 16-Jan-2025)

Ref Expression
Assertion onsucelab ⊢ A ∈ On → suc ⁡ A ∈ a ∈ On | ∃ b ∈ On a = suc ⁡ b

Proof

Step Hyp Ref Expression
1 onsuc ⊢ A ∈ On → suc ⁡ A ∈ On
2 eqid ⊢ suc ⁡ A = suc ⁡ A
3 id ⊢ A ∈ On → A ∈ On
4 suceq ⊢ b = A → suc ⁡ b = suc ⁡ A
5 4 eqeq2d ⊢ b = A → suc ⁡ A = suc ⁡ b ↔ suc ⁡ A = suc ⁡ A
6 5 adantl ⊢ A ∈ On ∧ b = A → suc ⁡ A = suc ⁡ b ↔ suc ⁡ A = suc ⁡ A
7 3 6 rspcedv ⊢ A ∈ On → suc ⁡ A = suc ⁡ A → ∃ b ∈ On suc ⁡ A = suc ⁡ b
8 2 7 mpi ⊢ A ∈ On → ∃ b ∈ On suc ⁡ A = suc ⁡ b
9 eqeq1 ⊢ a = suc ⁡ A → a = suc ⁡ b ↔ suc ⁡ A = suc ⁡ b
10 9 rexbidv ⊢ a = suc ⁡ A → ∃ b ∈ On a = suc ⁡ b ↔ ∃ b ∈ On suc ⁡ A = suc ⁡ b
11 10 elrab ⊢ suc ⁡ A ∈ a ∈ On | ∃ b ∈ On a = suc ⁡ b ↔ suc ⁡ A ∈ On ∧ ∃ b ∈ On suc ⁡ A = suc ⁡ b
12 1 8 11 sylanbrc ⊢ A ∈ On → suc ⁡ A ∈ a ∈ On | ∃ b ∈ On a = suc ⁡ b