# Metamath Proof Explorer

## Theorem unirnfdomd

Description: The union of the range of a function from an infinite set into the class of finite sets is dominated by its domain. Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses unirnfdomd.1 ${⊢}{\phi }\to {F}:{T}⟶\mathrm{Fin}$
unirnfdomd.2 ${⊢}{\phi }\to ¬{T}\in \mathrm{Fin}$
unirnfdomd.3 ${⊢}{\phi }\to {T}\in {V}$
Assertion unirnfdomd ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\preccurlyeq {T}$

### Proof

Step Hyp Ref Expression
1 unirnfdomd.1 ${⊢}{\phi }\to {F}:{T}⟶\mathrm{Fin}$
2 unirnfdomd.2 ${⊢}{\phi }\to ¬{T}\in \mathrm{Fin}$
3 unirnfdomd.3 ${⊢}{\phi }\to {T}\in {V}$
4 1 ffnd ${⊢}{\phi }\to {F}Fn{T}$
5 fnex ${⊢}\left({F}Fn{T}\wedge {T}\in {V}\right)\to {F}\in \mathrm{V}$
6 4 3 5 syl2anc ${⊢}{\phi }\to {F}\in \mathrm{V}$
7 rnexg ${⊢}{F}\in \mathrm{V}\to \mathrm{ran}{F}\in \mathrm{V}$
8 6 7 syl ${⊢}{\phi }\to \mathrm{ran}{F}\in \mathrm{V}$
9 frn ${⊢}{F}:{T}⟶\mathrm{Fin}\to \mathrm{ran}{F}\subseteq \mathrm{Fin}$
10 dfss3 ${⊢}\mathrm{ran}{F}\subseteq \mathrm{Fin}↔\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{Fin}$
11 9 10 sylib ${⊢}{F}:{T}⟶\mathrm{Fin}\to \forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{Fin}$
12 fict ${⊢}{x}\in \mathrm{Fin}\to {x}\preccurlyeq \mathrm{\omega }$
13 12 ralimi ${⊢}\forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{Fin}\to \forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{x}\preccurlyeq \mathrm{\omega }$
14 1 11 13 3syl ${⊢}{\phi }\to \forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{x}\preccurlyeq \mathrm{\omega }$
15 unidom ${⊢}\left(\mathrm{ran}{F}\in \mathrm{V}\wedge \forall {x}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{x}\preccurlyeq \mathrm{\omega }\right)\to \bigcup \mathrm{ran}{F}\preccurlyeq \left(\mathrm{ran}{F}×\mathrm{\omega }\right)$
16 8 14 15 syl2anc ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\preccurlyeq \left(\mathrm{ran}{F}×\mathrm{\omega }\right)$
17 fnrndomg ${⊢}{T}\in {V}\to \left({F}Fn{T}\to \mathrm{ran}{F}\preccurlyeq {T}\right)$
18 3 4 17 sylc ${⊢}{\phi }\to \mathrm{ran}{F}\preccurlyeq {T}$
19 omex ${⊢}\mathrm{\omega }\in \mathrm{V}$
20 19 xpdom1 ${⊢}\mathrm{ran}{F}\preccurlyeq {T}\to \left(\mathrm{ran}{F}×\mathrm{\omega }\right)\preccurlyeq \left({T}×\mathrm{\omega }\right)$
21 18 20 syl ${⊢}{\phi }\to \left(\mathrm{ran}{F}×\mathrm{\omega }\right)\preccurlyeq \left({T}×\mathrm{\omega }\right)$
22 domtr ${⊢}\left(\bigcup \mathrm{ran}{F}\preccurlyeq \left(\mathrm{ran}{F}×\mathrm{\omega }\right)\wedge \left(\mathrm{ran}{F}×\mathrm{\omega }\right)\preccurlyeq \left({T}×\mathrm{\omega }\right)\right)\to \bigcup \mathrm{ran}{F}\preccurlyeq \left({T}×\mathrm{\omega }\right)$
23 16 21 22 syl2anc ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\preccurlyeq \left({T}×\mathrm{\omega }\right)$
24 infinf ${⊢}{T}\in {V}\to \left(¬{T}\in \mathrm{Fin}↔\mathrm{\omega }\preccurlyeq {T}\right)$
25 3 24 syl ${⊢}{\phi }\to \left(¬{T}\in \mathrm{Fin}↔\mathrm{\omega }\preccurlyeq {T}\right)$
26 2 25 mpbid ${⊢}{\phi }\to \mathrm{\omega }\preccurlyeq {T}$
27 xpdom2g ${⊢}\left({T}\in {V}\wedge \mathrm{\omega }\preccurlyeq {T}\right)\to \left({T}×\mathrm{\omega }\right)\preccurlyeq \left({T}×{T}\right)$
28 3 26 27 syl2anc ${⊢}{\phi }\to \left({T}×\mathrm{\omega }\right)\preccurlyeq \left({T}×{T}\right)$
29 domtr ${⊢}\left(\bigcup \mathrm{ran}{F}\preccurlyeq \left({T}×\mathrm{\omega }\right)\wedge \left({T}×\mathrm{\omega }\right)\preccurlyeq \left({T}×{T}\right)\right)\to \bigcup \mathrm{ran}{F}\preccurlyeq \left({T}×{T}\right)$
30 23 28 29 syl2anc ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\preccurlyeq \left({T}×{T}\right)$
31 infxpidm ${⊢}\mathrm{\omega }\preccurlyeq {T}\to \left({T}×{T}\right)\approx {T}$
32 26 31 syl ${⊢}{\phi }\to \left({T}×{T}\right)\approx {T}$
33 domentr ${⊢}\left(\bigcup \mathrm{ran}{F}\preccurlyeq \left({T}×{T}\right)\wedge \left({T}×{T}\right)\approx {T}\right)\to \bigcup \mathrm{ran}{F}\preccurlyeq {T}$
34 30 32 33 syl2anc ${⊢}{\phi }\to \bigcup \mathrm{ran}{F}\preccurlyeq {T}$