oneptr

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

		Ref	Expression
	Assertion	oneptr	$⊢ (A \in On \land B \in On \land C \in On) \to ((A E B \land B E C) \to A E C)$

Step	Hyp	Ref	Expression
1		epweon	$⊢ E We On$
2		weso	$⊢ E We On \to E Or On$
3		sopo	$⊢ E Or On \to E Po On$
4		potr	$⊢ (E Po On \land (A \in On \land B \in On \land C \in On)) \to ((A E B \land B E C) \to A E C)$
5	4	ex	$⊢ E Po On \to ((A \in On \land B \in On \land C \in On) \to ((A E B \land B E C) \to A E C))$
6	3 5	syl	$⊢ E Or On \to ((A \in On \land B \in On \land C \in On) \to ((A E B \land B E C) \to A E C))$
7	1 2 6	mp2b	$⊢ (A \in On \land B \in On \land C \in On) \to ((A E B \land B E C) \to A E C)$

Metamath Proof Explorer