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

Theorem ordon 6750
Description: The class of all ordinal numbers is ordinal. Proposition 7.12 of [TakeutiZaring] p. 38, but without using the Axiom of Regularity. (Contributed by NM, 17-May-1994.)
Assertion
Ref Expression
ordon Ord On

Proof of Theorem ordon
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tron 5553 . 2 Tr On
2 onfr 5569 . . 3 E Fr On
3 eloni 5540 . . . . 5 (𝑥 ∈ On → Ord 𝑥)
4 eloni 5540 . . . . 5 (𝑦 ∈ On → Ord 𝑦)
5 ordtri3or 5562 . . . . . 6 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
6 epel 4846 . . . . . . 7 (𝑥 E 𝑦𝑥𝑦)
7 biid 249 . . . . . . 7 (𝑥 = 𝑦𝑥 = 𝑦)
8 epel 4846 . . . . . . 7 (𝑦 E 𝑥𝑦𝑥)
96, 7, 83orbi123i 1244 . . . . . 6 ((𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥) ↔ (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
105, 9sylibr 222 . . . . 5 ((Ord 𝑥 ∧ Ord 𝑦) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
113, 4, 10syl2an 492 . . . 4 ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥))
1211rgen2a 2864 . . 3 𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)
13 dfwe2 6749 . . 3 ( E We On ↔ ( E Fr On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥 E 𝑦𝑥 = 𝑦𝑦 E 𝑥)))
142, 12, 13mpbir2an 956 . 2 E We On
15 df-ord 5533 . 2 (Ord On ↔ (Tr On ∧ E We On))
161, 14, 15mpbir2an 956 1 Ord On
Colors of variables: wff setvar class
Syntax hints:  wa 382  w3o 1029  wcel 1938  wral 2800   class class class wbr 4481  Tr wtr 4578   E cep 4841   Fr wfr 4888   We wwe 4890  Ord word 5529  Oncon0 5530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pr 4732  ax-un 6723
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-tr 4579  df-eprel 4843  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-ord 5533  df-on 5534
This theorem is referenced by:  epweon  6751  onprc  6752  ssorduni  6753  ordeleqon  6756  ordsson  6757  onint  6763  suceloni  6781  limon  6804  tfi  6821  ordom  6842  ordtypelem2  8183  hartogs  8208  card2on  8218  tskwe  8535  alephsmo  8684  ondomon  9140  dford3lem2  36502  dford3  36503
  Copyright terms: Public domain W3C validator