Metamath Proof Explorer

Theorem oneptri

Description: The strict, complete (linear) order on the ordinals is complete. Theorem 1.9(iii) of Schloeder p. 1. (Contributed by RP, 15-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 epsoon ⊢ E Or On
2 sotrieq ⊢ E Or On ∧ A ∈ On ∧ B ∈ On → A = B ↔ ¬ A E B ∨ B E A
3 1 2 mpan ⊢ A ∈ On ∧ B ∈ On → A = B ↔ ¬ A E B ∨ B E A
4 xoror ⊢ A E B ∨ B E A ⊻ A = B → A E B ∨ B E A ∨ A = B
5 xorcom ⊢ A E B ∨ B E A ⊻ A = B ↔ A = B ⊻ A E B ∨ B E A
6 df-xor ⊢ A = B ⊻ A E B ∨ B E A ↔ ¬ A = B ↔ A E B ∨ B E A
7 xor3 ⊢ ¬ A = B ↔ A E B ∨ B E A ↔ A = B ↔ ¬ A E B ∨ B E A
8 5 6 7 3bitrri ⊢ A = B ↔ ¬ A E B ∨ B E A ↔ A E B ∨ B E A ⊻ A = B
9 df-3or ⊢ A E B ∨ B E A ∨ A = B ↔ A E B ∨ B E A ∨ A = B
10 4 8 9 3imtr4i ⊢ A = B ↔ ¬ A E B ∨ B E A → A E B ∨ B E A ∨ A = B
11 3 10 syl ⊢ A ∈ On ∧ B ∈ On → A E B ∨ B E A ∨ A = B