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 ) )