# Metamath Proof Explorer

## Theorem epweon

Description: The membership relation well-orders the class of ordinal numbers. This proof does not require the axiom of regularity. Proposition 4.8(g) of Mendelson p. 244. (Contributed by NM, 1-Nov-2003)

Ref Expression
Assertion epweon ${⊢}\mathrm{E}\mathrm{We}\mathrm{On}$

### Proof

Step Hyp Ref Expression
1 onfr ${⊢}\mathrm{E}\mathrm{Fr}\mathrm{On}$
2 eloni ${⊢}{x}\in \mathrm{On}\to \mathrm{Ord}{x}$
3 eloni ${⊢}{y}\in \mathrm{On}\to \mathrm{Ord}{y}$
4 ordtri3or ${⊢}\left(\mathrm{Ord}{x}\wedge \mathrm{Ord}{y}\right)\to \left({x}\in {y}\vee {x}={y}\vee {y}\in {x}\right)$
5 epel ${⊢}{x}\mathrm{E}{y}↔{x}\in {y}$
6 biid ${⊢}{x}={y}↔{x}={y}$
7 epel ${⊢}{y}\mathrm{E}{x}↔{y}\in {x}$
8 5 6 7 3orbi123i ${⊢}\left({x}\mathrm{E}{y}\vee {x}={y}\vee {y}\mathrm{E}{x}\right)↔\left({x}\in {y}\vee {x}={y}\vee {y}\in {x}\right)$
9 4 8 sylibr ${⊢}\left(\mathrm{Ord}{x}\wedge \mathrm{Ord}{y}\right)\to \left({x}\mathrm{E}{y}\vee {x}={y}\vee {y}\mathrm{E}{x}\right)$
10 2 3 9 syl2an ${⊢}\left({x}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({x}\mathrm{E}{y}\vee {x}={y}\vee {y}\mathrm{E}{x}\right)$
11 10 rgen2 ${⊢}\forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{E}{y}\vee {x}={y}\vee {y}\mathrm{E}{x}\right)$
12 dfwe2 ${⊢}\mathrm{E}\mathrm{We}\mathrm{On}↔\left(\mathrm{E}\mathrm{Fr}\mathrm{On}\wedge \forall {x}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{On}\phantom{\rule{.4em}{0ex}}\left({x}\mathrm{E}{y}\vee {x}={y}\vee {y}\mathrm{E}{x}\right)\right)$
13 1 11 12 mpbir2an ${⊢}\mathrm{E}\mathrm{We}\mathrm{On}$