Metamath Proof Explorer

Theorem onexgt

Description: For any ordinal, there is always a larger ordinal. (Contributed by RP, 1-Feb-2025)

Ref Expression
Assertion onexgt ⊢ A ∈ On → ∃ x ∈ On A ∈ x

Proof

Step Hyp Ref Expression
1 onsuc ⊢ A ∈ On → suc ⁡ A ∈ On
2 sucidg ⊢ A ∈ On → A ∈ suc ⁡ A
3 eleq2 ⊢ x = suc ⁡ A → A ∈ x ↔ A ∈ suc ⁡ A
4 3 rspcev ⊢ suc ⁡ A ∈ On ∧ A ∈ suc ⁡ A → ∃ x ∈ On A ∈ x
5 1 2 4 syl2anc ⊢ A ∈ On → ∃ x ∈ On A ∈ x