Metamath Proof Explorer

Theorem dford3

Description: Ordinals are precisely the hereditarily transitive classes. (Contributed by Stefan O'Rear, 28-Oct-2014)

Ref Expression
Assertion dford3 ⊢ Ord ⁡ N ↔ Tr ⁡ N ∧ ∀ x ∈ N Tr ⁡ x

Proof

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