Metamath Proof Explorer

Theorem ordsssuc

Description: An ordinal is a subset of another ordinal if and only if it belongs to its successor. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordsssuc ⊢ A ∈ On ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ suc ⁡ B

Proof

Step Hyp Ref Expression
1 eloni ⊢ A ∈ On → Ord ⁡ A
2 ordsseleq ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ B ∨ A = B
3 1 2 sylan ⊢ A ∈ On ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ B ∨ A = B
4 elsucg ⊢ A ∈ On → A ∈ suc ⁡ B ↔ A ∈ B ∨ A = B
5 4 adantr ⊢ A ∈ On ∧ Ord ⁡ B → A ∈ suc ⁡ B ↔ A ∈ B ∨ A = B
6 3 5 bitr4d ⊢ A ∈ On ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ suc ⁡ B