# Metamath Proof Explorer

## Theorem ustbas

Description: Recover the base of an uniform structure U . U. ran UnifOn is to UnifOn what Top is to TopOn . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Hypothesis ustbas.1 ${⊢}{X}=\mathrm{dom}\bigcup {U}$
Assertion ustbas ${⊢}{U}\in \bigcup \mathrm{ran}\mathrm{UnifOn}↔{U}\in \mathrm{UnifOn}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 ustbas.1 ${⊢}{X}=\mathrm{dom}\bigcup {U}$
2 ustfn ${⊢}\mathrm{UnifOn}Fn\mathrm{V}$
3 fnfun ${⊢}\mathrm{UnifOn}Fn\mathrm{V}\to \mathrm{Fun}\mathrm{UnifOn}$
4 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)$
5 2 3 4 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)$
6 ustbas2 ${⊢}{U}\in \mathrm{UnifOn}\left({x}\right)\to {x}=\mathrm{dom}\bigcup {U}$
7 6 1 syl6eqr ${⊢}{U}\in \mathrm{UnifOn}\left({x}\right)\to {x}={X}$
8 7 fveq2d ${⊢}{U}\in \mathrm{UnifOn}\left({x}\right)\to \mathrm{UnifOn}\left({x}\right)=\mathrm{UnifOn}\left({X}\right)$
9 8 eleq2d ${⊢}{U}\in \mathrm{UnifOn}\left({x}\right)\to \left({U}\in \mathrm{UnifOn}\left({x}\right)↔{U}\in \mathrm{UnifOn}\left({X}\right)\right)$
10 9 ibi ${⊢}{U}\in \mathrm{UnifOn}\left({x}\right)\to {U}\in \mathrm{UnifOn}\left({X}\right)$
11 10 rexlimivw ${⊢}\exists {x}\in \mathrm{dom}\mathrm{UnifOn}\phantom{\rule{.4em}{0ex}}{U}\in \mathrm{UnifOn}\left({x}\right)\to {U}\in \mathrm{UnifOn}\left({X}\right)$
12 5 11 sylbi ${⊢}{U}\in \bigcup \mathrm{ran}\mathrm{UnifOn}\to {U}\in \mathrm{UnifOn}\left({X}\right)$
13 elrnust ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {U}\in \bigcup \mathrm{ran}\mathrm{UnifOn}$
14 12 13 impbii ${⊢}{U}\in \bigcup \mathrm{ran}\mathrm{UnifOn}↔{U}\in \mathrm{UnifOn}\left({X}\right)$