Metamath Proof Explorer

Theorem ustimasn

Description: Lemma for ustuqtop . (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Assertion ustimasn 
|- ( ( U e. ( UnifOn ` X ) /\ V e. U /\ P e. X ) -> ( V " { P } ) C_ X )

Proof

Step Hyp Ref Expression
1 imassrn 
 |-  ( V " { P } ) C_ ran V
2 ustssxp 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( X X. X ) )
3 2 3adant3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ P e. X ) -> V C_ ( X X. X ) )
4 rnss 
 |-  ( V C_ ( X X. X ) -> ran V C_ ran ( X X. X ) )
5 rnxpid 
 |-  ran ( X X. X ) = X
6 4 5 sseqtrdi 
 |-  ( V C_ ( X X. X ) -> ran V C_ X )
7 3 6 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ P e. X ) -> ran V C_ X )
8 1 7 sstrid 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ P e. X ) -> ( V " { P } ) C_ X )