Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		ontr1	$⊢ C \in On \to ((A \in B \land B \in C) \to A \in C)$
2	1	3ad2ant3	$⊢ (A \in On \land B \in On \land C \in On) \to ((A \in B \land B \in C) \to A \in C)$