Step | Hyp | Ref
| Expression |
1 | | oms.m |
. . 3
toOMeas   |
2 | 1 | fveq1i 5866 |
. 2
     toOMeas      |
3 | | oms.o |
. . . 4
   |
4 | | oms.r |
. . . 4
          |
5 | | 0ss 3763 |
. . . . 5
  |
6 | | fdm 5733 |
. . . . . . 7
          |
7 | 4, 6 | syl 17 |
. . . . . 6
   |
8 | 7 | unieqd 4208 |
. . . . 5
     |
9 | 5, 8 | syl5sseq 3480 |
. . . 4
    |
10 | | omsfval 29118 |
. . . 4
            toOMeas     inf   


  Σ*              |
11 | 3, 4, 9, 10 | syl3anc 1268 |
. . 3
  toOMeas     inf   


  Σ*              |
12 | | iccssxr 11717 |
. . . . . 6
    |
13 | | xrltso 11440 |
. . . . . 6
 |
14 | | soss 4773 |
. . . . . 6
          |
15 | 12, 13, 14 | mp2 9 |
. . . . 5
    |
16 | 15 | a1i 11 |
. . . 4
      |
17 | | 0e0iccpnf 11743 |
. . . . 5
    |
18 | 17 | a1i 11 |
. . . 4
      |
19 | | oms.d |
. . . . . . . . . 10

  |
20 | 19 | snssd 4117 |
. . . . . . . . 9
     |
21 | | p0ex 4590 |
. . . . . . . . . 10
   |
22 | 21 | elpw 3957 |
. . . . . . . . 9
  
     |
23 | 20, 22 | sylibr 216 |
. . . . . . . 8
      |
24 | | 0ss 3763 |
. . . . . . . . 9
    |
25 | | 0ex 4535 |
. . . . . . . . . 10
 |
26 | | snct 28295 |
. . . . . . . . . 10

    |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . 9
   |
28 | 24, 27 | pm3.2i 457 |
. . . . . . . 8
     
  |
29 | 23, 28 | jctir 541 |
. . . . . . 7
          
    |
30 | | unieq 4206 |
. . . . . . . . . 10
         |
31 | 30 | sseq2d 3460 |
. . . . . . . . 9
    
      |
32 | | breq1 4405 |
. . . . . . . . 9
   
     |
33 | 31, 32 | anbi12d 717 |
. . . . . . . 8
    

           |
34 | 33 | elrab 3196 |
. . . . . . 7
  
   
           
    |
35 | 29, 34 | sylibr 216 |
. . . . . 6
      
    |
36 | | simpr 463 |
. . . . . . . . . 10
 

  |
37 | 36 | fveq2d 5869 |
. . . . . . . . 9
 

          |
38 | | oms.0 |
. . . . . . . . . 10
       |
39 | 38 | adantr 467 |
. . . . . . . . 9
 

      |
40 | 37, 39 | eqtrd 2485 |
. . . . . . . 8
 

      |
41 | 40, 19, 18 | esumsn 28886 |
. . . . . . 7
 Σ*         |
42 | 41 | eqcomd 2457 |
. . . . . 6

Σ*         |
43 | | esumeq1 28855 |
. . . . . . . 8
   Σ*      Σ*         |
44 | 43 | eqeq2d 2461 |
. . . . . . 7
   
Σ*      Σ*          |
45 | 44 | rspcev 3150 |
. . . . . 6
       
  Σ*            
   Σ*        |
46 | 35, 42, 45 | syl2anc 667 |
. . . . 5
     
   Σ*        |
47 | | 0xr 9687 |
. . . . . 6
 |
48 | | eqid 2451 |
. . . . . . 7
  


  Σ*         


  Σ*        |
49 | 48 | elrnmpt 5081 |
. . . . . 6

   


  Σ*           
   Σ*         |
50 | 47, 49 | ax-mp 5 |
. . . . 5
   


  Σ*           
   Σ*        |
51 | 46, 50 | sylibr 216 |
. . . 4
     
  Σ*         |
52 | | nfv 1761 |
. . . . . . . 8
   |
53 | | nfmpt1 4492 |
. . . . . . . . . 10
      
  Σ*        |
54 | 53 | nfrn 5077 |
. . . . . . . . 9
      
  Σ*        |
55 | 54 | nfcri 2586 |
. . . . . . . 8

  


  Σ*        |
56 | 52, 55 | nfan 2011 |
. . . . . . 7
  
      
Σ*         |
57 | | simpr 463 |
. . . . . . . 8
   
  


  Σ*              
Σ*       Σ*
       |
58 | | vex 3048 |
. . . . . . . . 9
 |
