Theorem epweon 7793

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 7753, see epweonALT 7794. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7753. (Revised by BTernaryTau, 30-Nov-2024.)

Assertion

Ref	Expression
epweon	⊢ E We On

Proof of Theorem epweon

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		onfr 6424	. 2 ⊢ E Fr On
2		df-po 5596	. . . 4 ⊢ ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
3		eloni 6395	. . . . . . . . 9 ⊢ (𝑥 ∈ On → Ord 𝑥)
4		ordirr 6403	. . . . . . . . 9 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥)
5	3, 4	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ On → ¬ 𝑥 ∈ 𝑥)
6		epel 5591	. . . . . . . 8 ⊢ (𝑥 E 𝑥 ↔ 𝑥 ∈ 𝑥)
7	5, 6	sylnibr 329	. . . . . . 7 ⊢ (𝑥 ∈ On → ¬ 𝑥 E 𝑥)
8		ontr1 6431	. . . . . . . 8 ⊢ (𝑧 ∈ On → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧))
9		epel 5591	. . . . . . . . 9 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦)
10		epel 5591	. . . . . . . . 9 ⊢ (𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧)
11	9, 10	anbi12i 628	. . . . . . . 8 ⊢ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧))
12		epel 5591	. . . . . . . 8 ⊢ (𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧)
13	8, 11, 12	3imtr4g 296	. . . . . . 7 ⊢ (𝑧 ∈ On → ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))
14	7, 13	anim12i 613	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
15	14	ralrimiva 3143	. . . . 5 ⊢ (𝑥 ∈ On → ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
16	15	ralrimivw 3147	. . . 4 ⊢ (𝑥 ∈ On → ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
17	2, 16	mprgbir 3065	. . 3 ⊢ E Po On
18		eloni 6395	. . . . 5 ⊢ (𝑦 ∈ On → Ord 𝑦)
19		ordtri3or 6417	. . . . . 6 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
20		biid 261	. . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦)
21		epel 5591	. . . . . . 7 ⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥)
22	9, 20, 21	3orbi123i 1155	. . . . . 6 ⊢ ((𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
23	19, 22	sylibr 234	. . . . 5 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))
24	3, 18, 23	syl2an 596	. . . 4 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))
25	24	rgen2 3196	. . 3 ⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)
26		df-so 5597	. . 3 ⊢ ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)))
27	17, 25, 26	mpbir2an 711	. 2 ⊢ E Or On
28		df-we 5642	. 2 ⊢ ( E We On ↔ ( E Fr On ∧ E Or On))
29	1, 27, 28	mpbir2an 711	1 ⊢ E We On

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ w3o 1085   ∈ wcel 2105  ∀wral 3058   class class class wbr 5147   E cep 5587   Po wpo 5594   Or wor 5595   Fr wfr 5637   We wwe 5639  Ord word 6384  Oncon0 6385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389

This theorem is referenced by:  ordon  7795  dford5  7802  omsinds  7907  omsindsOLD  7908  onnseq  8382  dfrecs3  8410  dfrecs3OLD  8411  tfr1ALT  8438  tfr2ALT  8439  tfr3ALT  8440  on2recsfn  8703  on2recsov  8704  on2ind  8705  on3ind  8706  ordunifi  9323  ordtypelem8  9562  oismo  9577  cantnfcl  9704  leweon  10048  r0weon  10049  ac10ct  10071  dfac12lem2  10182  cflim2  10300  cofsmo  10306  hsmexlem1  10463  smobeth  10623  gruina  10855  ltsopi  10925  finminlem  36300  dnwech  43036  aomclem4  43045  onsupuni  43217  oninfint  43224  epsoon  43241  epirron  43242  oneptr  43243  oaun3lem1  43363