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 𝑁 ↔ ( Tr 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 Tr 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtr	⊢ ( Ord 𝑁 → Tr 𝑁 )
2		ordelord	⊢ ( ( Ord 𝑁 ∧ 𝑥 ∈ 𝑁 ) → Ord 𝑥 )
3		ordtr	⊢ ( Ord 𝑥 → Tr 𝑥 )
4	2 3	syl	⊢ ( ( Ord 𝑁 ∧ 𝑥 ∈ 𝑁 ) → Tr 𝑥 )
5	4	ralrimiva	⊢ ( Ord 𝑁 → ∀ 𝑥 ∈ 𝑁 Tr 𝑥 )
6	1 5	jca	⊢ ( Ord 𝑁 → ( Tr 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 Tr 𝑥 ) )
7		simpl	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 Tr 𝑥 ) → Tr 𝑁 )
8		dford3lem1	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 Tr 𝑥 ) → ∀ 𝑎 ∈ 𝑁 ( Tr 𝑎 ∧ ∀ 𝑥 ∈ 𝑎 Tr 𝑥 ) )
9		dford3lem2	⊢ ( ( Tr 𝑎 ∧ ∀ 𝑥 ∈ 𝑎 Tr 𝑥 ) → 𝑎 ∈ On )
10	9	ralimi	⊢ ( ∀ 𝑎 ∈ 𝑁 ( Tr 𝑎 ∧ ∀ 𝑥 ∈ 𝑎 Tr 𝑥 ) → ∀ 𝑎 ∈ 𝑁 𝑎 ∈ On )
11	8 10	syl	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 Tr 𝑥 ) → ∀ 𝑎 ∈ 𝑁 𝑎 ∈ On )
12		dfss3	⊢ ( 𝑁 ⊆ On ↔ ∀ 𝑎 ∈ 𝑁 𝑎 ∈ On )
13	11 12	sylibr	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 Tr 𝑥 ) → 𝑁 ⊆ On )
14		ordon	⊢ Ord On
15	14	a1i	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 Tr 𝑥 ) → Ord On )
16		trssord	⊢ ( ( Tr 𝑁 ∧ 𝑁 ⊆ On ∧ Ord On ) → Ord 𝑁 )
17	7 13 15 16	syl3anc	⊢ ( ( Tr 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 Tr 𝑥 ) → Ord 𝑁 )
18	6 17	impbii	⊢ ( Ord 𝑁 ↔ ( Tr 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 Tr 𝑥 ) )