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

Theorem epweon 7710
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 7673, see epweonALT 7711. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7673. (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 6357 . 2 E Fr On
2 df-po 5546 . . . 4 ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
3 eloni 6328 . . . . . . . . 9 (𝑥 ∈ On → Ord 𝑥)
4 ordirr 6336 . . . . . . . . 9 (Ord 𝑥 → ¬ 𝑥𝑥)
53, 4syl 17 . . . . . . . 8 (𝑥 ∈ On → ¬ 𝑥𝑥)
6 epel 5541 . . . . . . . 8 (𝑥 E 𝑥𝑥𝑥)
75, 6sylnibr 329 . . . . . . 7 (𝑥 ∈ On → ¬ 𝑥 E 𝑥)
8 ontr1 6364 . . . . . . . 8 (𝑧 ∈ On → ((𝑥𝑦𝑦𝑧) → 𝑥𝑧))
9 epel 5541 . . . . . . . . 9 (𝑥 E 𝑦𝑥𝑦)
10 epel 5541 . . . . . . . . 9 (𝑦 E 𝑧𝑦𝑧)
119, 10anbi12i 628 . . . . . . . 8 ((𝑥 E 𝑦𝑦 E 𝑧) ↔ (𝑥𝑦𝑦𝑧))
12 epel 5541 . . . . . . . 8 (𝑥 E 𝑧𝑥𝑧)
138, 11, 123imtr4g 296 . . . . . . 7 (𝑧 ∈ On → ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧))
147, 13anim12i 614 . . . . . 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 3072 . . 3 E Po On
18 eloni 6328 . . . . 5 (𝑦 ∈ On → Ord 𝑦)
19 ordtri3or 6350 . . . . . 6 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
20 biid 261 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑦)
21 epel 5541 . . . . . . 7 (𝑦 E 𝑥𝑦𝑥)
229, 20, 213orbi123i 1157 . . . . . 6 ((𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥) ↔ (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
2319, 22sylibr 233 . . . . 5 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
243, 18, 23syl2an 597 . . . 4 ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
2524rgen2 3195 . . 3 𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)
26 df-so 5547 . . 3 ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)))
2717, 25, 26mpbir2an 710 . 2 E Or On
28 df-we 5591 . 2 ( E We On ↔ ( E Fr On ∧ E Or On))
291, 27, 28mpbir2an 710 1 E We On
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  w3o 1087  wcel 2107  wral 3065   class class class wbr 5106   E cep 5537   Po wpo 5544   Or wor 5545   Fr wfr 5586   We wwe 5588  Ord word 6317  Oncon0 6318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-tr 5224  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-ord 6321  df-on 6322
This theorem is referenced by:  ordon  7712  dford5  7719  omsinds  7824  omsindsOLD  7825  onnseq  8291  dfrecs3  8319  dfrecs3OLD  8320  tfr1ALT  8347  tfr2ALT  8348  tfr3ALT  8349  on2recsfn  8614  on2recsov  8615  on2ind  8616  on3ind  8617  ordunifi  9238  ordtypelem8  9462  oismo  9477  cantnfcl  9604  leweon  9948  r0weon  9949  ac10ct  9971  dfac12lem2  10081  cflim2  10200  cofsmo  10206  hsmexlem1  10363  smobeth  10523  gruina  10755  ltsopi  10825  finminlem  34793  dnwech  41378  aomclem4  41387  onsupuni  41566  oninfint  41573  epsoon  41590  epirron  41591  oneptr  41592
  Copyright terms: Public domain W3C validator