Theorem dford5

Description: A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021)

	Ref	Expression
Assertion	dford5	|- ( Ord A <-> ( A C_ On /\ Tr A ) )

Proof

Step	Hyp	Ref	Expression
1		ordsson	|- ( Ord A -> A C_ On )
2		ordtr	|- ( Ord A -> Tr A )
3	1 2	jca	|- ( Ord A -> ( A C_ On /\ Tr A ) )
4		epweon	|- _E We On
5		wess	|- ( A C_ On -> ( _E We On -> _E We A ) )
6	4 5	mpi	|- ( A C_ On -> _E We A )
7		df-ord	|- ( Ord A <-> ( Tr A /\ _E We A ) )
8	7	biimpri	|- ( ( Tr A /\ _E We A ) -> Ord A )
9	8	ancoms	|- ( ( _E We A /\ Tr A ) -> Ord A )
10	6 9	sylan	|- ( ( A C_ On /\ Tr A ) -> Ord A )
11	3 10	impbii	|- ( Ord A <-> ( A C_ On /\ Tr A ) )