Step | Hyp | Ref
| Expression |
1 | | ismbf3d.1 |
. 2
       |
2 | | fimacnv 6012 |
. . . 4
            |
3 | 1, 2 | syl 17 |
. . 3
     
  |
4 | | imaiun 6150 |
. . . . 5
                     |
5 | | ioossre 11696 |
. . . . . . . . 9
     |
6 | 5 | rgenw 2749 |
. . . . . . . 8
      |
7 | | iunss 4319 |
. . . . . . . 8
 
           |
8 | 6, 7 | mpbir 213 |
. . . . . . 7
      |
9 | | renegcl 9937 |
. . . . . . . . . . 11
    |
10 | | arch 10866 |
. . . . . . . . . . 11
 
    |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
     |
12 | | simpl 459 |
. . . . . . . . . . . . 13
 
   |
13 | 12 | biantrurd 511 |
. . . . . . . . . . . 12
 
         |
14 | | nnre 10616 |
. . . . . . . . . . . . 13
   |
15 | | ltnegcon1 10115 |
. . . . . . . . . . . . 13
 
       |
16 | 14, 15 | sylan2 477 |
. . . . . . . . . . . 12
 
       |
17 | 14 | adantl 468 |
. . . . . . . . . . . . . . 15
 
   |
18 | 17 | renegcld 10046 |
. . . . . . . . . . . . . 14
 
    |
19 | 18 | rexrd 9690 |
. . . . . . . . . . . . 13
 
    |
20 | | elioopnf 11728 |
. . . . . . . . . . . . 13
 
    
      |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
 
       
    |
22 | 13, 16, 21 | 3bitr4d 289 |
. . . . . . . . . . 11
 
          |
23 | 22 | rexbidva 2898 |
. . . . . . . . . 10
  

        |
24 | 11, 23 | mpbid 214 |
. . . . . . . . 9
        |
25 | | eliun 4283 |
. . . . . . . . 9
     
       |
26 | 24, 25 | sylibr 216 |
. . . . . . . 8
        |
27 | 26 | ssriv 3436 |
. . . . . . 7
      |
28 | 8, 27 | eqssi 3448 |
. . . . . 6
      |
29 | 28 | imaeq2i 5166 |
. . . . 5
                |
30 | 4, 29 | eqtr3i 2475 |
. . . 4
                |
31 | | ismbf3d.2 |
. . . . . . . 8
 

          |
32 | 31 | ralrimiva 2802 |
. . . . . . 7
            |
33 | 14 | renegcld 10046 |
. . . . . . 7
    |
34 | | oveq1 6297 |
. . . . . . . . . 10
   
       |
35 | 34 | imaeq2d 5168 |
. . . . . . . . 9
                     |
36 | 35 | eleq1d 2513 |
. . . . . . . 8
                       |
37 | 36 | rspccva 3149 |
. . . . . . 7
                        |
38 | 32, 33, 37 | syl2an 480 |
. . . . . 6
 

           |
39 | 38 | ralrimiva 2802 |
. . . . 5
             |
40 | | iunmbl 22506 |
. . . . 5
 
                     |
41 | 39, 40 | syl 17 |
. . . 4
             |
42 | 30, 41 | syl5eqelr 2534 |
. . 3
     
  |
43 | 3, 42 | eqeltrrd 2530 |
. 2
   |
44 | | imaiun 6150 |
. . . . . . 7
      ![(,] (,]](_ioc.gif)             ![(,] (,]](_ioc.gif)        |
45 | | eliun 4283 |
. . . . . . . . . 10
   ![(,] (,]](_ioc.gif)     
  ![(,] (,]](_ioc.gif)        |
46 | | 3simpb 1006 |
. . . . . . . . . . . . . . . 16
 
             |
47 | | simplr 762 |
. . . . . . . . . . . . . . . . . . . 20
    
 
  |
48 | | nnrp 11311 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
49 | 48 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
  |
50 | 49 | rpreccld 11351 |
. . . . . . . . . . . . . . . . . . . 20
    
 
    |
51 | 47, 50 | ltsubrpd 11370 |
. . . . . . . . . . . . . . . . . . 19
    
 
      |
52 | | simprr 766 |
. . . . . . . . . . . . . . . . . . . 20
    
 
  |
53 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
 

  |
54 | | nnrecre 10646 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
55 | | resubcl 9938 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
56 | 53, 54, 55 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . 21
           |
57 | 56 | adantrr 723 |
. . . . . . . . . . . . . . . . . . . 20
    
 
      |
58 | | lelttr 9724 |
. . . . . . . . . . . . . . . . . . . 20
     
               |
59 | 52, 57, 47, 58 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . 19
    
 
 
            |
60 | 51, 59 | mpan2d 680 |
. . . . . . . . . . . . . . . . . 18
    
 
    
   |
61 | 60 | anassrs 654 |
. . . . . . . . . . . . . . . . 17
   

      
   |
62 | 61 | imdistanda 699 |
. . . . . . . . . . . . . . . 16
      
          |
63 | 46, 62 | syl5 33 |
. . . . . . . . . . . . . . 15
                 |
