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

Theorem epweon 7795
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 7755, see epweonALT 7796. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7755. (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 6423 . 2 E Fr On
2 df-po 5592 . . . 4 ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
3 eloni 6394 . . . . . . . . 9 (𝑥 ∈ On → Ord 𝑥)
4 ordirr 6402 . . . . . . . . 9 (Ord 𝑥 → ¬ 𝑥𝑥)
53, 4syl 17 . . . . . . . 8 (𝑥 ∈ On → ¬ 𝑥𝑥)
6 epel 5587 . . . . . . . 8 (𝑥 E 𝑥𝑥𝑥)
75, 6sylnibr 329 . . . . . . 7 (𝑥 ∈ On → ¬ 𝑥 E 𝑥)
8 ontr1 6430 . . . . . . . 8 (𝑧 ∈ On → ((𝑥𝑦𝑦𝑧) → 𝑥𝑧))
9 epel 5587 . . . . . . . . 9 (𝑥 E 𝑦𝑥𝑦)
10 epel 5587 . . . . . . . . 9 (𝑦 E 𝑧𝑦𝑧)
119, 10anbi12i 628 . . . . . . . 8 ((𝑥 E 𝑦𝑦 E 𝑧) ↔ (𝑥𝑦𝑦𝑧))
12 epel 5587 . . . . . . . 8 (𝑥 E 𝑧𝑥𝑧)
138, 11, 123imtr4g 296 . . . . . . 7 (𝑧 ∈ On → ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧))
147, 13anim12i 613 . . . . . 6 ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
1514ralrimiva 3146 . . . . 5 (𝑥 ∈ On → ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
1615ralrimivw 3150 . . . 4 (𝑥 ∈ On → ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
172, 16mprgbir 3068 . . 3 E Po On
18 eloni 6394 . . . . 5 (𝑦 ∈ On → Ord 𝑦)
19 ordtri3or 6416 . . . . . 6 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
20 biid 261 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑦)
21 epel 5587 . . . . . . 7 (𝑦 E 𝑥𝑦𝑥)
229, 20, 213orbi123i 1157 . . . . . 6 ((𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥) ↔ (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
2319, 22sylibr 234 . . . . 5 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
243, 18, 23syl2an 596 . . . 4 ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
2524rgen2 3199 . . 3 𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)
26 df-so 5593 . . 3 ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)))
2717, 25, 26mpbir2an 711 . 2 E Or On
28 df-we 5639 . 2 ( E We On ↔ ( E Fr On ∧ E Or On))
291, 27, 28mpbir2an 711 1 E We On
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  w3o 1086  wcel 2108  wral 3061   class class class wbr 5143   E cep 5583   Po wpo 5590   Or wor 5591   Fr wfr 5634   We wwe 5636  Ord word 6383  Oncon0 6384
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388
This theorem is referenced by:  ordon  7797  dford5  7804  omsinds  7908  onnseq  8384  dfrecs3  8412  dfrecs3OLD  8413  tfr1ALT  8440  tfr2ALT  8441  tfr3ALT  8442  on2recsfn  8705  on2recsov  8706  on2ind  8707  on3ind  8708  ordunifi  9326  ordtypelem8  9565  oismo  9580  cantnfcl  9707  leweon  10051  r0weon  10052  ac10ct  10074  dfac12lem2  10185  cflim2  10303  cofsmo  10309  hsmexlem1  10466  smobeth  10626  gruina  10858  ltsopi  10928  finminlem  36319  dnwech  43060  aomclem4  43069  onsupuni  43241  oninfint  43248  epsoon  43265  epirron  43266  oneptr  43267  oaun3lem1  43387
  Copyright terms: Public domain W3C validator