Metamath Proof Explorer


Theorem ustuqtop2

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 ustuqtop2 U UnifOn X p X fi N p N p

Proof

Step Hyp Ref Expression
1 utopustuq.1 N = p X ran v U v p
2 simp-6l U UnifOn X p X a N p b N p w U a = w p u U b = u p U UnifOn X p X
3 simp-7l U UnifOn X p X a N p b N p w U a = w p u U b = u p U UnifOn X
4 simp-4r U UnifOn X p X a N p b N p w U a = w p u U b = u p w U
5 simplr U UnifOn X p X a N p b N p w U a = w p u U b = u p u U
6 ustincl U UnifOn X w U u U w u U
7 3 4 5 6 syl3anc U UnifOn X p X a N p b N p w U a = w p u U b = u p w u U
8 ineq12 a = w p b = u p a b = w p u p
9 inimasn p V w u p = w p u p
10 9 elv w u p = w p u p
11 8 10 eqtr4di a = w p b = u p a b = w u p
12 11 ad4ant24 U UnifOn X p X a N p b N p w U a = w p u U b = u p a b = w u p
13 imaeq1 x = w u x p = w u p
14 13 rspceeqv w u U a b = w u p x U a b = x p
15 7 12 14 syl2anc U UnifOn X p X a N p b N p w U a = w p u U b = u p x U a b = x p
16 vex a V
17 16 inex1 a b V
18 1 ustuqtoplem U UnifOn X p X a b V a b N p x U a b = x p
19 17 18 mpan2 U UnifOn X p X a b N p x U a b = x p
20 19 biimpar U UnifOn X p X x U a b = x p a b N p
21 2 15 20 syl2anc U UnifOn X p X a N p b N p w U a = w p u U b = u p a b N p
22 1 ustuqtoplem U UnifOn X p X b V b N p u U b = u p
23 22 elvd U UnifOn X p X b N p u U b = u p
24 23 biimpa U UnifOn X p X b N p u U b = u p
25 24 ad5ant13 U UnifOn X p X a N p b N p w U a = w p u U b = u p
26 21 25 r19.29a U UnifOn X p X a N p b N p w U a = w p a b N p
27 1 ustuqtoplem U UnifOn X p X a V a N p w U a = w p
28 27 elvd U UnifOn X p X a N p w U a = w p
29 28 biimpa U UnifOn X p X a N p w U a = w p
30 29 adantr U UnifOn X p X a N p b N p w U a = w p
31 26 30 r19.29a U UnifOn X p X a N p b N p a b N p
32 31 ralrimiva U UnifOn X p X a N p b N p a b N p
33 32 ralrimiva U UnifOn X p X a N p b N p a b N p
34 fvex N p V
35 inficl N p V a N p b N p a b N p fi N p = N p
36 34 35 ax-mp a N p b N p a b N p fi N p = N p
37 33 36 sylib U UnifOn X p X fi N p = N p
38 eqimss fi N p = N p fi N p N p
39 37 38 syl U UnifOn X p X fi N p N p