# Metamath Proof Explorer

## Theorem elrnust

Description: First direction for ustbas . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion elrnust ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {U}\in \bigcup \mathrm{ran}\mathrm{UnifOn}$

### Proof

Step Hyp Ref Expression
1 elfvdm ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}\in \mathrm{dom}\mathrm{UnifOn}$
2 fveq2 ${⊢}{x}={X}\to \mathrm{UnifOn}\left({x}\right)=\mathrm{UnifOn}\left({X}\right)$
3 2 eleq2d ${⊢}{x}={X}\to \left({U}\in \mathrm{UnifOn}\left({x}\right)↔{U}\in \mathrm{UnifOn}\left({X}\right)\right)$
4 3 rspcev ${⊢}\left({X}\in \mathrm{dom}\mathrm{UnifOn}\wedge {U}\in \mathrm{UnifOn}\left({X}\right)\right)\to \exists {x}\in \mathrm{dom}\mathrm{UnifOn}\phantom{\rule{.4em}{0ex}}{U}\in \mathrm{UnifOn}\left({x}\right)$
5 1 4 mpancom ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \exists {x}\in \mathrm{dom}\mathrm{UnifOn}\phantom{\rule{.4em}{0ex}}{U}\in \mathrm{UnifOn}\left({x}\right)$
6 ustfn ${⊢}\mathrm{UnifOn}Fn\mathrm{V}$
7 fnfun ${⊢}\mathrm{UnifOn}Fn\mathrm{V}\to \mathrm{Fun}\mathrm{UnifOn}$
8 elunirn ${⊢}\mathrm{Fun}\mathrm{UnifOn}\to \left({U}\in \bigcup \mathrm{ran}\mathrm{UnifOn}↔\exists {x}\in \mathrm{dom}\mathrm{UnifOn}\phantom{\rule{.4em}{0ex}}{U}\in \mathrm{UnifOn}\left({x}\right)\right)$
9 6 7 8 mp2b ${⊢}{U}\in \bigcup \mathrm{ran}\mathrm{UnifOn}↔\exists {x}\in \mathrm{dom}\mathrm{UnifOn}\phantom{\rule{.4em}{0ex}}{U}\in \mathrm{UnifOn}\left({x}\right)$
10 5 9 sylibr ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {U}\in \bigcup \mathrm{ran}\mathrm{UnifOn}$