# Metamath Proof Explorer

## Theorem ssorduni

Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of TakeutiZaring p. 40. (Contributed by NM, 30-May-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion ssorduni ${⊢}{A}\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup {A}$

### Proof

Step Hyp Ref Expression
1 eluni2 ${⊢}{x}\in \bigcup {A}↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}$
2 ssel ${⊢}{A}\subseteq \mathrm{On}\to \left({y}\in {A}\to {y}\in \mathrm{On}\right)$
3 onelss ${⊢}{y}\in \mathrm{On}\to \left({x}\in {y}\to {x}\subseteq {y}\right)$
4 2 3 syl6 ${⊢}{A}\subseteq \mathrm{On}\to \left({y}\in {A}\to \left({x}\in {y}\to {x}\subseteq {y}\right)\right)$
5 anc2r ${⊢}\left({y}\in {A}\to \left({x}\in {y}\to {x}\subseteq {y}\right)\right)\to \left({y}\in {A}\to \left({x}\in {y}\to \left({x}\subseteq {y}\wedge {y}\in {A}\right)\right)\right)$
6 4 5 syl ${⊢}{A}\subseteq \mathrm{On}\to \left({y}\in {A}\to \left({x}\in {y}\to \left({x}\subseteq {y}\wedge {y}\in {A}\right)\right)\right)$
7 ssuni ${⊢}\left({x}\subseteq {y}\wedge {y}\in {A}\right)\to {x}\subseteq \bigcup {A}$
8 6 7 syl8 ${⊢}{A}\subseteq \mathrm{On}\to \left({y}\in {A}\to \left({x}\in {y}\to {x}\subseteq \bigcup {A}\right)\right)$
9 8 rexlimdv ${⊢}{A}\subseteq \mathrm{On}\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to {x}\subseteq \bigcup {A}\right)$
10 1 9 syl5bi ${⊢}{A}\subseteq \mathrm{On}\to \left({x}\in \bigcup {A}\to {x}\subseteq \bigcup {A}\right)$
11 10 ralrimiv ${⊢}{A}\subseteq \mathrm{On}\to \forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq \bigcup {A}$
12 dftr3 ${⊢}\mathrm{Tr}\bigcup {A}↔\forall {x}\in \bigcup {A}\phantom{\rule{.4em}{0ex}}{x}\subseteq \bigcup {A}$
13 11 12 sylibr ${⊢}{A}\subseteq \mathrm{On}\to \mathrm{Tr}\bigcup {A}$
14 onelon ${⊢}\left({y}\in \mathrm{On}\wedge {x}\in {y}\right)\to {x}\in \mathrm{On}$
15 14 ex ${⊢}{y}\in \mathrm{On}\to \left({x}\in {y}\to {x}\in \mathrm{On}\right)$
16 2 15 syl6 ${⊢}{A}\subseteq \mathrm{On}\to \left({y}\in {A}\to \left({x}\in {y}\to {x}\in \mathrm{On}\right)\right)$
17 16 rexlimdv ${⊢}{A}\subseteq \mathrm{On}\to \left(\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\in {y}\to {x}\in \mathrm{On}\right)$
18 1 17 syl5bi ${⊢}{A}\subseteq \mathrm{On}\to \left({x}\in \bigcup {A}\to {x}\in \mathrm{On}\right)$
19 18 ssrdv ${⊢}{A}\subseteq \mathrm{On}\to \bigcup {A}\subseteq \mathrm{On}$
20 ordon ${⊢}\mathrm{Ord}\mathrm{On}$
21 trssord ${⊢}\left(\mathrm{Tr}\bigcup {A}\wedge \bigcup {A}\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{On}\right)\to \mathrm{Ord}\bigcup {A}$
22 21 3exp ${⊢}\mathrm{Tr}\bigcup {A}\to \left(\bigcup {A}\subseteq \mathrm{On}\to \left(\mathrm{Ord}\mathrm{On}\to \mathrm{Ord}\bigcup {A}\right)\right)$
23 20 22 mpii ${⊢}\mathrm{Tr}\bigcup {A}\to \left(\bigcup {A}\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup {A}\right)$
24 13 19 23 sylc ${⊢}{A}\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup {A}$