Metamath Proof Explorer

Theorem oneltri

Description: The elementhood relation on the ordinals is complete, so we have triality. Theorem 1.9(iii) of Schloeder p. 1. See ordtri3or . (Contributed by RP, 15-Jan-2025)

Ref Expression
Assertion oneltri ⊢ A ∈ On ∧ B ∈ On → A ∈ B ∨ B ∈ A ∨ A = B

Proof

Step Hyp Ref Expression
1 eloni ⊢ A ∈ On → Ord ⁡ A
2 eloni ⊢ B ∈ On → Ord ⁡ B
3 ordtri3or ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ∈ B ∨ A = B ∨ B ∈ A
4 1 2 3 syl2an ⊢ A ∈ On ∧ B ∈ On → A ∈ B ∨ A = B ∨ B ∈ A
5 3orcomb ⊢ A ∈ B ∨ A = B ∨ B ∈ A ↔ A ∈ B ∨ B ∈ A ∨ A = B
6 4 5 sylib ⊢ A ∈ On ∧ B ∈ On → A ∈ B ∨ B ∈ A ∨ A = B