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

Theorem epweon 7625
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. (Contributed by NM, 1-Nov-2003.) Avoid ax-un 7588. (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 6305 . 2 E Fr On
2 df-po 5503 . . . 4 ( E Po On ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
3 eloni 6276 . . . . . . . . 9 (𝑥 ∈ On → Ord 𝑥)
4 ordirr 6284 . . . . . . . . 9 (Ord 𝑥 → ¬ 𝑥𝑥)
53, 4syl 17 . . . . . . . 8 (𝑥 ∈ On → ¬ 𝑥𝑥)
6 epel 5498 . . . . . . . 8 (𝑥 E 𝑥𝑥𝑥)
75, 6sylnibr 329 . . . . . . 7 (𝑥 ∈ On → ¬ 𝑥 E 𝑥)
8 ontr1 6312 . . . . . . . 8 (𝑧 ∈ On → ((𝑥𝑦𝑦𝑧) → 𝑥𝑧))
9 epel 5498 . . . . . . . . 9 (𝑥 E 𝑦𝑥𝑦)
10 epel 5498 . . . . . . . . 9 (𝑦 E 𝑧𝑦𝑧)
119, 10anbi12i 627 . . . . . . . 8 ((𝑥 E 𝑦𝑦 E 𝑧) ↔ (𝑥𝑦𝑦𝑧))
12 epel 5498 . . . . . . . 8 (𝑥 E 𝑧𝑥𝑧)
138, 11, 123imtr4g 296 . . . . . . 7 (𝑧 ∈ On → ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧))
147, 13anim12i 613 . . . . . 6 ((𝑥 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
1514ralrimiva 3103 . . . . 5 (𝑥 ∈ On → ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
1615ralrimivw 3104 . . . 4 (𝑥 ∈ On → ∀𝑦 ∈ On ∀𝑧 ∈ On (¬ 𝑥 E 𝑥 ∧ ((𝑥 E 𝑦𝑦 E 𝑧) → 𝑥 E 𝑧)))
172, 16mprgbir 3079 . . 3 E Po On
18 eloni 6276 . . . . 5 (𝑦 ∈ On → Ord 𝑦)
19 ordtri3or 6298 . . . . . 6 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
20 biid 260 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑦)
21 epel 5498 . . . . . . 7 (𝑦 E 𝑥𝑦𝑥)
229, 20, 213orbi123i 1155 . . . . . 6 ((𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥) ↔ (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
2319, 22sylibr 233 . . . . 5 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
243, 18, 23syl2an 596 . . . 4 ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
2524rgen2 3120 . . 3 𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)
26 df-so 5504 . . 3 ( E Or On ↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)))
2717, 25, 26mpbir2an 708 . 2 E Or On
28 df-we 5546 . 2 ( E We On ↔ ( E Fr On ∧ E Or On))
291, 27, 28mpbir2an 708 1 E We On
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3o 1085  wcel 2106  wral 3064   class class class wbr 5074   E cep 5494   Po wpo 5501   Or wor 5502   Fr wfr 5541   We wwe 5543  Ord word 6265  Oncon0 6266
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269  df-on 6270
This theorem is referenced by:  ordon  7627  omsinds  7733  omsindsOLD  7734  onnseq  8175  dfrecs3  8203  dfrecs3OLD  8204  tfr1ALT  8231  tfr2ALT  8232  tfr3ALT  8233  ordunifi  9064  ordtypelem8  9284  oismo  9299  cantnfcl  9425  leweon  9767  r0weon  9768  ac10ct  9790  dfac12lem2  9900  cflim2  10019  cofsmo  10025  hsmexlem1  10182  smobeth  10342  gruina  10574  ltsopi  10644  dford5  33671  on2recsfn  33826  on2recsov  33827  on2ind  33828  on3ind  33829  finminlem  34507  dnwech  40873  aomclem4  40882
  Copyright terms: Public domain W3C validator