Step | Hyp | Ref
| Expression |
1 | | omsOLD.m |
. . 3
toOMeas   |
2 | 1 | fveq1i 5866 |
. 2
     toOMeas      |
3 | | omsOLD.o |
. . . 4
   |
4 | | omsOLD.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 | | omsfvalOLD 29122 |
. . . 4
            toOMeas           
  Σ*              |
11 | 3, 4, 9, 10 | syl3anc 1268 |
. . 3
  toOMeas           
  Σ*              |
12 | | iccssxr 11717 |
. . . . . 6
    |
13 | | xrltso 11440 |
. . . . . . 7
 |
14 | | cnvso 5375 |
. . . . . . 7
  |
15 | 13, 14 | mpbi 212 |
. . . . . 6
 |
16 | | soss 4773 |
. . . . . 6
           |
17 | 12, 15, 16 | mp2 9 |
. . . . 5
    |
18 | 17 | a1i 11 |
. . . 4
      |
19 | | 0xr 9687 |
. . . . . 6
 |
20 | | pnfxr 11412 |
. . . . . 6
 |
21 | | pnfge 11432 |
. . . . . . 7

  |
22 | 19, 21 | ax-mp 5 |
. . . . . 6
 |
23 | | lbicc2 11748 |
. . . . . 6
  
     |
24 | 19, 20, 22, 23 | mp3an 1364 |
. . . . 5
    |
25 | 24 | a1i 11 |
. . . 4
      |
26 | | omsOLD.d |
. . . . . . . . . 10

  |
27 | | 0ex 4535 |
. . . . . . . . . . 11
 |
28 | 27 | snss 4096 |
. . . . . . . . . 10

    |
29 | 26, 28 | sylib 200 |
. . . . . . . . 9
     |
30 | | p0ex 4590 |
. . . . . . . . . 10
   |
31 | 30 | elpw 3957 |
. . . . . . . . 9
  
     |
32 | 29, 31 | sylibr 216 |
. . . . . . . 8
      |
33 | | 0ss 3763 |
. . . . . . . . 9
    |
34 | | snct 28295 |
. . . . . . . . . 10

    |
35 | 27, 34 | ax-mp 5 |
. . . . . . . . 9
   |
36 | 33, 35 | pm3.2i 457 |
. . . . . . . 8
     
  |
37 | 32, 36 | jctir 541 |
. . . . . . 7
          
    |
38 | | unieq 4206 |
. . . . . . . . . 10
         |
39 | 38 | sseq2d 3460 |
. . . . . . . . 9
    
      |
40 | | breq1 4405 |
. . . . . . . . 9
   
     |
41 | 39, 40 | anbi12d 717 |
. . . . . . . 8
    

           |
42 | 41 | elrab 3196 |
. . . . . . 7
  
   
           
    |
43 | 37, 42 | sylibr 216 |
. . . . . 6
      
    |
44 | | simpr 463 |
. . . . . . . . . 10
 

  |
45 | 44 | fveq2d 5869 |
. . . . . . . . 9
 

          |
46 | | omsOLD.0 |
. . . . . . . . . 10
       |
47 | 46 | adantr 467 |
. . . . . . . . 9
 

      |
48 | 45, 47 | eqtrd 2485 |
. . . . . . . 8
 

      |
49 | 27 | a1i 11 |
. . . . . . . 8

  |
50 | 48, 49, 25 | esumsn 28886 |
. . . . . . 7
 Σ*         |
51 | 50 | eqcomd 2457 |
. . . . . 6

Σ*         |
52 | | esumeq1 28855 |
. . . . . . . 8
   Σ*      Σ*         |
53 | 52 | eqeq2d 2461 |
. . . . . . 7
   
Σ*      Σ*          |
54 | 53 | rspcev 3150 |
. . . . . 6
       
  Σ*            
   Σ*        |
55 | 43, 51, 54 | syl2anc 667 |
. . . . 5
     
   Σ*        |
56 | | eqid 2451 |
. . . . . . 7
  


  Σ*         


  Σ*        |
57 | 56 | elrnmpt 5081 |
. . . . . 6

   


  Σ*           
   Σ*         |
58 | 19, 57 | ax-mp 5 |
. . . . 5
   


  Σ*           
   Σ*        |
59 | 55, 58 | sylibr 216 |
. . . 4
     
  Σ*         |
60 | | nfv 1761 |
. . . . . . . 8
   |
61 | | nfcv 2592 |
. . . . . . . . 9
   |
62 | | nfmpt1 4492 |
. . . . . . . . . 10
      
  Σ*        |
63 | 62 | nfrn 5077 |
. . . . . . . . 9
      
  Σ*        |
64 | 61, 63 | nfel 2604 |
. . . . . . . 8

  


  Σ*        |
65 | 60, 64 | nfan 2011 |
. . . . . . 7
  
      
Σ*         |
66 | | simpr 463 |
. . . . . . . 8
   
  


  Σ*              
Σ*       Σ*
       |
67 | | vex 3048 |
. . . . . . . . . 10
 |
