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	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\in B\vee B\in A\vee A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
2		eloni	$$⊢B\in \mathrm{On}\to \mathrm{Ord}B$$
3		ordtri3or	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\in B\vee A=B\vee B\in A\right)$$
4	1 2 3	syl2an	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\in B\vee A=B\vee B\in A\right)$$
5		3orcomb	$$⊢\left(A\in B\vee A=B\vee B\in A\right)\leftrightarrow \left(A\in B\vee B\in A\vee A=B\right)$$
6	4 5	sylib	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \left(A\in B\vee B\in A\vee A=B\right)$$