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

Theorem onuni 7770
Description: The union of an ordinal number is an ordinal number. (Contributed by NM, 29-Sep-2006.)
Assertion
Ref Expression
onuni (𝐴 ∈ On → 𝐴 ∈ On)

Proof of Theorem onuni
StepHypRef Expression
1 onss 7766 . 2 (𝐴 ∈ On → 𝐴 ⊆ On)
2 ssonuni 7761 . 2 (𝐴 ∈ On → (𝐴 ⊆ On → 𝐴 ∈ On))
31, 2mpd 15 1 (𝐴 ∈ On → 𝐴 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2098  wss 3941   cuni 4900  Oncon0 6355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418  ax-un 7719
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-tr 5257  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-ord 6358  df-on 6359
This theorem is referenced by:  onuninsuci  7823  oeeulem  8597  cnfcom3lem  9695  rankxpsuc  9874  dfac12lem2  10136  ttukeylem3  10503  r1limwun  10728  ontgval  35816  ordtoplem  35820  ordcmp  35832  1oequni2o  36749  rdgsucuni  36750  aomclem1  42346  omlimcl2  42540  onsucf1lem  42568  onsucf1olem  42569  onov0suclim  42573  dflim5  42628
  Copyright terms: Public domain W3C validator