Metamath Proof Explorer

Theorem ustimasn

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

Ref Expression
Assertion ustimasn ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → V P ⊆ X

Proof

Step Hyp Ref Expression
1 imassrn ⊢ V P ⊆ ran ⁡ V
2 ustssxp ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → V ⊆ X × X
3 2 3adant3 ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → V ⊆ X × X
4 rnss ⊢ V ⊆ X × X → ran ⁡ V ⊆ ran ⁡ X × X
5 rnxpid ⊢ ran ⁡ X × X = X
6 4 5 sseqtrdi ⊢ V ⊆ X × X → ran ⁡ V ⊆ X
7 3 6 syl ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → ran ⁡ V ⊆ X
8 1 7 sstrid ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ P ∈ X → V P ⊆ X