Theorem onuni 7791

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

Step	Hyp	Ref	Expression
1		onss 7788	. 2 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On)
2		ssonuni 7783	. 2 ⊢ (𝐴 ∈ On → (𝐴 ⊆ On → ∪ 𝐴 ∈ On))
3	1, 2	mpd 16	1 ⊢ (𝐴 ∈ On → ∪ 𝐴 ∈ On)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  ∪ cuni 4867  Oncon0 6355

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6358  df-on 6359

This theorem is used by:  onuninsuci  7840  oeeulem  8594  cnfcom3lem  9688  rankxpsuc  9880  dfac12lem2  10204  ttukeylem3  10570  r1limwun  10802  ontgval  37189  ordtoplem  37193  ordcmp  37205  1oequni2o  38259  rdgsucuni  38260  aomclem1  44014  omlimcl2  44202  onsucf1lem  44229  onsucf1olem  44230  onov0suclim  44234  dflim5  44289