MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  epweon Structured version   Visualization version   GIF version

Theorem epweon 7766
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 7729, see epweonALT 7767. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7729. (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.
StepHypRef Expression
1 onfr 6404 . 2 E Fr On
2 df-po 5589 . . . 4 ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
3 eloni 6375 . . . . . . . . 9 (𝑥 ∈ On → Ord 𝑥)
4 ordirr 6383 . . . . . . . . 9 (Ord 𝑥 → ¬ 𝑥𝑥)
53, 4syl 17 . . . . . . . 8 (𝑥 ∈ On → ¬ 𝑥𝑥)
6 epel 5584 . . . . . . . 8 (𝑥 E 𝑥𝑥𝑥)
75, 6sylnibr 328 . . . . . . 7 (𝑥 ∈ On → ¬ 𝑥 E 𝑥)
8 ontr1 6411 . . . . . . . 8 (𝑧 ∈ On → ((𝑥𝑦𝑦𝑧) → 𝑥𝑧))
9 epel 5584 . . . . . . . . 9 (𝑥 E 𝑦𝑥𝑦)
10 epel 5584 . . . . . . . . 9 (𝑦 E 𝑧𝑦𝑧)
119, 10anbi12i 625 . . . . . . . 8 ((𝑥 E 𝑦𝑦 E 𝑧) ↔ (𝑥𝑦𝑦𝑧))
12 epel 5584 . . . . . . . 8 (𝑥 E 𝑧𝑥𝑧)
138, 11, 123imtr4g 295 . . . . . . 7 (𝑧 ∈ On → ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧))
147, 13anim12i 611 . . . . . 6 ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
1514ralrimiva 3144 . . . . 5 (𝑥 ∈ On → ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
1615ralrimivw 3148 . . . 4 (𝑥 ∈ On → ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
172, 16mprgbir 3066 . . 3 E Po On
18 eloni 6375 . . . . 5 (𝑦 ∈ On → Ord 𝑦)
19 ordtri3or 6397 . . . . . 6 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
20 biid 260 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑦)
21 epel 5584 . . . . . . 7 (𝑦 E 𝑥𝑦𝑥)
229, 20, 213orbi123i 1154 . . . . . 6 ((𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥) ↔ (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
2319, 22sylibr 233 . . . . 5 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
243, 18, 23syl2an 594 . . . 4 ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
2524rgen2 3195 . . 3 𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)
26 df-so 5590 . . 3 ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)))
2717, 25, 26mpbir2an 707 . 2 E Or On
28 df-we 5634 . 2 ( E We On ↔ ( E Fr On ∧ E Or On))
291, 27, 28mpbir2an 707 1 E We On
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  w3o 1084  wcel 2104  wral 3059   class class class wbr 5149   E cep 5580   Po wpo 5587   Or wor 5588   Fr wfr 5629   We wwe 5631  Ord word 6364  Oncon0 6365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369
This theorem is referenced by:  ordon  7768  dford5  7775  omsinds  7880  omsindsOLD  7881  onnseq  8348  dfrecs3  8376  dfrecs3OLD  8377  tfr1ALT  8404  tfr2ALT  8405  tfr3ALT  8406  on2recsfn  8670  on2recsov  8671  on2ind  8672  on3ind  8673  ordunifi  9297  ordtypelem8  9524  oismo  9539  cantnfcl  9666  leweon  10010  r0weon  10011  ac10ct  10033  dfac12lem2  10143  cflim2  10262  cofsmo  10268  hsmexlem1  10425  smobeth  10585  gruina  10817  ltsopi  10887  finminlem  35508  dnwech  42094  aomclem4  42103  onsupuni  42282  oninfint  42289  epsoon  42306  epirron  42307  oneptr  42308  oaun3lem1  42428
  Copyright terms: Public domain W3C validator