Metamath Proof Explorer

Theorem ustuqtop4

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

Ref Expression
Hypothesis utopustuq.1 
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
Assertion ustuqtop4 
|- ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )

Proof

Step Hyp Ref Expression
1 utopustuq.1 
 |-  N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )
2 simplll 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> ( U e. ( UnifOn ` X ) /\ p e. X ) )
3 simplr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> u e. U )
4 eqid 
 |-  ( u " { p } ) = ( u " { p } )
5 imaeq1 
 |-  ( w = u -> ( w " { p } ) = ( u " { p } ) )
6 5 rspceeqv 
 |-  ( ( u e. U /\ ( u " { p } ) = ( u " { p } ) ) -> E. w e. U ( u " { p } ) = ( w " { p } ) )
7 4 6 mpan2 
 |-  ( u e. U -> E. w e. U ( u " { p } ) = ( w " { p } ) )
8 7 adantl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ u e. U ) -> E. w e. U ( u " { p } ) = ( w " { p } ) )
9 imaexg 
 |-  ( u e. U -> ( u " { p } ) e. _V )
10 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ ( u " { p } ) e. _V ) -> ( ( u " { p } ) e. ( N ` p ) <-> E. w e. U ( u " { p } ) = ( w " { p } ) ) )
11 9 10 sylan2 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ u e. U ) -> ( ( u " { p } ) e. ( N ` p ) <-> E. w e. U ( u " { p } ) = ( w " { p } ) ) )
12 8 11 mpbird 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ u e. U ) -> ( u " { p } ) e. ( N ` p ) )
13 2 3 12 syl2anc 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> ( u " { p } ) e. ( N ` p ) )
14 simp-5l 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> U e. ( UnifOn ` X ) )
15 2 simpld 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> U e. ( UnifOn ` X ) )
16 simp-4r 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> p e. X )
17 ustimasn 
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U /\ p e. X ) -> ( u " { p } ) C_ X )
18 15 3 16 17 syl3anc 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> ( u " { p } ) C_ X )
19 18 sselda 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> q e. X )
20 14 19 jca 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( U e. ( UnifOn ` X ) /\ q e. X ) )
21 simplr 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> q e. ( u " { p } ) )
22 simp-6l 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> U e. ( UnifOn ` X ) )
23 simp-4r 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> u e. U )
24 ustrel 
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U ) -> Rel u )
25 22 23 24 syl2anc 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> Rel u )
26 elrelimasn 
 |-  ( Rel u -> ( q e. ( u " { p } ) <-> p u q ) )
27 25 26 syl 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( q e. ( u " { p } ) <-> p u q ) )
28 21 27 mpbid 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> p u q )
29 simpr 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> r e. ( u " { q } ) )
30 elrelimasn 
 |-  ( Rel u -> ( r e. ( u " { q } ) <-> q u r ) )
31 25 30 syl 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( r e. ( u " { q } ) <-> q u r ) )
32 29 31 mpbid 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> q u r )
33 vex 
 |-  p e. _V
34 vex 
 |-  r e. _V
35 33 34 brco 
 |-  ( p ( u o. u ) r <-> E. q ( p u q /\ q u r ) )
36 35 biimpri 
 |-  ( E. q ( p u q /\ q u r ) -> p ( u o. u ) r )
37 36 19.23bi 
 |-  ( ( p u q /\ q u r ) -> p ( u o. u ) r )
38 28 32 37 syl2anc 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> p ( u o. u ) r )
39 simpllr 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( u o. u ) C_ w )
40 39 ssbrd 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( p ( u o. u ) r -> p w r ) )
41 38 40 mpd 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> p w r )
42 simp-5r 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> w e. U )
43 ustrel 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U ) -> Rel w )
44 22 42 43 syl2anc 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> Rel w )
45 elrelimasn 
 |-  ( Rel w -> ( r e. ( w " { p } ) <-> p w r ) )
46 44 45 syl 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> ( r e. ( w " { p } ) <-> p w r ) )
47 41 46 mpbird 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) /\ r e. ( u " { q } ) ) -> r e. ( w " { p } ) )
48 47 ex 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( r e. ( u " { q } ) -> r e. ( w " { p } ) ) )
49 48 ssrdv 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( u " { q } ) C_ ( w " { p } ) )
50 simp-4r 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> w e. U )
51 16 adantr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> p e. X )
52 ustimasn 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U /\ p e. X ) -> ( w " { p } ) C_ X )
53 14 50 51 52 syl3anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( w " { p } ) C_ X )
54 20 49 53 3jca 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) )
55 simpllr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> u e. U )
56 eqidd 
 |-  ( u e. U -> ( u " { q } ) = ( u " { q } ) )