59 | | nfv 1761 |
. . . . . . . . . . . . 13
   |
60 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
         |
61 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
   |
62 | 61 | nfesum1 28861 |
. . . . . . . . . . . . . . . 16
 Σ*       |
63 | 60, 62 | nfmpt 4491 |
. . . . . . . . . . . . . . 15
      
  Σ*        |
64 | 63 | nfrn 5077 |
. . . . . . . . . . . . . 14
      
  Σ*        |
65 | 64 | nfcri 2586 |
. . . . . . . . . . . . 13
     
  Σ*        |
66 | 59, 65 | nfan 2011 |
. . . . . . . . . . . 12
         
Σ*         |
67 | | nfv 1761 |
. . . . . . . . . . . 12
    
   |
68 | 66, 67 | nfan 2011 |
. . . . . . . . . . 11
   
  


  Σ*                |
69 | 62 | nfeq2 2607 |
. . . . . . . . . . 11

Σ*       |
70 | 68, 69 | nfan 2011 |
. . . . . . . . . 10
         
  Σ*              
Σ*        |
71 | 4 | ad4antr 738 |
. . . . . . . . . . . 12
         
  Σ*              
Σ*                 |
72 | | ssrab2 3514 |
. . . . . . . . . . . . . . . 16
   
    |
73 | | simpllr 769 |
. . . . . . . . . . . . . . . 16
         
  Σ*              
Σ*                |
74 | 72, 73 | sseldi 3430 |
. . . . . . . . . . . . . . 15
         
  Σ*              
Σ*           |
75 | 7 | pweqd 3956 |
. . . . . . . . . . . . . . . 16
     |
76 | 75 | ad4antr 738 |
. . . . . . . . . . . . . . 15
         
  Σ*              
Σ*            |
77 | 74, 76 | eleqtrd 2531 |
. . . . . . . . . . . . . 14
         
  Σ*              
Σ*           |
78 | 77 | elpwid 3961 |
. . . . . . . . . . . . 13
         
  Σ*              
Σ*          |
79 | | simpr 463 |
. . . . . . . . . . . . 13
         
  Σ*              
Σ*          |
80 | 78, 79 | sseldd 3433 |
. . . . . . . . . . . 12
         
  Σ*              
Σ*          |
81 | 71, 80 | ffvelrnd 6023 |
. . . . . . . . . . 11
         
  Σ*              
Σ*                 |
82 | 81 | ex 436 |
. . . . . . . . . 10
   
  


  Σ*              
Σ*                  |
83 | 70, 82 | ralrimi 2788 |
. . . . . . . . 9
   
  


  Σ*              
Σ*       
         |
84 | 61 | esumcl 28851 |
. . . . . . . . 9
          
Σ*           |
85 | 58, 83, 84 | sylancr 669 |
. . . . . . . 8
   
  


  Σ*              
Σ*      
Σ*           |
86 | 57, 85 | eqeltrd 2529 |
. . . . . . 7
   
  


  Σ*              
Σ*            |
87 | | vex 3048 |
. . . . . . . . . 10
 |
88 | 48 | elrnmpt 5081 |
. . . . . . . . . 10
      
  Σ*           
   Σ*         |
89 | 87, 88 | ax-mp 5 |
. . . . . . . . 9
   


  Σ*           
   Σ*        |
90 | 89 | biimpi 198 |
. . . . . . . 8
   


  Σ*      
        Σ*        |
91 | 90 | adantl 468 |
. . . . . . 7
 
    
  Σ*                Σ*        |
92 | 56, 86, 91 | r19.29af 2930 |
. . . . . 6
 
    
  Σ*             |
93 | | pnfxr 11412 |
. . . . . . 7
 |
94 | | iccgelb 11691 |
. . . . . . 7
        |
95 | 47, 93, 94 | mp3an12 1354 |
. . . . . 6
   
  |
96 | 92, 95 | syl 17 |
. . . . 5
 
    
  Σ*          |
97 | 12, 92 | sseldi 3430 |
. . . . . 6
 
    
  Σ*          |
98 | | xrlenlt 9699 |
. . . . . . 7
   
   |
99 | 98 | bicomd 205 |
. . . . . 6
   
   |
100 | 47, 97, 99 | sylancr 669 |
. . . . 5
 
    
  Σ*        
   |
101 | 96, 100 | mpbird 236 |
. . . 4
 
    
  Σ*          |
102 | 16, 18, 51, 101 | infmin 8010 |
. . 3
 inf   


  Σ*              |
103 | 11, 102 | eqtrd 2485 |
. 2
  toOMeas       |
104 | 2, 103 | syl5eq 2497 |
1
       |