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 ↔ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( ¬ 𝑥 E 𝑥 ∧ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ) )
3 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
4 ordirr ⊢ ( Ord 𝑥 → ¬ 𝑥 ∈ 𝑥 )
5 3 4 syl ⊢ ( 𝑥 ∈ On → ¬ 𝑥 ∈ 𝑥 )
6 epel ⊢ ( 𝑥 E 𝑥 ↔ 𝑥 ∈ 𝑥 )
7 5 6 sylnibr ⊢ ( 𝑥 ∈ On → ¬ 𝑥 E 𝑥 )
8 ontr1 ⊢ ( 𝑧 ∈ On → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ∈ 𝑧 ) )
9 epel ⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
10 epel ⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 )
11 9 10 anbi12i ⊢ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧 ) )
12 epel ⊢ ( 𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧 )
13 8 11 12 3imtr4g ⊢ ( 𝑧 ∈ On → ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) )
14 7 13 anim12i ⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( ¬ 𝑥 E 𝑥 ∧ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ) )
15 14 ralrimiva ⊢ ( 𝑥 ∈ On → ∀ 𝑧 ∈ On ( ¬ 𝑥 E 𝑥 ∧ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ) )
16 15 ralrimivw ⊢ ( 𝑥 ∈ On → ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( ¬ 𝑥 E 𝑥 ∧ ( ( 𝑥 E 𝑦 ∧ 𝑦 E 𝑧 ) → 𝑥 E 𝑧 ) ) )
17 2 16 mprgbir ⊢ E Po On
18 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
19 ordtri3or ⊢ ( ( Ord 𝑥 ∧ Ord 𝑦 ) → ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) )
20 biid ⊢ ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 )
21 epel ⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 )
22 9 20 21 3orbi123i ⊢ ( ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) )
23 19 22 sylibr ⊢ ( ( Ord 𝑥 ∧ Ord 𝑦 ) → ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) )
24 3 18 23 syl2an ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) )
25 24 rgen2 ⊢ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 )
26 df-so ⊢ ( E Or On ↔ ( E Po On ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) ) )
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