# 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 = dom U. U
Assertion ustbas
|- ( U e. U. ran UnifOn <-> U e. ( UnifOn ` X ) )

### Proof

Step Hyp Ref Expression
1 ustbas.1
|-  X = dom U. U
2 ustfn
|-  UnifOn Fn _V
3 fnfun
|-  ( UnifOn Fn _V -> Fun UnifOn )
4 elunirn
|-  ( Fun UnifOn -> ( U e. U. ran UnifOn <-> E. x e. dom UnifOn U e. ( UnifOn ` x ) ) )
5 2 3 4 mp2b
|-  ( U e. U. ran UnifOn <-> E. x e. dom UnifOn U e. ( UnifOn ` x ) )
6 ustbas2
|-  ( U e. ( UnifOn ` x ) -> x = dom U. U )
7 6 1 syl6eqr
|-  ( U e. ( UnifOn ` x ) -> x = X )
8 7 fveq2d
|-  ( U e. ( UnifOn ` x ) -> ( UnifOn ` x ) = ( UnifOn ` X ) )
9 8 eleq2d
|-  ( U e. ( UnifOn ` x ) -> ( U e. ( UnifOn ` x ) <-> U e. ( UnifOn ` X ) ) )
10 9 ibi
|-  ( U e. ( UnifOn ` x ) -> U e. ( UnifOn ` X ) )
11 10 rexlimivw
|-  ( E. x e. dom UnifOn U e. ( UnifOn ` x ) -> U e. ( UnifOn ` X ) )
12 5 11 sylbi
|-  ( U e. U. ran UnifOn -> U e. ( UnifOn ` X ) )
13 elrnust
|-  ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn )
14 12 13 impbii
|-  ( U e. U. ran UnifOn <-> U e. ( UnifOn ` X ) )