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 v p
Assertion ustuqtop0 U UnifOn X N : X 𝒫 𝒫 X

Proof

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