Metamath Proof Explorer

Theorem ustuqtop0

Description: Lemma for ustuqtop . (Contributed by Thierry Arnoux, 11-Jan-2018)

Ref Expression
Hypothesis utopustuq.1 ⊢N=p∈X⟼ran⁡v∈U⟼vp
Assertion ustuqtop0 ⊢U∈UnifOn⁡X→N:X⟶𝒫𝒫X

Proof

Step Hyp Ref Expression
1 utopustuq.1 ⊢N=p∈X⟼ran⁡v∈U⟼vp
2 ustimasn ⊢U∈UnifOn⁡X∧v∈U∧p∈X→vp⊆X
3 2 3expa ⊢U∈UnifOn⁡X∧v∈U∧p∈X→vp⊆X
4 3 an32s ⊢U∈UnifOn⁡X∧p∈X∧v∈U→vp⊆X
5 vex ⊢v∈V
6 5 imaex ⊢vp∈V
7 6 elpw ⊢vp∈𝒫X↔vp⊆X
8 4 7 sylibr ⊢U∈UnifOn⁡X∧p∈X∧v∈U→vp∈𝒫X
9 8 ralrimiva ⊢U∈UnifOn⁡X∧p∈X→∀v∈Uvp∈𝒫X
10 eqid ⊢v∈U⟼vp=v∈U⟼vp
11 10 rnmptss ⊢∀v∈Uvp∈𝒫X→ran⁡v∈U⟼vp⊆𝒫X
12 9 11 syl ⊢U∈UnifOn⁡X∧p∈X→ran⁡v∈U⟼vp⊆𝒫X
13 mptexg ⊢U∈UnifOn⁡X→v∈U⟼vp∈V
14 rnexg ⊢v∈U⟼vp∈V→ran⁡v∈U⟼vp∈V
15 elpwg ⊢ran⁡v∈U⟼vp∈V→ran⁡v∈U⟼vp∈𝒫𝒫X↔ran⁡v∈U⟼vp⊆𝒫X
16 13 14 15 3syl ⊢U∈UnifOn⁡X→ran⁡v∈U⟼vp∈𝒫𝒫X↔ran⁡v∈U⟼vp⊆𝒫X
17 16 adantr ⊢U∈UnifOn⁡X∧p∈X→ran⁡v∈U⟼vp∈𝒫𝒫X↔ran⁡v∈U⟼vp⊆𝒫X
18 12 17 mpbird ⊢U∈UnifOn⁡X∧p∈X→ran⁡v∈U⟼vp∈𝒫𝒫X
19 18 1 fmptd ⊢U∈UnifOn⁡X→N:X⟶𝒫𝒫X