Theorem ustimasn

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

	Ref	Expression
Assertion	ustimasn	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑉 “ { 𝑃 } ) ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		imassrn	⊢ ( 𝑉 “ { 𝑃 } ) ⊆ ran 𝑉
2		ustssxp	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( 𝑋 × 𝑋 ) )
3	2	3adant3	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → 𝑉 ⊆ ( 𝑋 × 𝑋 ) )
4		rnss	⊢ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) → ran 𝑉 ⊆ ran ( 𝑋 × 𝑋 ) )
5		rnxpid	⊢ ran ( 𝑋 × 𝑋 ) = 𝑋
6	4 5	sseqtrdi	⊢ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) → ran 𝑉 ⊆ 𝑋 )
7	3 6	syl	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ran 𝑉 ⊆ 𝑋 )
8	1 7	sstrid	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋 ) → ( 𝑉 “ { 𝑃 } ) ⊆ 𝑋 )