Metamath Proof Explorer


Theorem ustuqtop5

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

Ref Expression
Hypothesis utopustuq.1 N=pXranvUvp
Assertion ustuqtop5 UUnifOnXpXXNp

Proof

Step Hyp Ref Expression
1 utopustuq.1 N=pXranvUvp
2 ustbasel UUnifOnXX×XU
3 snssi pXpX
4 dfss pXp=pX
5 3 4 sylib pXp=pX
6 incom pX=Xp
7 5 6 eqtr2di pXXp=p
8 snnzg pXp
9 7 8 eqnetrd pXXp
10 9 adantl UUnifOnXpXXp
11 xpima2 XpX×Xp=X
12 10 11 syl UUnifOnXpXX×Xp=X
13 12 eqcomd UUnifOnXpXX=X×Xp
14 imaeq1 w=X×Xwp=X×Xp
15 14 rspceeqv X×XUX=X×XpwUX=wp
16 2 13 15 syl2an2r UUnifOnXpXwUX=wp
17 elfvex UUnifOnXXV
18 1 ustuqtoplem UUnifOnXpXXVXNpwUX=wp
19 17 18 mpidan UUnifOnXpXXNpwUX=wp
20 16 19 mpbird UUnifOnXpXXNp