This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ontr2

Description: Transitive law for ordinal numbers. Exercise 3 of TakeutiZaring p. 40. (Contributed by NM, 6-Nov-2003)

		Ref	Expression
	Assertion	ontr2	$⊢ (A \in On \land C \in On) \to ((A \subseteq B \land B \in C) \to A \in C)$

Step	Hyp	Ref	Expression
1		eloni	$⊢ A \in On \to Ord A$
2		eloni	$⊢ C \in On \to Ord C$
3		ordtr2	$⊢ (Ord A \land Ord C) \to ((A \subseteq B \land B \in C) \to A \in C)$
4	1 2 3	syl2an	$⊢ (A \in On \land C \in On) \to ((A \subseteq B \land B \in C) \to A \in C)$