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 sspss ⊢ A ⊆ B ↔ A ⊂ B ∨ A = B
2 ordelpss ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ↔ A ⊂ B
3 2 orbi1d ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ A = B ↔ A ⊂ B ∨ A = B
4 1 3 bitr4id ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ B ∨ A = B