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 e. On /\ B e. On ) -> ( A e. B \/ B e. A \/ A = B ) )

Proof

Step	Hyp	Ref	Expression
1		eloni	|- ( A e. On -> Ord A )
2		eloni	|- ( B e. On -> Ord B )
3		ordtri3or	|- ( ( Ord A /\ Ord B ) -> ( A e. B \/ A = B \/ B e. A ) )
4	1 2 3	syl2an	|- ( ( A e. On /\ B e. On ) -> ( A e. B \/ A = B \/ B e. A ) )
5		3orcomb	|- ( ( A e. B \/ A = B \/ B e. A ) <-> ( A e. B \/ B e. A \/ A = B ) )
6	4 5	sylib	|- ( ( A e. On /\ B e. On ) -> ( A e. B \/ B e. A \/ A = B ) )