57 imaeq1 
 |-  ( w = u -> ( w " { q } ) = ( u " { q } ) )
58 57 rspceeqv 
 |-  ( ( u e. U /\ ( u " { q } ) = ( u " { q } ) ) -> E. w e. U ( u " { q } ) = ( w " { q } ) )
59 56 58 mpdan 
 |-  ( u e. U -> E. w e. U ( u " { q } ) = ( w " { q } ) )
60 59 adantl 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ u e. U ) -> E. w e. U ( u " { q } ) = ( w " { q } ) )
61 imaexg 
 |-  ( u e. U -> ( u " { q } ) e. _V )
62 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) e. _V ) -> ( ( u " { q } ) e. ( N ` q ) <-> E. w e. U ( u " { q } ) = ( w " { q } ) ) )
63 61 62 sylan2 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ u e. U ) -> ( ( u " { q } ) e. ( N ` q ) <-> E. w e. U ( u " { q } ) = ( w " { q } ) ) )
64 60 63 mpbird 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ u e. U ) -> ( u " { q } ) e. ( N ` q ) )
65 14 19 55 64 syl21anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( u " { q } ) e. ( N ` q ) )
66 54 65 jca 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) )
67 imaexg 
 |-  ( w e. U -> ( w " { p } ) e. _V )
68 sseq2 
 |-  ( b = ( w " { p } ) -> ( ( u " { q } ) C_ b <-> ( u " { q } ) C_ ( w " { p } ) ) )
69 sseq1 
 |-  ( b = ( w " { p } ) -> ( b C_ X <-> ( w " { p } ) C_ X ) )
70 68 69 3anbi23d 
 |-  ( b = ( w " { p } ) -> ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) <-> ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) ) )
71 70 anbi1d 
 |-  ( b = ( w " { p } ) -> ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) <-> ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) ) )
72 71 anbi1d 
 |-  ( b = ( w " { p } ) -> ( ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) <-> ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) ) )
73 eleq1 
 |-  ( b = ( w " { p } ) -> ( b e. ( N ` q ) <-> ( w " { p } ) e. ( N ` q ) ) )
74 72 73 imbi12d 
 |-  ( b = ( w " { p } ) -> ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> b e. ( N ` q ) ) <-> ( ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> ( w " { p } ) e. ( N ` q ) ) ) )
75 sseq1 
 |-  ( a = ( u " { q } ) -> ( a C_ b <-> ( u " { q } ) C_ b ) )
76 75 3anbi2d 
 |-  ( a = ( u " { q } ) -> ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) <-> ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) ) )
77 eleq1 
 |-  ( a = ( u " { q } ) -> ( a e. ( N ` q ) <-> ( u " { q } ) e. ( N ` q ) ) )
78 76 77 anbi12d 
 |-  ( a = ( u " { q } ) -> ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) <-> ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) ) )
79 78 imbi1d 
 |-  ( a = ( u " { q } ) -> ( ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) -> b e. ( N ` q ) ) <-> ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) -> b e. ( N ` q ) ) ) )
80 eleq1 
 |-  ( p = q -> ( p e. X <-> q e. X ) )
81 80 anbi2d 
 |-  ( p = q -> ( ( U e. ( UnifOn ` X ) /\ p e. X ) <-> ( U e. ( UnifOn ` X ) /\ q e. X ) ) )
82 81 3anbi1d 
 |-  ( p = q -> ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) <-> ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) ) )
83 fveq2 
 |-  ( p = q -> ( N ` p ) = ( N ` q ) )
84 83 eleq2d 
 |-  ( p = q -> ( a e. ( N ` p ) <-> a e. ( N ` q ) ) )
85 82 84 anbi12d 
 |-  ( p = q -> ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) <-> ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) ) )
86 83 eleq2d 
 |-  ( p = q -> ( b e. ( N ` p ) <-> b e. ( N ` q ) ) )
87 85 86 imbi12d 
 |-  ( p = q -> ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) ) <-> ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) -> b e. ( N ` q ) ) ) )
88 1 ustuqtop1 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
89 87 88 chvarvv 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` q ) ) -> b e. ( N ` q ) )
90 79 89 vtoclg 
 |-  ( ( u " { q } ) e. _V -> ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) -> b e. ( N ` q ) ) )
91 61 90 syl 
 |-  ( u e. U -> ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) -> b e. ( N ` q ) ) )
92 91 impcom 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ b /\ b C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> b e. ( N ` q ) )
93 74 92 vtoclg 
 |-  ( ( w " { p } ) e. _V -> ( ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> ( w " { p } ) e. ( N ` q ) ) )
94 67 93 syl 
 |-  ( w e. U -> ( ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) -> ( w " { p } ) e. ( N ` q ) ) )
95 94 impcom 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ q e. X ) /\ ( u " { q } ) C_ ( w " { p } ) /\ ( w " { p } ) C_ X ) /\ ( u " { q } ) e. ( N ` q ) ) /\ u e. U ) /\ w e. U ) -> ( w " { p } ) e. ( N ` q ) )
96 66 55 50 95 syl21anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) /\ q e. ( u " { p } ) ) -> ( w " { p } ) e. ( N ` q ) )
97 96 ralrimiva 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> A. q e. ( u " { p } ) ( w " { p } ) e. ( N ` q ) )
98 raleq 
 |-  ( b = ( u " { p } ) -> ( A. q e. b ( w " { p } ) e. ( N ` q ) <-> A. q e. ( u " { p } ) ( w " { p } ) e. ( N ` q ) ) )