64 | | mnfxr 11414 |
. . . . . . . . . . . . . . . 16
 |
65 | | elioc2 11697 |
. . . . . . . . . . . . . . . 16
        ![(,] (,]](_ioc.gif)               |
66 | 64, 56, 65 | sylancr 669 |
. . . . . . . . . . . . . . 15
       ![(,] (,]](_ioc.gif)     
         |
67 | | rexr 9686 |
. . . . . . . . . . . . . . . . . 18
   |
68 | 67 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 

  |
69 | | elioomnf 11729 |
. . . . . . . . . . . . . . . . 17

   
     |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . 16
 

   
     |
71 | 70 | adantr 467 |
. . . . . . . . . . . . . . 15
        
     |
72 | 63, 66, 71 | 3imtr4d 272 |
. . . . . . . . . . . . . 14
       ![(,] (,]](_ioc.gif)     
      |
73 | 72 | rexlimdva 2879 |
. . . . . . . . . . . . 13
 

 
 ![(,] (,]](_ioc.gif)     
      |
74 | 73, 70 | sylibd 218 |
. . . . . . . . . . . 12
 

 
 ![(,] (,]](_ioc.gif)     
     |
75 | | simprl 764 |
. . . . . . . . . . . . . . . 16
         |
76 | 75 | adantr 467 |
. . . . . . . . . . . . . . 15
   
             |
77 | | mnflt 11425 |
. . . . . . . . . . . . . . . 16
   |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . 15
   
          
  |
79 | 56 | ad2ant2r 753 |
. . . . . . . . . . . . . . . 16
   
                 |
80 | 54 | ad2antrl 734 |
. . . . . . . . . . . . . . . . 17
   
               |
81 | | simplr 762 |
. . . . . . . . . . . . . . . . . 18
         |
82 | 81 | adantr 467 |
. . . . . . . . . . . . . . . . 17
   
             |
83 | | simprr 766 |
. . . . . . . . . . . . . . . . 17
   
                 |
84 | 80, 82, 76, 83 | ltsub13d 10219 |
. . . . . . . . . . . . . . . 16
   
                 |
85 | 76, 79, 84 | ltled 9783 |
. . . . . . . . . . . . . . 15
   
                 |
86 | 66 | ad2ant2r 753 |
. . . . . . . . . . . . . . 15
   
             ![(,] (,]](_ioc.gif)               |
87 | 76, 78, 85, 86 | mpbir3and 1191 |
. . . . . . . . . . . . . 14
   
            ![(,] (,]](_ioc.gif)        |
88 | 81, 75 | resubcld 10047 |
. . . . . . . . . . . . . . 15
           |
89 | | simprr 766 |
. . . . . . . . . . . . . . . 16
         |
90 | 75, 81 | posdifd 10200 |
. . . . . . . . . . . . . . . 16
             |
91 | 89, 90 | mpbid 214 |
. . . . . . . . . . . . . . 15
           |
92 | | nnrecl 10867 |
. . . . . . . . . . . . . . 15
       
 
    |
93 | 88, 91, 92 | syl2anc 667 |
. . . . . . . . . . . . . 14
         
    |
94 | 87, 93 | reximddv 2863 |
. . . . . . . . . . . . 13
       
 ![(,] (,]](_ioc.gif)        |
95 | 94 | ex 436 |
. . . . . . . . . . . 12
 

   
 ![(,] (,]](_ioc.gif)         |
96 | 74, 95 | impbid 194 |
. . . . . . . . . . 11
 

 
 ![(,] (,]](_ioc.gif)           |
97 | 96, 70 | bitr4d 260 |
. . . . . . . . . 10
 

 
 ![(,] (,]](_ioc.gif)     
      |
98 | 45, 97 | syl5bb 261 |
. . . . . . . . 9
 

   ![(,] (,]](_ioc.gif)     
      |
99 | 98 | eqrdv 2449 |
. . . . . . . 8
 

  ![(,] (,]](_ioc.gif)           |
100 | 99 | imaeq2d 5168 |
. . . . . . 7
 

      ![(,] (,]](_ioc.gif)                 |
101 | 44, 100 | syl5eqr 2499 |
. . . . . 6
 

      ![(,] (,]](_ioc.gif)                 |
102 | 1 | ad2antrr 732 |
. . . . . . . . . . 11
           |
103 | | ffun 5731 |
. . . . . . . . . . 11
       |
104 | | funcnvcnv 5641 |
. . . . . . . . . . 11

    |
105 | | imadif 5658 |
. . . . . . . . . . 11
  
                                   |
106 | 102, 103,
104, 105 | 4syl 19 |
. . . . . . . . . 10
                                        |
107 | 64 | a1i 11 |
. . . . . . . . . . . . . 14
       |
108 | 56 | rexrd 9690 |
. . . . . . . . . . . . . 14
           |
109 | | pnfxr 11412 |
. . . . . . . . . . . . . . 15
 |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . 14
       |
111 | | mnflt 11425 |
. . . . . . . . . . . . . . 15
           |
112 | 56, 111 | syl 17 |
. . . . . . . . . . . . . 14
           |
