Theorem epweon 7730

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 7690, see epweonALT 7731. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7690. (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 6364	. 2 ⊢ E Fr On
2		df-po 5540	. . . 4 ⊢ ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
3		eloni 6335	. . . . . . . . 9 ⊢ (𝑥 ∈ On → Ord 𝑥)
4		ordirr 6343	. . . . . . . . 9 ⊢ (Ord 𝑥 → ¬ 𝑥 ∈ 𝑥)
5	3, 4	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ On → ¬ 𝑥 ∈ 𝑥)
6		epel 5535	. . . . . . . 8 ⊢ (𝑥 E 𝑥 ↔ 𝑥 ∈ 𝑥)
7	5, 6	sylnibr 329	. . . . . . 7 ⊢ (𝑥 ∈ On → ¬ 𝑥 E 𝑥)
8		ontr1 6372	. . . . . . . 8 ⊢ (𝑧 ∈ On → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧))
9		epel 5535	. . . . . . . . 9 ⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦)
10		epel 5535	. . . . . . . . 9 ⊢ (𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧)
11	9, 10	anbi12i 629	. . . . . . . 8 ⊢ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) ↔ (𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧))
12		epel 5535	. . . . . . . 8 ⊢ (𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧)
13	8, 11, 12	3imtr4g 296	. . . . . . 7 ⊢ (𝑧 ∈ On → ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧))
14	7, 13	anim12i 614	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
15	14	ralrimiva 3130	. . . . 5 ⊢ (𝑥 ∈ On → ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
16	15	ralrimivw 3134	. . . 4 ⊢ (𝑥 ∈ On → ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦 ∧ 𝑦 E 𝑧) → 𝑥 E 𝑧)))
17	2, 16	mprgbir 3059	. . 3 ⊢ E Po On
18		eloni 6335	. . . . 5 ⊢ (𝑦 ∈ On → Ord 𝑦)
19		ordtri3or 6357	. . . . . 6 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
20		biid 261	. . . . . . 7 ⊢ (𝑥 = 𝑦 ↔ 𝑥 = 𝑦)
21		epel 5535	. . . . . . 7 ⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥)
22	9, 20, 21	3orbi123i 1157	. . . . . 6 ⊢ ((𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
23	19, 22	sylibr 234	. . . . 5 ⊢ ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))
24	3, 18, 23	syl2an 597	. . . 4 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥))
25	24	rgen2 3178	. . 3 ⊢ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)
26		df-so 5541	. . 3 ⊢ ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥)))
27	17, 25, 26	mpbir2an 712	. 2 ⊢ E Or On
28		df-we 5587	. 2 ⊢ ( E We On ↔ ( E Fr On ∧ E Or On))
29	1, 27, 28	mpbir2an 712	1 ⊢ E We On

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ w3o 1086   ∈ wcel 2114  ∀wral 3052   class class class wbr 5100   E cep 5531   Po wpo 5538   Or wor 5539   Fr wfr 5582   We wwe 5584  Ord word 6324  Oncon0 6325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-ord 6328  df-on 6329

This theorem is referenced by:  ordon  7732  dford5  7739  omsinds  7839  onnseq  8286  dfrecs3  8314  tfr1ALT  8341  tfr2ALT  8342  tfr3ALT  8343  on2recsfn  8605  on2recsov  8606  on2ind  8607  on3ind  8608  ordunifi  9202  ordtypelem8  9442  oismo  9457  cantnfcl  9588  leweon  9933  r0weon  9934  ac10ct  9956  dfac12lem2  10067  cflim2  10185  cofsmo  10191  hsmexlem1  10348  smobeth  10509  gruina  10741  ltsopi  10811  onswe  28280  finminlem  36531  dnwech  43399  aomclem4  43408  onsupuni  43580  oninfint  43587  epsoon  43604  epirron  43605  oneptr  43606  oaun3lem1  43725