# Metamath Proof Explorer

## Theorem ustimasn

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

Ref Expression
Assertion ustimasn ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {P}\in {X}\right)\to {V}\left[\left\{{P}\right\}\right]\subseteq {X}$

### Proof

Step Hyp Ref Expression
1 imassrn ${⊢}{V}\left[\left\{{P}\right\}\right]\subseteq \mathrm{ran}{V}$
2 ustssxp ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {V}\subseteq {X}×{X}$
3 2 3adant3 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {P}\in {X}\right)\to {V}\subseteq {X}×{X}$
4 rnss ${⊢}{V}\subseteq {X}×{X}\to \mathrm{ran}{V}\subseteq \mathrm{ran}\left({X}×{X}\right)$
5 rnxpid ${⊢}\mathrm{ran}\left({X}×{X}\right)={X}$
6 4 5 sseqtrdi ${⊢}{V}\subseteq {X}×{X}\to \mathrm{ran}{V}\subseteq {X}$
7 3 6 syl ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {P}\in {X}\right)\to \mathrm{ran}{V}\subseteq {X}$
8 1 7 sstrid ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\wedge {P}\in {X}\right)\to {V}\left[\left\{{P}\right\}\right]\subseteq {X}$