113 | | ltpnf 11422 |
. . . . . . . . . . . . . . 15
           |
114 | 56, 113 | syl 17 |
. . . . . . . . . . . . . 14
           |
115 | | df-ioc 11640 |
. . . . . . . . . . . . . . 15


      |
116 | | df-ioo 11639 |
. . . . . . . . . . . . . . 15


      |
117 | | xrltnle 9701 |
. . . . . . . . . . . . . . 15
           
       |
118 | | xrlelttr 11453 |
. . . . . . . . . . . . . . 15
     

 
            |
119 | | xrlttr 11439 |
. . . . . . . . . . . . . . 15
    
 
        
   |
120 | 115, 116,
117, 116, 118, 119 | ixxun 11651 |
. . . . . . . . . . . . . 14
                   ![(,] (,]](_ioc.gif)                  |
121 | 107, 108,
110, 112, 114, 120 | syl32anc 1276 |
. . . . . . . . . . . . 13
       ![(,] (,]](_ioc.gif)                  |
122 | | uncom 3578 |
. . . . . . . . . . . . 13
  ![(,] (,]](_ioc.gif)                     
 ![(,] (,]](_ioc.gif)        |
123 | | ioomax 11709 |
. . . . . . . . . . . . 13
   |
124 | 121, 122,
123 | 3eqtr3g 2508 |
. . . . . . . . . . . 12
            
 ![(,] (,]](_ioc.gif)         |
125 | | ioossre 11696 |
. . . . . . . . . . . . 13
        |
126 | | incom 3625 |
. . . . . . . . . . . . . 14
       
 ![(,] (,]](_ioc.gif)         ![(,] (,]](_ioc.gif)               |
127 | 115, 116,
117 | ixxdisj 11650 |
. . . . . . . . . . . . . . . 16
    

  ![(,] (,]](_ioc.gif)                |
128 | 64, 109, 127 | mp3an13 1355 |
. . . . . . . . . . . . . . 15
    
  ![(,] (,]](_ioc.gif)                |
129 | 108, 128 | syl 17 |
. . . . . . . . . . . . . 14
       ![(,] (,]](_ioc.gif)                |
130 | 126, 129 | syl5eq 2497 |
. . . . . . . . . . . . 13
              ![(,] (,]](_ioc.gif)         |
131 | | uneqdifeq 3856 |
. . . . . . . . . . . . 13
                  ![(,] (,]](_ioc.gif)       
        
 ![(,] (,]](_ioc.gif)                 ![(,] (,]](_ioc.gif)         |
132 | 125, 130,
131 | sylancr 669 |
. . . . . . . . . . . 12
             
 ![(,] (,]](_ioc.gif)      
          ![(,] (,]](_ioc.gif)         |
133 | 124, 132 | mpbid 214 |
. . . . . . . . . . 11
               ![(,] (,]](_ioc.gif)        |
134 | 133 | imaeq2d 5168 |
. . . . . . . . . 10
                        ![(,] (,]](_ioc.gif)         |
135 | 106, 134 | eqtr3d 2487 |
. . . . . . . . 9
          
                  ![(,] (,]](_ioc.gif)         |
136 | 42 | ad2antrr 732 |
. . . . . . . . . 10
            |
137 | 32 | ad2antrr 732 |
. . . . . . . . . . 11
                |
138 | | oveq1 6297 |
. . . . . . . . . . . . . 14
      
          |
139 | 138 | imaeq2d 5168 |
. . . . . . . . . . . . 13
                           |
140 | 139 | eleq1d 2513 |
. . . . . . . . . . . 12
                             |
141 | 140 | rspcv 3146 |
. . . . . . . . . . 11
      
                       |
142 | 56, 137, 141 | sylc 62 |
. . . . . . . . . 10
                   |
143 | | difmbl 22496 |
. . . . . . . . . 10
      
            
                     |
144 | 136, 142,
143 | syl2anc 667 |
. . . . . . . . 9
          
               |
145 | 135, 144 | eqeltrrd 2530 |
. . . . . . . 8
          ![(,] (,]](_ioc.gif)         |
146 | 145 | ralrimiva 2802 |
. . . . . . 7
 

      ![(,] (,]](_ioc.gif)         |
147 | | iunmbl 22506 |
. . . . . . 7
 
     ![(,] (,]](_ioc.gif)      
      ![(,] (,]](_ioc.gif)         |
148 | 146, 147 | syl 17 |
. . . . . 6
 

      ![(,] (,]](_ioc.gif)         |
149 | 101, 148 | eqeltrrd 2530 |
. . . . 5
 

          |
150 | 149 | ralrimiva 2802 |
. . . 4
            |
151 | | oveq2 6298 |
. . . . . . 7
         |
152 | 151 | imaeq2d 5168 |
. . . . . 6
                   |
153 | 152 | eleq1d 2513 |
. . . . 5
                     |
154 | 153 | cbvralv 3019 |
. . . 4
 
                   |
155 | 150, 154 | sylib 200 |
. . 3
            |
156 | 155 | r19.21bi 2757 |
. 2
 

          |
157 | 1, 43, 31, 156 | ismbf2d 22597 |
1
 MblFn |