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 <-> ( Tr N /\ A. x e. N Tr x ) )

Proof

Step	Hyp	Ref	Expression
1		ordtr	|- ( Ord N -> Tr N )
2		ordelord	|- ( ( Ord N /\ x e. N ) -> Ord x )
3		ordtr	|- ( Ord x -> Tr x )
4	2 3	syl	|- ( ( Ord N /\ x e. N ) -> Tr x )
5	4	ralrimiva	|- ( Ord N -> A. x e. N Tr x )
6	1 5	jca	|- ( Ord N -> ( Tr N /\ A. x e. N Tr x ) )
7		simpl	|- ( ( Tr N /\ A. x e. N Tr x ) -> Tr N )
8		dford3lem1	|- ( ( Tr N /\ A. x e. N Tr x ) -> A. a e. N ( Tr a /\ A. x e. a Tr x ) )
9		dford3lem2	|- ( ( Tr a /\ A. x e. a Tr x ) -> a e. On )
10	9	ralimi	|- ( A. a e. N ( Tr a /\ A. x e. a Tr x ) -> A. a e. N a e. On )
11	8 10	syl	|- ( ( Tr N /\ A. x e. N Tr x ) -> A. a e. N a e. On )
12		dfss3	|- ( N C_ On <-> A. a e. N a e. On )
13	11 12	sylibr	|- ( ( Tr N /\ A. x e. N Tr x ) -> N C_ On )
14		ordon	|- Ord On
15	14	a1i	|- ( ( Tr N /\ A. x e. N Tr x ) -> Ord On )
16		trssord	|- ( ( Tr N /\ N C_ On /\ Ord On ) -> Ord N )
17	7 13 15 16	syl3anc	|- ( ( Tr N /\ A. x e. N Tr x ) -> Ord N )
18	6 17	impbii	|- ( Ord N <-> ( Tr N /\ A. x e. N Tr x ) )