trssord

Description: A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994)

		Ref	Expression
	Assertion	trssord	$⊢ (Tr A \land A \subseteq B \land Ord B) \to Ord A$

Step	Hyp	Ref	Expression
1		wess	$⊢ A \subseteq B \to (E We B \to E We A)$
2		ordwe	$⊢ Ord B \to E We B$
3	1 2	impel	$⊢ (A \subseteq B \land Ord B) \to E We A$
4	3	anim2i	$⊢ (Tr A \land (A \subseteq B \land Ord B)) \to (Tr A \land E We A)$
5	4	3impb	$⊢ (Tr A \land A \subseteq B \land Ord B) \to (Tr A \land E We A)$
6		df-ord	$⊢ Ord A \leftrightarrow (Tr A \land E We A)$
7	5 6	sylibr	$⊢ (Tr A \land A \subseteq B \land Ord B) \to Ord A$

Metamath Proof Explorer