# Metamath Proof Explorer

## Theorem omabslem

Description: Lemma for omabs . (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Assertion omabslem ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge {A}\in \mathrm{\omega }\wedge \varnothing \in {A}\right)\to {A}{\cdot }_{𝑜}\mathrm{\omega }=\mathrm{\omega }$

### Proof

Step Hyp Ref Expression
1 nnon ${⊢}{A}\in \mathrm{\omega }\to {A}\in \mathrm{On}$
2 limom ${⊢}\mathrm{Lim}\mathrm{\omega }$
3 2 jctr ${⊢}\mathrm{\omega }\in \mathrm{On}\to \left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{Lim}\mathrm{\omega }\right)$
4 omlim ${⊢}\left({A}\in \mathrm{On}\wedge \left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{Lim}\mathrm{\omega }\right)\right)\to {A}{\cdot }_{𝑜}\mathrm{\omega }=\bigcup _{{x}\in \mathrm{\omega }}\left({A}{\cdot }_{𝑜}{x}\right)$
5 1 3 4 syl2an ${⊢}\left({A}\in \mathrm{\omega }\wedge \mathrm{\omega }\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\mathrm{\omega }=\bigcup _{{x}\in \mathrm{\omega }}\left({A}{\cdot }_{𝑜}{x}\right)$
6 ordom ${⊢}\mathrm{Ord}\mathrm{\omega }$
7 nnmcl ${⊢}\left({A}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}{x}\in \mathrm{\omega }$
8 ordelss ${⊢}\left(\mathrm{Ord}\mathrm{\omega }\wedge {A}{\cdot }_{𝑜}{x}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}{x}\subseteq \mathrm{\omega }$
9 6 7 8 sylancr ${⊢}\left({A}\in \mathrm{\omega }\wedge {x}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}{x}\subseteq \mathrm{\omega }$
10 9 ralrimiva ${⊢}{A}\in \mathrm{\omega }\to \forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}{x}\subseteq \mathrm{\omega }$
11 iunss ${⊢}\bigcup _{{x}\in \mathrm{\omega }}\left({A}{\cdot }_{𝑜}{x}\right)\subseteq \mathrm{\omega }↔\forall {x}\in \mathrm{\omega }\phantom{\rule{.4em}{0ex}}{A}{\cdot }_{𝑜}{x}\subseteq \mathrm{\omega }$
12 10 11 sylibr ${⊢}{A}\in \mathrm{\omega }\to \bigcup _{{x}\in \mathrm{\omega }}\left({A}{\cdot }_{𝑜}{x}\right)\subseteq \mathrm{\omega }$
13 12 adantr ${⊢}\left({A}\in \mathrm{\omega }\wedge \mathrm{\omega }\in \mathrm{On}\right)\to \bigcup _{{x}\in \mathrm{\omega }}\left({A}{\cdot }_{𝑜}{x}\right)\subseteq \mathrm{\omega }$
14 5 13 eqsstrd ${⊢}\left({A}\in \mathrm{\omega }\wedge \mathrm{\omega }\in \mathrm{On}\right)\to {A}{\cdot }_{𝑜}\mathrm{\omega }\subseteq \mathrm{\omega }$
15 14 ancoms ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge {A}\in \mathrm{\omega }\right)\to {A}{\cdot }_{𝑜}\mathrm{\omega }\subseteq \mathrm{\omega }$
16 15 3adant3 ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge {A}\in \mathrm{\omega }\wedge \varnothing \in {A}\right)\to {A}{\cdot }_{𝑜}\mathrm{\omega }\subseteq \mathrm{\omega }$
17 omword2 ${⊢}\left(\left(\mathrm{\omega }\in \mathrm{On}\wedge {A}\in \mathrm{On}\right)\wedge \varnothing \in {A}\right)\to \mathrm{\omega }\subseteq {A}{\cdot }_{𝑜}\mathrm{\omega }$
18 17 3impa ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge {A}\in \mathrm{On}\wedge \varnothing \in {A}\right)\to \mathrm{\omega }\subseteq {A}{\cdot }_{𝑜}\mathrm{\omega }$
19 1 18 syl3an2 ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge {A}\in \mathrm{\omega }\wedge \varnothing \in {A}\right)\to \mathrm{\omega }\subseteq {A}{\cdot }_{𝑜}\mathrm{\omega }$
20 16 19 eqssd ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge {A}\in \mathrm{\omega }\wedge \varnothing \in {A}\right)\to {A}{\cdot }_{𝑜}\mathrm{\omega }=\mathrm{\omega }$