99 98 rspcev 
 |-  ( ( ( u " { p } ) e. ( N ` p ) /\ A. q e. ( u " { p } ) ( w " { p } ) e. ( N ` q ) ) -> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) )
100 13 97 99 syl2anc 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ u e. U ) /\ ( u o. u ) C_ w ) -> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) )
101 ustexhalf 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U ) -> E. u e. U ( u o. u ) C_ w )
102 101 adantlr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) -> E. u e. U ( u o. u ) C_ w )
103 100 102 r19.29a 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) -> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) )
104 103 adantr 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ a = ( w " { p } ) ) -> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) )
105 eleq1 
 |-  ( a = ( w " { p } ) -> ( a e. ( N ` q ) <-> ( w " { p } ) e. ( N ` q ) ) )
106 105 rexralbidv 
 |-  ( a = ( w " { p } ) -> ( E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) <-> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) ) )
107 106 adantl 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ a = ( w " { p } ) ) -> ( E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) <-> E. b e. ( N ` p ) A. q e. b ( w " { p } ) e. ( N ` q ) ) )
108 104 107 mpbird 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ w e. U ) /\ a = ( w " { p } ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
109 108 adantllr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) /\ w e. U ) /\ a = ( w " { p } ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
110 vex 
 |-  a e. _V
111 1 ustuqtoplem 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. _V ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
112 110 111 mpan2 
 |-  ( ( U e. ( UnifOn ` X ) /\ p e. X ) -> ( a e. ( N ` p ) <-> E. w e. U a = ( w " { p } ) ) )
113 112 biimpa 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. w e. U a = ( w " { p } ) )
114 109 113 r19.29a 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )