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 \leftrightarrow (A \subseteq On \land Tr A)$

Step	Hyp	Ref	Expression
1		ordsson	$⊢ Ord A \to A \subseteq On$
2		ordtr	$⊢ Ord A \to Tr A$
3	1 2	jca	$⊢ Ord A \to (A \subseteq On \land Tr A)$
4		epweon	$⊢ E We On$
5		wess	$⊢ A \subseteq On \to (E We On \to E We A)$
6	4 5	mpi	$⊢ A \subseteq On \to E We A$
7		df-ord	$⊢ Ord A \leftrightarrow (Tr A \land E We A)$
8	7	biimpri	$⊢ (Tr A \land E We A) \to Ord A$
9	8	ancoms	$⊢ (E We A \land Tr A) \to Ord A$
10	6 9	sylan	$⊢ (A \subseteq On \land Tr A) \to Ord A$
11	3 10	impbii	$⊢ Ord A \leftrightarrow (A \subseteq On \land Tr A)$

Metamath Proof Explorer