# 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 ${⊢}\mathrm{Ord}{N}↔\left(\mathrm{Tr}{N}\wedge \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)$

### Proof

Step Hyp Ref Expression
1 ordtr ${⊢}\mathrm{Ord}{N}\to \mathrm{Tr}{N}$
2 ordelord ${⊢}\left(\mathrm{Ord}{N}\wedge {x}\in {N}\right)\to \mathrm{Ord}{x}$
3 ordtr ${⊢}\mathrm{Ord}{x}\to \mathrm{Tr}{x}$
4 2 3 syl ${⊢}\left(\mathrm{Ord}{N}\wedge {x}\in {N}\right)\to \mathrm{Tr}{x}$
5 4 ralrimiva ${⊢}\mathrm{Ord}{N}\to \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}$
6 1 5 jca ${⊢}\mathrm{Ord}{N}\to \left(\mathrm{Tr}{N}\wedge \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)$
7 simpl ${⊢}\left(\mathrm{Tr}{N}\wedge \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)\to \mathrm{Tr}{N}$
8 dford3lem1 ${⊢}\left(\mathrm{Tr}{N}\wedge \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)\to \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Tr}{a}\wedge \forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)$
9 dford3lem2 ${⊢}\left(\mathrm{Tr}{a}\wedge \forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)\to {a}\in \mathrm{On}$
10 9 ralimi ${⊢}\forall {a}\in {N}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Tr}{a}\wedge \forall {x}\in {a}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)\to \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}{a}\in \mathrm{On}$
11 8 10 syl ${⊢}\left(\mathrm{Tr}{N}\wedge \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)\to \forall {a}\in {N}\phantom{\rule{.4em}{0ex}}{a}\in \mathrm{On}$
12 dfss3 ${⊢}{N}\subseteq \mathrm{On}↔\forall {a}\in {N}\phantom{\rule{.4em}{0ex}}{a}\in \mathrm{On}$
13 11 12 sylibr ${⊢}\left(\mathrm{Tr}{N}\wedge \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)\to {N}\subseteq \mathrm{On}$
14 ordon ${⊢}\mathrm{Ord}\mathrm{On}$
15 14 a1i ${⊢}\left(\mathrm{Tr}{N}\wedge \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)\to \mathrm{Ord}\mathrm{On}$
16 trssord ${⊢}\left(\mathrm{Tr}{N}\wedge {N}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{On}\right)\to \mathrm{Ord}{N}$
17 7 13 15 16 syl3anc ${⊢}\left(\mathrm{Tr}{N}\wedge \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)\to \mathrm{Ord}{N}$
18 6 17 impbii ${⊢}\mathrm{Ord}{N}↔\left(\mathrm{Tr}{N}\wedge \forall {x}\in {N}\phantom{\rule{.4em}{0ex}}\mathrm{Tr}{x}\right)$