Metamath Proof Explorer

Theorem onpsssuc

Description: An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Assertion onpsssuc ⊢ A ∈ On → A ⊂ suc ⁡ A

Proof

Step Hyp Ref Expression
1 sucidg ⊢ A ∈ On → A ∈ suc ⁡ A
2 eloni ⊢ A ∈ On → Ord ⁡ A
3 ordsuc ⊢ Ord ⁡ A ↔ Ord ⁡ suc ⁡ A
4 2 3 sylib ⊢ A ∈ On → Ord ⁡ suc ⁡ A
5 ordelpss ⊢ Ord ⁡ A ∧ Ord ⁡ suc ⁡ A → A ∈ suc ⁡ A ↔ A ⊂ suc ⁡ A
6 2 4 5 syl2anc ⊢ A ∈ On → A ∈ suc ⁡ A ↔ A ⊂ suc ⁡ A
7 1 6 mpbid ⊢ A ∈ On → A ⊂ suc ⁡ A