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

Theorem epweon 7489
 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.)
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 6223 . 2 E Fr On
2 eloni 6194 . . . 4 (𝑥 ∈ On → Ord 𝑥)
3 eloni 6194 . . . 4 (𝑦 ∈ On → Ord 𝑦)
4 ordtri3or 6216 . . . . 5 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
5 epel 5462 . . . . . 6 (𝑥 E 𝑦𝑥𝑦)
6 biid 263 . . . . . 6 (𝑥 = 𝑦𝑥 = 𝑦)
7 epel 5462 . . . . . 6 (𝑦 E 𝑥𝑦𝑥)
85, 6, 73orbi123i 1151 . . . . 5 ((𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥) ↔ (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
94, 8sylibr 236 . . . 4 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
102, 3, 9syl2an 597 . . 3 ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
1110rgen2 3201 . 2 𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)
12 dfwe2 7488 . 2 ( E We On ↔ ( E Fr On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)))
131, 11, 12mpbir2an 709 1 E We On
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 398   ∨ w3o 1081   ∈ wcel 2108  ∀wral 3136   class class class wbr 5057   E cep 5457   Fr wfr 5504   We wwe 5506  Ord word 6183  Oncon0 6184 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7453 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188 This theorem is referenced by:  ordon  7490  omsinds  7592  onnseq  7973  dfrecs3  8001  tfr1ALT  8028  tfr2ALT  8029  tfr3ALT  8030  ordunifi  8760  ordtypelem8  8981  oismo  8996  cantnfcl  9122  leweon  9429  r0weon  9430  ac10ct  9452  dfac12lem2  9562  cflim2  9677  cofsmo  9683  hsmexlem1  9840  smobeth  10000  gruina  10232  ltsopi  10302  dford5  32950  finminlem  33659  dnwech  39638  aomclem4  39647
 Copyright terms: Public domain W3C validator