| Step | Hyp | Ref
| Expression |
| 1 | | df-subrng 13754 |
. . 3
SubRng  Rng        ↾s  Rng  |
| 2 | 1 | mptrcl 5644 |
. 2
 SubRng 
Rng |
| 3 | | simp1 999 |
. 2
  Rng  ↾s  Rng 
Rng |
| 4 | | df-subrng 13754 |
. . . . 5
SubRng  Rng        ↾s  Rng  |
| 5 | | fveq2 5558 |
. . . . . . 7
           |
| 6 | 5 | pweqd 3610 |
. . . . . 6
             |
| 7 | | oveq1 5929 |
. . . . . . 7
  ↾s   ↾s    |
| 8 | 7 | eleq1d 2265 |
. . . . . 6
  
↾s  Rng  ↾s  Rng  |
| 9 | 6, 8 | rabeqbidv 2758 |
. . . . 5
        ↾s  Rng        ↾s  Rng  |
| 10 | | id 19 |
. . . . 5
 Rng Rng |
| 11 | | basfn 12736 |
. . . . . . . 8
 |
| 12 | | elex 2774 |
. . . . . . . 8
 Rng   |
| 13 | | funfvex 5575 |
. . . . . . . . 9
 
       |
| 14 | 13 | funfni 5358 |
. . . . . . . 8
 
       |
| 15 | 11, 12, 14 | sylancr 414 |
. . . . . . 7
 Rng       |
| 16 | 15 | pwexd 4214 |
. . . . . 6
 Rng        |
| 17 | | rabexg 4176 |
. . . . . 6
            
↾s  Rng
  |
| 18 | 16, 17 | syl 14 |
. . . . 5
 Rng        ↾s  Rng   |
| 19 | 4, 9, 10, 18 | fvmptd3 5655 |
. . . 4
 Rng SubRng         ↾s  Rng  |
| 20 | 19 | eleq2d 2266 |
. . 3
 Rng  SubRng         ↾s  Rng   |
| 21 | | oveq2 5930 |
. . . . . 6
  ↾s   ↾s    |
| 22 | 21 | eleq1d 2265 |
. . . . 5
  
↾s  Rng  ↾s  Rng  |
| 23 | 22 | elrab 2920 |
. . . 4
        ↾s  Rng
     
 ↾s 
Rng  |
| 24 | | issubrng.b |
. . . . . . . . 9
     |
| 25 | 24 | eqcomi 2200 |
. . . . . . . 8
     |
| 26 | 25 | sseq2i 3210 |
. . . . . . 7
    
  |
| 27 | 26 | anbi2i 457 |
. . . . . 6
  
↾s  Rng     
  ↾s  Rng    |
| 28 | | ibar 301 |
. . . . . 6
 Rng    ↾s  Rng 
 Rng   ↾s  Rng      |
| 29 | 27, 28 | bitrid 192 |
. . . . 5
 Rng    ↾s  Rng     
 Rng   ↾s  Rng      |
| 30 | | ancom 266 |
. . . . . 6
       
↾s  Rng  
↾s  Rng
        |
| 31 | | elpw2g 4189 |
. . . . . . . 8
    
     
       |
| 32 | 15, 31 | syl 14 |
. . . . . . 7
 Rng      
       |
| 33 | 32 | anbi2d 464 |
. . . . . 6
 Rng    ↾s  Rng
        ↾s  Rng
        |
| 34 | 30, 33 | bitrid 192 |
. . . . 5
 Rng         ↾s  Rng  
↾s  Rng         |
| 35 | | 3anass 984 |
. . . . . 6
  Rng  ↾s  Rng 
 Rng   ↾s  Rng     |
| 36 | 35 | a1i 9 |
. . . . 5
 Rng   Rng
 ↾s  Rng

 Rng   ↾s  Rng      |
| 37 | 29, 34, 36 | 3bitr4d 220 |
. . . 4
 Rng         ↾s  Rng  Rng  ↾s  Rng     |
| 38 | 23, 37 | bitrid 192 |
. . 3
 Rng         ↾s  Rng
 Rng  ↾s  Rng
    |
| 39 | 20, 38 | bitrd 188 |
. 2
 Rng  SubRng   Rng  ↾s  Rng     |
| 40 | 2, 3, 39 | pm5.21nii 705 |
1
 SubRng   Rng 
↾s  Rng    |