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. For a shorter proof requiring ax-un , see epweonALT . (Contributed by NM, 1-Nov-2003) Avoid ax-un . (Revised by BTernaryTau, 30-Nov-2024)

Ref Expression
Assertion epweon ⊢ E We On

Proof

Step Hyp Ref Expression
1 onfr ⊢ E Fr On
2 df-po ⊢ E Po On ↔ ∀ x ∈ On ∀ y ∈ On ∀ z ∈ On ¬ x E x ∧ x E y ∧ y E z → x E z
3 eloni ⊢ x ∈ On → Ord ⁡ x
4 ordirr ⊢ Ord ⁡ x → ¬ x ∈ x
5 3 4 syl ⊢ x ∈ On → ¬ x ∈ x
6 epel ⊢ x E x ↔ x ∈ x
7 5 6 sylnibr ⊢ x ∈ On → ¬ x E x
8 ontr1 ⊢ z ∈ On → x ∈ y ∧ y ∈ z → x ∈ z
9 epel ⊢ x E y ↔ x ∈ y
10 epel ⊢ y E z ↔ y ∈ z
11 9 10 anbi12i ⊢ x E y ∧ y E z ↔ x ∈ y ∧ y ∈ z
12 epel ⊢ x E z ↔ x ∈ z
13 8 11 12 3imtr4g ⊢ z ∈ On → x E y ∧ y E z → x E z
14 7 13 anim12i ⊢ x ∈ On ∧ z ∈ On → ¬ x E x ∧ x E y ∧ y E z → x E z
15 14 ralrimiva ⊢ x ∈ On → ∀ z ∈ On ¬ x E x ∧ x E y ∧ y E z → x E z
16 15 ralrimivw ⊢ x ∈ On → ∀ y ∈ On ∀ z ∈ On ¬ x E x ∧ x E y ∧ y E z → x E z
17 2 16 mprgbir ⊢ E Po On
18 eloni ⊢ y ∈ On → Ord ⁡ y
19 ordtri3or ⊢ Ord ⁡ x ∧ Ord ⁡ y → x ∈ y ∨ x = y ∨ y ∈ x
20 biid ⊢ x = y ↔ x = y
21 epel ⊢ y E x ↔ y ∈ x
22 9 20 21 3orbi123i ⊢ x E y ∨ x = y ∨ y E x ↔ x ∈ y ∨ x = y ∨ y ∈ x
23 19 22 sylibr ⊢ Ord ⁡ x ∧ Ord ⁡ y → x E y ∨ x = y ∨ y E x
24 3 18 23 syl2an ⊢ x ∈ On ∧ y ∈ On → x E y ∨ x = y ∨ y E x
25 24 rgen2 ⊢ ∀ x ∈ On ∀ y ∈ On x E y ∨ x = y ∨ y E x
26 df-so ⊢ E Or On ↔ E Po On ∧ ∀ x ∈ On ∀ y ∈ On x E y ∨ x = y ∨ y E x
27 17 25 26 mpbir2an ⊢ E Or On
28 df-we ⊢ E We On ↔ E Fr On ∧ E Or On
29 1 27 28 mpbir2an ⊢ E We On