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

Theorem epweon 7762
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 7722, see epweonALT 7763. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7722. (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 6389 . 2 E Fr On
2 df-po 5559 . . . 4 ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
3 eloni 6359 . . . . . . . . 9 (𝑥 ∈ On → Ord 𝑥)
4 ordirr 6367 . . . . . . . . 9 (Ord 𝑥 → ¬ 𝑥𝑥)
53, 4syl 18 . . . . . . . 8 (𝑥 ∈ On → ¬ 𝑥𝑥)
6 epel 5554 . . . . . . . 8 (𝑥 E 𝑥𝑥𝑥)
75, 6sylnibr 332 . . . . . . 7 (𝑥 ∈ On → ¬ 𝑥 E 𝑥)
8 ontr1 6397 . . . . . . . 8 (𝑧 ∈ On → ((𝑥𝑦𝑦𝑧) → 𝑥𝑧))
9 epel 5554 . . . . . . . . 9 (𝑥 E 𝑦𝑥𝑦)
10 epel 5554 . . . . . . . . 9 (𝑦 E 𝑧𝑦𝑧)
119, 10anbi12i 639 . . . . . . . 8 ((𝑥 E 𝑦𝑦 E 𝑧) ↔ (𝑥𝑦𝑦𝑧))
12 epel 5554 . . . . . . . 8 (𝑥 E 𝑧𝑥𝑧)
138, 11, 123imtr4g 299 . . . . . . 7 (𝑧 ∈ On → ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧))
147, 13anim12i 624 . . . . . 6 ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
1514ralrimiva 3157 . . . . 5 (𝑥 ∈ On → ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
1615ralrimivw 3161 . . . 4 (𝑥 ∈ On → ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
172, 16mprgbir 3086 . . 3 E Po On
18 eloni 6359 . . . . 5 (𝑦 ∈ On → Ord 𝑦)
19 ordtri3or 6382 . . . . . 6 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
20 biid 264 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑦)
21 epel 5554 . . . . . . 7 (𝑦 E 𝑥𝑦𝑥)
229, 20, 213orbi123i 1172 . . . . . 6 ((𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥) ↔ (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
2319, 22sylibr 237 . . . . 5 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
243, 18, 23syl2an 607 . . . 4 ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
2524rgen2 3205 . . 3 𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)
26 df-so 5560 . . 3 ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)))
2717, 25, 26mpbir2an 723 . 2 E Or On
28 df-we 5606 . 2 ( E We On ↔ ( E Fr On ∧ E Or On))
291, 27, 28mpbir2an 723 1 E We On
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 400  w3o 1100  wcel 2145  wral 3079   class class class wbr 5104   E cep 5550   Po wpo 5557   Or wor 5558   Fr wfr 5601   We wwe 5603  Ord word 6348  Oncon0 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6352  df-on 6353
This theorem is referenced by:  ordon  7764  dford5  7771  omsinds  7871  onnseq  8319  dfrecs3  8347  tfr1ALT  8375  tfr2ALT  8376  tfr3ALT  8377  on2recsfn  8641  on2recsov  8642  on2ind  8643  on3ind  8644  ordunifi  9238  ordtypelem8  9475  oismo  9490  cantnfcl  9624  leweon  9983  r0weon  9984  ac10ct  10006  dfac12lem2  10116  cflim2  10235  cofsmo  10241  hsmexlem1  10398  smobeth  10559  gruina  10791  ltsopi  10861  onswe  28419  finminlem  36686  dnwech  43632  aomclem4  43641  onsupuni  43813  oninfint  43820  epsoon  43837  epirron  43838  oneptr  43839  oaun3lem1  43958
  Copyright terms: Public domain W3C validator