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 \in On \land B \in On) \to (A E B \lor B E A \lor A = B)$

Proof

Step	Hyp	Ref	Expression
1		epsoon	$⊢ E Or On$
2		sotrieq	$⊢ (E Or On \land (A \in On \land B \in On)) \to (A = B \leftrightarrow \neg (A E B \lor B E A))$
3	1 2	mpan	$⊢ (A \in On \land B \in On) \to (A = B \leftrightarrow \neg (A E B \lor B E A))$
4		xoror	$⊢ ((A E B \lor B E A) ⊻ A = B) \to ((A E B \lor B E A) \lor A = B)$
5		xorcom	$⊢ ((A E B \lor B E A) ⊻ A = B) \leftrightarrow (A = B ⊻ (A E B \lor B E A))$
6		df-xor	$⊢ (A = B ⊻ (A E B \lor B E A)) \leftrightarrow \neg (A = B \leftrightarrow (A E B \lor B E A))$
7		xor3	$⊢ \neg (A = B \leftrightarrow (A E B \lor B E A)) \leftrightarrow (A = B \leftrightarrow \neg (A E B \lor B E A))$
8	5 6 7	3bitrri	$⊢ (A = B \leftrightarrow \neg (A E B \lor B E A)) \leftrightarrow ((A E B \lor B E A) ⊻ A = B)$
9		df-3or	$⊢ (A E B \lor B E A \lor A = B) \leftrightarrow ((A E B \lor B E A) \lor A = B)$
10	4 8 9	3imtr4i	$⊢ (A = B \leftrightarrow \neg (A E B \lor B E A)) \to (A E B \lor B E A \lor A = B)$
11	3 10	syl	$⊢ (A \in On \land B \in On) \to (A E B \lor B E A \lor A = B)$