Theorem trssord

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

	Ref	Expression
Assertion	trssord	|- ( ( Tr A /\ A C_ B /\ Ord B ) -> Ord A )

Proof

Step	Hyp	Ref	Expression
1		wess	|- ( A C_ B -> ( _E We B -> _E We A ) )
2		ordwe	|- ( Ord B -> _E We B )
3	1 2	impel	|- ( ( A C_ B /\ Ord B ) -> _E We A )
4	3	anim2i	|- ( ( Tr A /\ ( A C_ B /\ Ord B ) ) -> ( Tr A /\ _E We A ) )
5	4	3impb	|- ( ( Tr A /\ A C_ B /\ Ord B ) -> ( Tr A /\ _E We A ) )
6		df-ord	|- ( Ord A <-> ( Tr A /\ _E We A ) )
7	5 6	sylibr	|- ( ( Tr A /\ A C_ B /\ Ord B ) -> Ord A )