Metamath Proof Explorer

Theorem elrnust

Description: First direction for ustbas . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion elrnust 
|- ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( U e. ( UnifOn ` X ) -> X e. dom UnifOn )
2 fveq2 
 |-  ( x = X -> ( UnifOn ` x ) = ( UnifOn ` X ) )
3 2 eleq2d 
 |-  ( x = X -> ( U e. ( UnifOn ` x ) <-> U e. ( UnifOn ` X ) ) )
4 3 rspcev 
 |-  ( ( X e. dom UnifOn /\ U e. ( UnifOn ` X ) ) -> E. x e. dom UnifOn U e. ( UnifOn ` x ) )
5 1 4 mpancom 
 |-  ( U e. ( UnifOn ` X ) -> E. x e. dom UnifOn U e. ( UnifOn ` x ) )
6 ustfn 
 |-  UnifOn Fn _V
7 fnfun 
 |-  ( UnifOn Fn _V -> Fun UnifOn )
8 elunirn 
 |-  ( Fun UnifOn -> ( U e. U. ran UnifOn <-> E. x e. dom UnifOn U e. ( UnifOn ` x ) ) )
9 6 7 8 mp2b 
 |-  ( U e. U. ran UnifOn <-> E. x e. dom UnifOn U e. ( UnifOn ` x ) )
10 5 9 sylibr 
 |-  ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn )