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 ⊢ E We On

Proof

Step Hyp Ref Expression
1 onfr ⊢ E Fr On
2 eloni ⊢ x ∈ On → Ord ⁡ x
3 eloni ⊢ y ∈ On → Ord ⁡ y
4 ordtri3or ⊢ Ord ⁡ x ∧ Ord ⁡ y → x ∈ y ∨ x = y ∨ y ∈ x
5 epel ⊢ x E y ↔ x ∈ y
6 biid ⊢ x = y ↔ x = y
7 epel ⊢ y E x ↔ y ∈ x
8 5 6 7 3orbi123i ⊢ x E y ∨ x = y ∨ y E x ↔ x ∈ y ∨ x = y ∨ y ∈ x
9 4 8 sylibr ⊢ Ord ⁡ x ∧ Ord ⁡ y → x E y ∨ x = y ∨ y E x
10 2 3 9 syl2an ⊢ x ∈ On ∧ y ∈ On → x E y ∨ x = y ∨ y E x
11 10 rgen2 ⊢ ∀ x ∈ On ∀ y ∈ On x E y ∨ x = y ∨ y E x
12 dfwe2 ⊢ E We On ↔ E Fr On ∧ ∀ x ∈ On ∀ y ∈ On x E y ∨ x = y ∨ y E x
13 1 11 12 mpbir2an ⊢ E We On