Metamath Proof Explorer

Theorem dford3

Description: Ordinals are precisely the hereditarily transitive classes. Definition 1.2 of Schloeder p. 1. (Contributed by Stefan O'Rear, 28-Oct-2014)

		Ref	Expression
	Assertion	dford3	$⊢ Ord N \leftrightarrow (Tr N \land \forall x \in N Tr x)$

Proof

Step	Hyp	Ref	Expression
1		ordtr	$⊢ Ord N \to Tr N$
2		ordelord	$⊢ (Ord N \land x \in N) \to Ord x$
3		ordtr	$⊢ Ord x \to Tr x$
4	2 3	syl	$⊢ (Ord N \land x \in N) \to Tr x$
5	4	ralrimiva	$⊢ Ord N \to \forall x \in N Tr x$
6	1 5	jca	$⊢ Ord N \to (Tr N \land \forall x \in N Tr x)$
7		simpl	$⊢ (Tr N \land \forall x \in N Tr x) \to Tr N$
8		dford3lem1	$⊢ (Tr N \land \forall x \in N Tr x) \to \forall a \in N (Tr a \land \forall x \in a Tr x)$
9		dford3lem2	$⊢ (Tr a \land \forall x \in a Tr x) \to a \in On$
10	9	ralimi	$⊢ \forall a \in N (Tr a \land \forall x \in a Tr x) \to \forall a \in N a \in On$
11	8 10	syl	$⊢ (Tr N \land \forall x \in N Tr x) \to \forall a \in N a \in On$
12		dfss3	$⊢ N \subseteq On \leftrightarrow \forall a \in N a \in On$
13	11 12	sylibr	$⊢ (Tr N \land \forall x \in N Tr x) \to N \subseteq On$
14		ordon	$⊢ Ord On$
15	14	a1i	$⊢ (Tr N \land \forall x \in N Tr x) \to Ord On$
16		trssord	$⊢ (Tr N \land N \subseteq On \land Ord On) \to Ord N$
17	7 13 15 16	syl3anc	$⊢ (Tr N \land \forall x \in N Tr x) \to Ord N$
18	6 17	impbii	$⊢ Ord N \leftrightarrow (Tr N \land \forall x \in N Tr x)$