This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtr4di 
 |-  ( 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 elfvunirn 
 |-  ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn )
14 12 13 impbii 
 |-  ( U e. U. ran UnifOn <-> U e. ( UnifOn ` X ) )