Metamath Proof Explorer

Theorem ontri1

Description: A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003)

Ref Expression
Assertion ontri1 ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ¬ B ∈ A

Proof

Step Hyp Ref Expression
1 eloni ⊢ A ∈ On → Ord ⁡ A
2 eloni ⊢ B ∈ On → Ord ⁡ B
3 ordtri1 ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ ¬ B ∈ A
4 1 2 3 syl2an ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ¬ B ∈ A