Metamath Proof Explorer


Theorem ustuqtop1

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

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

Proof

Step Hyp Ref Expression
1 utopustuq.1 N = p X ran v U v p
2 simpl1l U UnifOn X p X a b b X a N p w U a = w p U UnifOn X
3 2 3anassrs U UnifOn X p X a b b X a N p w U a = w p U UnifOn X
4 simplr U UnifOn X p X a b b X a N p w U a = w p w U
5 ustssxp U UnifOn X w U w X × X
6 3 4 5 syl2anc U UnifOn X p X a b b X a N p w U a = w p w X × X
7 simpl1r U UnifOn X p X a b b X a N p w U a = w p p X
8 7 3anassrs U UnifOn X p X a b b X a N p w U a = w p p X
9 8 snssd U UnifOn X p X a b b X a N p w U a = w p p X
10 simpl3 U UnifOn X p X a b b X a N p w U a = w p b X
11 10 3anassrs U UnifOn X p X a b b X a N p w U a = w p b X
12 xpss12 p X b X p × b X × X
13 9 11 12 syl2anc U UnifOn X p X a b b X a N p w U a = w p p × b X × X
14 6 13 unssd U UnifOn X p X a b b X a N p w U a = w p w p × b X × X
15 ssun1 w w p × b
16 15 a1i U UnifOn X p X a b b X a N p w U a = w p w w p × b
17 ustssel U UnifOn X w U w p × b X × X w w p × b w p × b U
18 17 imp U UnifOn X w U w p × b X × X w w p × b w p × b U
19 3 4 14 16 18 syl31anc U UnifOn X p X a b b X a N p w U a = w p w p × b U
20 simpl2 U UnifOn X p X a b b X a N p w U a = w p a b
21 20 3anassrs U UnifOn X p X a b b X a N p w U a = w p a b
22 ssequn1 a b a b = b
23 22 biimpi a b a b = b
24 id a = w p a = w p
25 inidm p p = p
26 vex p V
27 26 snnz p
28 25 27 eqnetri p p
29 xpima2 p p p × b p = b
30 28 29 mp1i a = w p p × b p = b
31 30 eqcomd a = w p b = p × b p
32 24 31 uneq12d a = w p a b = w p p × b p
33 imaundir w p × b p = w p p × b p
34 32 33 eqtr4di a = w p a b = w p × b p
35 23 34 sylan9req a b a = w p b = w p × b p
36 21 35 sylancom U UnifOn X p X a b b X a N p w U a = w p b = w p × b p
37 imaeq1 u = w p × b u p = w p × b p
38 37 rspceeqv w p × b U b = w p × b p u U b = u p
39 19 36 38 syl2anc U UnifOn X p X a b b X a N p w U a = w p u U b = u p
40 1 ustuqtoplem U UnifOn X p X a V a N p w U a = w p
41 40 elvd U UnifOn X p X a N p w U a = w p
42 41 biimpa U UnifOn X p X a N p w U a = w p
43 42 3ad2antl1 U UnifOn X p X a b b X a N p w U a = w p
44 39 43 r19.29a U UnifOn X p X a b b X a N p u U b = u p
45 1 ustuqtoplem U UnifOn X p X b V b N p u U b = u p
46 45 elvd U UnifOn X p X b N p u U b = u p
47 46 3ad2ant1 U UnifOn X p X a b b X b N p u U b = u p
48 47 adantr U UnifOn X p X a b b X a N p b N p u U b = u p
49 44 48 mpbird U UnifOn X p X a b b X a N p b N p