Theorem oneltr

Description: The elementhood relation on the ordinals is transitive. Theorem 1.9(ii) of Schloeder p. 1. See ontr1 . (Contributed by RP, 15-Jan-2025)

	Ref	Expression
Assertion	oneltr	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A e. B /\ B e. C ) -> A e. C ) )

Proof

Step	Hyp	Ref	Expression
1		ontr1	|- ( C e. On -> ( ( A e. B /\ B e. C ) -> A e. C ) )
2	1	3ad2ant3	|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A e. B /\ B e. C ) -> A e. C ) )