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