Metamath Proof Explorer

Theorem ordsseleq

Description: For ordinal classes, inclusion is equivalent to membership or equality. (Contributed by NM, 25-Nov-1995) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ordsseleq ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ B ∨ A = B

Proof

Step Hyp Ref Expression
1 ordelpss ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ↔ A ⊂ B
2 1 orbi1d ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ A = B ↔ A ⊂ B ∨ A = B
3 sspss ⊢ A ⊆ B ↔ A ⊂ B ∨ A = B
4 2 3 syl6rbbr ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ B ∨ A = B