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 e. On /\ B e. 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 e. On /\ B e. On ) ) -> ( A = B <-> -. ( A _E B \/ B _E A ) ) )
3	1 2	mpan	|- ( ( A e. On /\ B e. 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 e. On /\ B e. On ) -> ( A _E B \/ B _E A \/ A = B ) )