Metamath Proof Explorer


Theorem ustuqtop3

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

Ref Expression
Hypothesis utopustuq.1 N = p X ran v U v p
Assertion ustuqtop3 U UnifOn X p X a N p p a

Proof

Step Hyp Ref Expression
1 utopustuq.1 N = p X ran v U v p
2 fnresi I X Fn X
3 fnsnfv I X Fn X p X I X p = I X p
4 2 3 mpan p X I X p = I X p
5 4 ad4antlr U UnifOn X p X a N p w U a = w p I X p = I X p
6 ustdiag U UnifOn X w U I X w
7 6 ad5ant14 U UnifOn X p X a N p w U a = w p I X w
8 imass1 I X w I X p w p
9 7 8 syl U UnifOn X p X a N p w U a = w p I X p w p
10 5 9 eqsstrd U UnifOn X p X a N p w U a = w p I X p w p
11 fvex I X p V
12 11 snss I X p w p I X p w p
13 10 12 sylibr U UnifOn X p X a N p w U a = w p I X p w p
14 fvresi p X I X p = p
15 14 eqcomd p X p = I X p
16 15 ad4antlr U UnifOn X p X a N p w U a = w p p = I X p
17 simpr U UnifOn X p X a N p w U a = w p a = w p
18 13 16 17 3eltr4d U UnifOn X p X a N p w U a = w p p a
19 1 ustuqtoplem U UnifOn X p X a V a N p w U a = w p
20 19 elvd U UnifOn X p X a N p w U a = w p
21 20 biimpa U UnifOn X p X a N p w U a = w p
22 18 21 r19.29a U UnifOn X p X a N p p a