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 3902  ∪ cuni 4870  Oncon0 6361

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 2734  ax-sep 5255  ax-pr 5402  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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-tr 5217  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365

This theorem is used by:  onuninsuci  7840  oeeulem  8593  cnfcom3lem  9686  rankxpsuc  9868  dfac12lem2  10151  ttukeylem3  10517  r1limwun  10749  ontgval  37058  ordtoplem  37062  ordcmp  37074  1oequni2o  38130  rdgsucuni  38131  aomclem1  43903  omlimcl2  44091  onsucf1lem  44118  onsucf1olem  44119  onov0suclim  44123  dflim5  44178