68 | 67 | a1i 11 |
. . . . . . . . 9
   
  


  Σ*              
Σ*         |
69 | | nfv 1761 |
. . . . . . . . . . . . 13
   |
70 | | nfcv 2592 |
. . . . . . . . . . . . . 14
   |
71 | | nfcv 2592 |
. . . . . . . . . . . . . . . 16
         |
72 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
   |
73 | 72 | nfesum1 28861 |
. . . . . . . . . . . . . . . 16
 Σ*       |
74 | 71, 73 | nfmpt 4491 |
. . . . . . . . . . . . . . 15
      
  Σ*        |
75 | 74 | nfrn 5077 |
. . . . . . . . . . . . . 14
      
  Σ*        |
76 | 70, 75 | nfel 2604 |
. . . . . . . . . . . . 13
     
  Σ*        |
77 | 69, 76 | nfan 2011 |
. . . . . . . . . . . 12
         
Σ*         |
78 | | nfv 1761 |
. . . . . . . . . . . 12
    
   |
79 | 77, 78 | nfan 2011 |
. . . . . . . . . . 11
   
  


  Σ*                |
80 | 70, 73 | nfeq 2603 |
. . . . . . . . . . 11

Σ*       |
81 | 79, 80 | nfan 2011 |
. . . . . . . . . 10
         
  Σ*              
Σ*        |
82 | 4 | ad4antr 738 |
. . . . . . . . . . . 12
         
  Σ*              
Σ*                 |
83 | | ssrab2 3514 |
. . . . . . . . . . . . . . . 16
   
    |
84 | | simpllr 769 |
. . . . . . . . . . . . . . . 16
         
  Σ*              
Σ*                |
85 | 83, 84 | sseldi 3430 |
. . . . . . . . . . . . . . 15
         
  Σ*              
Σ*           |
86 | 7 | pweqd 3956 |
. . . . . . . . . . . . . . . 16
     |
87 | 86 | ad4antr 738 |
. . . . . . . . . . . . . . 15
         
  Σ*              
Σ*            |
88 | 85, 87 | eleqtrd 2531 |
. . . . . . . . . . . . . 14
         
  Σ*              
Σ*           |
89 | | elpwi 3960 |
. . . . . . . . . . . . . 14
    |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . 13
         
  Σ*              
Σ*          |
91 | | simpr 463 |
. . . . . . . . . . . . 13
         
  Σ*              
Σ*          |
92 | 90, 91 | sseldd 3433 |
. . . . . . . . . . . 12
         
  Σ*              
Σ*          |
93 | 82, 92 | ffvelrnd 6023 |
. . . . . . . . . . 11
         
  Σ*              
Σ*                 |
94 | 93 | ex 436 |
. . . . . . . . . 10
   
  


  Σ*              
Σ*                  |
95 | 81, 94 | ralrimi 2788 |
. . . . . . . . 9
   
  


  Σ*              
Σ*       
         |
96 | 72 | esumcl 28851 |
. . . . . . . . 9
          
Σ*           |
97 | 68, 95, 96 | syl2anc 667 |
. . . . . . . 8
   
  


  Σ*              
Σ*      
Σ*           |
98 | 66, 97 | eqeltrd 2529 |
. . . . . . 7
   
  


  Σ*              
Σ*            |
99 | | vex 3048 |
. . . . . . . . . 10
 |
100 | 56 | elrnmpt 5081 |
. . . . . . . . . 10
      
  Σ*           
   Σ*         |
101 | 99, 100 | ax-mp 5 |
. . . . . . . . 9
   


  Σ*           
   Σ*        |
102 | 101 | biimpi 198 |
. . . . . . . 8
   


  Σ*      
        Σ*        |
103 | 102 | adantl 468 |
. . . . . . 7
 
    
  Σ*                Σ*        |
104 | 65, 98, 103 | r19.29af 2930 |
. . . . . 6
 
    
  Σ*             |
105 | | iccgelb 11691 |
. . . . . . 7
        |
106 | 19, 20, 105 | mp3an12 1354 |
. . . . . 6
   
  |
107 | 104, 106 | syl 17 |
. . . . 5
 
    
  Σ*          |
108 | 19 | a1i 11 |
. . . . . 6
 
    
  Σ*          |
109 | 12, 104 | sseldi 3430 |
. . . . . 6
 
    
  Σ*          |
110 | | brcnvg 5015 |
. . . . . . . 8
        |
111 | 110 | notbid 296 |
. . . . . . 7
        |
112 | | xrlenlt 9699 |
. . . . . . 7
   
   |
113 | 111, 112 | bitr4d 260 |
. . . . . 6
        |
114 | 108, 109,
113 | syl2anc 667 |
. . . . 5
 
    
  Σ*             |
115 | 107, 114 | mpbird 236 |
. . . 4
 
    
  Σ*        
  |
116 | 18, 25, 59, 115 | supmax 7981 |
. . 3
       
  Σ*              |
117 | 11, 116 | eqtrd 2485 |
. 2
  toOMeas       |
118 | 2, 117 | syl5eq 2497 |
1
       |