Step | Hyp | Ref
| Expression |
1 | | firest 15409 |
. . . 4
            

                      ↾t 
               
                      
↾t    |
2 | | snex 4641 |
. . . . . . . 8
        |
3 | | ptrest.0 |
. . . . . . . . . 10
   |
4 | | fvex 5889 |
. . . . . . . . . . 11
     |
5 | 4 | rgenw 2768 |
. . . . . . . . . 10

     |
6 | | eqid 2471 |
. . . . . . . . . . 11
                                               |
7 | 6 | mpt2exxg 6886 |
. . . . . . . . . 10
         
                       |
8 | 3, 5, 7 | sylancl 675 |
. . . . . . . . 9
  
                       |
9 | | rnexg 6744 |
. . . . . . . . 9
                       
                         |
10 | 8, 9 | syl 17 |
. . . . . . . 8
                          |
11 | | unexg 6611 |
. . . . . . . 8
                                                                   |
12 | 2, 10, 11 | sylancr 676 |
. . . . . . 7
                                   |
13 | | ptrest.2 |
. . . . . . . . 9
 
   |
14 | 13 | ralrimiva 2809 |
. . . . . . . 8
 
  |
15 | | ixpexg 7564 |
. . . . . . . 8
 

  |
16 | 14, 15 | syl 17 |
. . . . . . 7
 
  |
17 | | restval 15403 |
. . . . . . 7
                                 
           

                      ↾t 
 
        

                       
    |
18 | 12, 16, 17 | syl2anc 673 |
. . . . . 6
                                  ↾t 
          

                       
    |
19 | | mptun 5719 |
. . . . . . . . 9
                                  
            
   

                      
    |
20 | 19 | rneqi 5067 |
. . . . . . . 8
         

                       
            
                                |
21 | | rnun 5250 |
. . . . . . . 8
              

                      
             
                           
    |
22 | 20, 21 | eqtri 2493 |
. . . . . . 7
         

                       
            
                           
    |
23 | | elsni 3985 |
. . . . . . . . . . . . . 14
               |
24 | 23 | ineq1d 3624 |
. . . . . . . . . . . . 13
         
      
    |
25 | 24 | mpteq2ia 4478 |
. . . . . . . . . . . 12
         
                
   |
26 | | fvex 5889 |
. . . . . . . . . . . . . 14
     |
27 | 26 | uniex 6606 |
. . . . . . . . . . . . 13
      |
28 | 27 | inex1 4537 |
. . . . . . . . . . . . 13
         |
29 | | fmptsn 6100 |
. . . . . . . . . . . . 13
            
                     
             
    |
30 | 27, 28, 29 | mp2an 686 |
. . . . . . . . . . . 12
                  
             
   |
31 | 25, 30 | eqtr4i 2496 |
. . . . . . . . . . 11
         
                     |
32 | 31 | rneqi 5067 |
. . . . . . . . . 10
         
                
    |
33 | 27 | rnsnop 5324 |
. . . . . . . . . 10
                         
   |
34 | 32, 33 | eqtri 2493 |
. . . . . . . . 9
         
         
   |
35 | | ptrest.1 |
. . . . . . . . . . . . . . . 16
       |
36 | 35 | ffvelrnda 6037 |
. . . . . . . . . . . . . . 15
 
       |
37 | | inss1 3643 |
. . . . . . . . . . . . . . 15
             |
38 | | eqid 2471 |
. . . . . . . . . . . . . . . 16
           |
39 | 38 | restuni 20255 |
. . . . . . . . . . . . . . 15
            
     
             ↾t           |
40 | 36, 37, 39 | sylancl 675 |
. . . . . . . . . . . . . 14
 
      
       ↾t           |
41 | | fvex 5889 |
. . . . . . . . . . . . . . . . 17
     |
42 | 38 | restin 20259 |
. . . . . . . . . . . . . . . . 17
     
     
↾t       ↾t           |
43 | 41, 13, 42 | sylancr 676 |
. . . . . . . . . . . . . . . 16
 
      ↾t       ↾t           |
44 | | incom 3616 |
. . . . . . . . . . . . . . . . 17
               |
45 | 44 | oveq2i 6319 |
. . . . . . . . . . . . . . . 16
     ↾t              ↾t          |
46 | 43, 45 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
 
      ↾t       ↾t           |
47 | 46 | unieqd 4200 |
. . . . . . . . . . . . . 14
 
       ↾t       
↾t           |
48 | 40, 47 | eqtr4d 2508 |
. . . . . . . . . . . . 13
 
      
       ↾t    |
49 | 48 | ixpeq2dva 7555 |
. . . . . . . . . . . 12
         
      ↾t    |
50 | | ixpin 7565 |
. . . . . . . . . . . 12

              
  |
51 | | nfcv 2612 |
. . . . . . . . . . . . . 14
       
↾t   |
52 | | nfcv 2612 |
. . . . . . . . . . . . . . . 16
       |
53 | | nfcv 2612 |
. . . . . . . . . . . . . . . 16
 ↾t |
54 | | nfcsb1v 3365 |
. . . . . . . . . . . . . . . 16
  
 ![]_ ]_](_urbrack.gif)  |
55 | 52, 53, 54 | nfov 6334 |
. . . . . . . . . . . . . . 15
      
↾t   ![]_ ]_](_urbrack.gif)   |
56 | 55 | nfuni 4196 |
. . . . . . . . . . . . . 14
       
↾t   ![]_ ]_](_urbrack.gif)   |
57 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
           |
58 | | csbeq1a 3358 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   |
59 | 57, 58 | oveq12d 6326 |
. . . . . . . . . . . . . . 15
      ↾t       ↾t 
 ![]_ ]_](_urbrack.gif)    |
60 | 59 | unieqd 4200 |
. . . . . . . . . . . . . 14
       ↾t       
↾t   ![]_ ]_](_urbrack.gif)    |
61 | 51, 56, 60 | cbvixp 7557 |
. . . . . . . . . . . . 13

      ↾t  
     
↾t   ![]_ ]_](_urbrack.gif)   |
62 | | ixpeq2 7554 |
. . . . . . . . . . . . . 14
 
        ↾t            ↾t   ![]_ ]_](_urbrack.gif) 
         ↾t      
     
↾t   ![]_ ]_](_urbrack.gif)    |
63 | | ovex 6336 |
. . . . . . . . . . . . . . . 16
     ↾t   ![]_ ]_](_urbrack.gif)   |
64 | | nfcv 2612 |
. . . . . . . . . . . . . . . . 17
   |
65 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
      ↾t         ↾t    |
66 | 64, 55, 59, 65 | fvmptf 5981 |
. . . . . . . . . . . . . . . 16
      
↾t   ![]_ ]_](_urbrack.gif)          ↾t           ↾t   ![]_ ]_](_urbrack.gif)    |
67 | 63, 66 | mpan2 685 |
. . . . . . . . . . . . . . 15
       
↾t           ↾t 
 ![]_ ]_](_urbrack.gif)    |
68 | 67 | unieqd 4200 |
. . . . . . . . . . . . . 14
        
↾t           
↾t   ![]_ ]_](_urbrack.gif)    |
69 | 62, 68 | mprg 2770 |
. . . . . . . . . . . . 13

       
↾t      
     
↾t   ![]_ ]_](_urbrack.gif)   |
70 | 61, 69 | eqtr4i 2496 |
. . . . . . . . . . . 12

      ↾t  
        ↾t       |
71 | 49, 50, 70 | 3eqtr3g 2528 |
. . . . . . . . . . 11
        
 
        ↾t        |
72 | | eqid 2471 |
. . . . . . . . . . . . . 14
         |
73 | 72 | ptuni 20686 |
. . . . . . . . . . . . 13
                    |
74 | 3, 35, 73 | syl2anc 673 |
. . . . . . . . . . . 12
              |
75 | 74 | ineq1d 3624 |
. . . . . . . . . . 11
        
      
    |
76 | | resttop 20253 |
. . . . . . . . . . . . . 14
     
     
↾t    |
77 | 36, 13, 76 | syl2anc 673 |
. . . . . . . . . . . . 13
 
      ↾t    |
78 | 77, 65 | fmptd 6061 |
. . . . . . . . . . . 12
      
↾t         |
79 | | eqid 2471 |
. . . . . . . . . . . . 13
        
↾t             ↾t     |
80 | 79 | ptuni 20686 |
. . . . . . . . . . . 12
       
↾t        
       
↾t                ↾t      |
81 | 3, 78, 80 | syl2anc 673 |
. . . . . . . . . . 11
          ↾t               
↾t      |
82 | 71, 75, 81 | 3eqtr3d 2513 |
. . . . . . . . . 10
       
           ↾t      |
83 | 82 | sneqd 3971 |
. . . . . . . . 9
        
             ↾t       |
84 | 34, 83 | syl5eq 2517 |
. . . . . . . 8
          
             ↾t       |
85 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
86 | 85 | elixp 7547 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
87 | 86 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
88 | | nfcsb1v 3365 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
 ![]_ ]_](_urbrack.gif)  |
89 | 88 | nfel2 2628 |
. . . . . . . . . . . . . . . . . . . . . . 23
        ![]_ ]_](_urbrack.gif)  |
90 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
91 | | csbeq1a 3358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   ![]_ ]_](_urbrack.gif)   |
92 | 90, 91 | eleq12d 2543 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
      ![]_ ]_](_urbrack.gif)    |
93 | 89, 92 | rspc 3130 |
. . . . . . . . . . . . . . . . . . . . . 22
  
          ![]_ ]_](_urbrack.gif)    |
94 | 87, 93 | syl5 32 |
. . . . . . . . . . . . . . . . . . . . 21
  
      ![]_ ]_](_urbrack.gif)    |
95 | 94 | pm4.71d 646 |
. . . . . . . . . . . . . . . . . . . 20
  
        ![]_ ]_](_urbrack.gif)     |
96 | 95 | anbi2d 718 |
. . . . . . . . . . . . . . . . . . 19
        
     

             
      ![]_ ]_](_urbrack.gif)      |
97 | | an4 840 |
. . . . . . . . . . . . . . . . . . . 20
                     ![]_ ]_](_urbrack.gif)  
      
             ![]_ ]_](_urbrack.gif)     |
98 | | elin 3608 |
. . . . . . . . . . . . . . . . . . . . 21
      
 ![]_ ]_](_urbrack.gif) 
    
      ![]_ ]_](_urbrack.gif)    |
99 | 98 | anbi2i 708 |
. . . . . . . . . . . . . . . . . . . 20
        

       ![]_ ]_](_urbrack.gif)  
      
             ![]_ ]_](_urbrack.gif)     |
100 | 97, 99 | bitr4i 260 |
. . . . . . . . . . . . . . . . . . 19
                     ![]_ ]_](_urbrack.gif)  
      
         ![]_ ]_](_urbrack.gif)     |
101 | 96, 100 | syl6bb 269 |
. . . . . . . . . . . . . . . . . 18
        
     

      
         ![]_ ]_](_urbrack.gif)      |
102 | | elin 3608 |
. . . . . . . . . . . . . . . . . . . 20
       

     
    |
103 | 82 | eleq2d 2534 |
. . . . . . . . . . . . . . . . . . . 20
       
 
          ↾t       |
104 | 102, 103 | syl5bbr 267 |
. . . . . . . . . . . . . . . . . . 19
       
 
          ↾t       |
105 | 104 | anbi1d 719 |
. . . . . . . . . . . . . . . . . 18
                  ![]_ ]_](_urbrack.gif)  
           ↾t           ![]_ ]_](_urbrack.gif)      |
106 | 101, 105 | sylan9bbr 715 |
. . . . . . . . . . . . . . . . 17
 
        
     

           ↾t           ![]_ ]_](_urbrack.gif)      |
107 | 106 | abbidv 2589 |
. . . . . . . . . . . . . . . 16
 
                 
           ↾t           ![]_ ]_](_urbrack.gif)      |
108 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
                       |
109 | 108 | mptpreima 5335 |
. . . . . . . . . . . . . . . . . . 19
                            |
110 | | df-rab 2765 |
. . . . . . . . . . . . . . . . . . 19
                         |
111 | 109, 110 | eqtr2i 2494 |
. . . . . . . . . . . . . . . . . 18
      
                       |
112 | | abid2 2593 |
. . . . . . . . . . . . . . . . . 18


   |
113 | 111, 112 | ineq12i 3623 |
. . . . . . . . . . . . . . . . 17
               
                   
  |
114 | | inab 3702 |
. . . . . . . . . . . . . . . . 17
               
               
   |
115 | 113, 114 | eqtr3i 2495 |
. . . . . . . . . . . . . . . 16
                 
              
   |
116 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
          
↾t                    ↾t          |
117 | 116 | mptpreima 5335 |
. . . . . . . . . . . . . . . . 17
             ↾t              ![]_ ]_](_urbrack.gif)              ↾t           ![]_ ]_](_urbrack.gif)    |
118 | | df-rab 2765 |
. . . . . . . . . . . . . . . . 17
           ↾t           ![]_ ]_](_urbrack.gif)              
↾t           ![]_ ]_](_urbrack.gif)     |
119 | 117, 118 | eqtri 2493 |
. . . . . . . . . . . . . . . 16
             ↾t              ![]_ ]_](_urbrack.gif)               ↾t           ![]_ ]_](_urbrack.gif)     |
120 | 107, 115,
119 | 3eqtr4g 2530 |
. . . . . . . . . . . . . . 15
 
                  
              ↾t           
  ![]_ ]_](_urbrack.gif)     |
121 | 120 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
 
                   
              ↾t            
 ![]_ ]_](_urbrack.gif)      |
122 | 121 | rexbidv 2892 |
. . . . . . . . . . . . 13
 
  
                      
                    ↾t            
 ![]_ ]_](_urbrack.gif)      |
123 | | ineq1 3618 |
. . . . . . . . . . . . . . . 16
 
  ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)    |
124 | 123 | imaeq2d 5174 |
. . . . . . . . . . . . . . 15
              ↾t           
  ![]_ ]_](_urbrack.gif)                ↾t            
 ![]_ ]_](_urbrack.gif)     |
125 | 124 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
               ↾t              ![]_ ]_](_urbrack.gif)  
             ↾t           
  ![]_ ]_](_urbrack.gif)      |
126 | 125 | cbvrexv 3006 |
. . . . . . . . . . . . 13
                    ↾t            
 ![]_ ]_](_urbrack.gif)  
                   ↾t           
  ![]_ ]_](_urbrack.gif)     |
127 | 122, 126 | syl6bb 269 |
. . . . . . . . . . . 12
 
  
                      
                    ↾t            
 ![]_ ]_](_urbrack.gif)      |
128 | | vex 3034 |
. . . . . . . . . . . . . . 15
 |
129 | 128 | inex1 4537 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)   |
130 | 129 | a1i 11 |
. . . . . . . . . . . . 13
         
  ![]_ ]_](_urbrack.gif)    |
131 | | ovex 6336 |
. . . . . . . . . . . . . . . . 17
     ↾t   ![]_ ]_](_urbrack.gif)   |
132 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . 18
   |
133 | | nfcv 2612 |
. . . . . . . . . . . . . . . . . . 19
       |
134 | 133, 53, 88 | nfov 6334 |
. . . . . . . . . . . . . . . . . 18
      
↾t   ![]_ ]_](_urbrack.gif)   |
135 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
136 | 135, 91 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . 18
      ↾t       ↾t 
 ![]_ ]_](_urbrack.gif)    |
137 | 132, 134,
136, 65 | fvmptf 5981 |
. . . . . . . . . . . . . . . . 17
      
↾t   ![]_ ]_](_urbrack.gif)          ↾t           ↾t   ![]_ ]_](_urbrack.gif)    |
138 | 131, 137 | mpan2 685 |
. . . . . . . . . . . . . . . 16
       
↾t           ↾t 
 ![]_ ]_](_urbrack.gif)    |
139 | 138 | adantl 473 |
. . . . . . . . . . . . . . 15
 
       
↾t           ↾t 
 ![]_ ]_](_urbrack.gif)    |
140 | 139 | eleq2d 2534 |
. . . . . . . . . . . . . 14
 
         ↾t     
    
↾t   ![]_ ]_](_urbrack.gif)     |
141 | | nfv 1769 |
. . . . . . . . . . . . . . . . 17
     |
142 | | nfcsb1v 3365 |
. . . . . . . . . . . . . . . . . 18
  
 ![]_ ]_](_urbrack.gif)  |
143 | 88, 142 | nfel 2624 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)  |
144 | 141, 143 | nfim 2023 |
. . . . . . . . . . . . . . . 16
   
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)   |
145 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . 18
 
   |
146 | 145 | anbi2d 718 |
. . . . . . . . . . . . . . . . 17
  

     |
147 | | csbeq1a 3358 |
. . . . . . . . . . . . . . . . . 18
   ![]_ ]_](_urbrack.gif)   |
148 | 91, 147 | eleq12d 2543 |
. . . . . . . . . . . . . . . . 17
 
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)    |
149 | 146, 148 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
   
   
   ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)     |
150 | 144, 149,
13 | chvar 2119 |
. . . . . . . . . . . . . . 15
 
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
151 | | elrest 15404 |
. . . . . . . . . . . . . . 15
        ![]_ ]_](_urbrack.gif)
  ![]_ ]_](_urbrack.gif)        ↾t 
 ![]_ ]_](_urbrack.gif) 
         ![]_ ]_](_urbrack.gif)     |
152 | 4, 150, 151 | sylancr 676 |
. . . . . . . . . . . . . 14
 
       ↾t   ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)     |
153 | 140, 152 | bitrd 261 |
. . . . . . . . . . . . 13
 
         ↾t     
         ![]_ ]_](_urbrack.gif)     |
154 | | imaeq2 5170 |
. . . . . . . . . . . . . . 15
  
 ![]_ ]_](_urbrack.gif)               ↾t                         ↾t              ![]_ ]_](_urbrack.gif)     |
155 | 154 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
  
 ![]_ ]_](_urbrack.gif)                ↾t                         ↾t              ![]_ ]_](_urbrack.gif)      |
156 | 155 | adantl 473 |
. . . . . . . . . . . . 13
     
 ![]_ ]_](_urbrack.gif)                 ↾t           
             ↾t           
  ![]_ ]_](_urbrack.gif)      |
157 | 130, 153,
156 | rexxfr2d 4615 |
. . . . . . . . . . . 12
 
  
      
↾t                   
↾t                               ↾t              ![]_ ]_](_urbrack.gif)      |
158 | 127, 157 | bitr4d 264 |
. . . . . . . . . . 11
 
  
                      
         ↾t                   
↾t               |
159 | 158 | rexbidva 2889 |
. . . . . . . . . 10
                          


        ↾t                    ↾t               |
160 | 159 | abbidv 2589 |
. . . . . . . . 9
  

                         


       ↾t                   
↾t               |
161 | | eqid 2471 |
. . . . . . . . . . 11
                             

                      
   |
162 | 161 | rnmpt 5086 |
. . . . . . . . . 10
                         
                             
   |
163 | | nfre1 2846 |
. . . . . . . . . . 11
  


                          |
164 | | nfv 1769 |
. . . . . . . . . . 11
   
                      
  |
165 | 27 | mptex 6152 |
. . . . . . . . . . . . . . . 16
            |
166 | 165 | cnvex 6759 |
. . . . . . . . . . . . . . 15
             |
167 | | imaexg 6749 |
. . . . . . . . . . . . . . 15
                               |
168 | 166, 167 | ax-mp 5 |
. . . . . . . . . . . . . 14
                 |
169 | 168 | rgen2w 2769 |
. . . . . . . . . . . . 13

                       |
170 | | ineq1 3618 |
. . . . . . . . . . . . . . 15
                  
                  
   |
171 | 170 | eqeq2d 2481 |
. . . . . . . . . . . . . 14
                   
                 
     |
172 | 6, 171 | rexrnmpt2 6431 |
. . . . . . . . . . . . 13
 

                       

                        

                       
    |
173 | 169, 172 | ax-mp 5 |
. . . . . . . . . . . 12
                           


                       
   |
174 | | eqeq1 2475 |
. . . . . . . . . . . . 13
                   
                 
     |
175 | 174 | 2rexbidv 2897 |
. . . . . . . . . . . 12
  

                      
  
                           |
176 | 173, 175 | syl5bb 265 |
. . . . . . . . . . 11
  


                        

                       
    |
177 | 163, 164,
176 | cbvab 2594 |
. . . . . . . . . 10
                           
 
  
                      
   |
178 | 162, 177 | eqtri 2493 |
. . . . . . . . 9
                         
    
                      
   |
179 | | eqid 2471 |
. . . . . . . . . 10
         ↾t                   ↾t                      ↾t                  
↾t              |
180 | 179 | rnmpt2 6425 |
. . . . . . . . 9
         ↾t                   ↾t               
      
↾t                   
↾t              |
181 | 160, 178,
180 | 3eqtr4g 2530 |
. . . . . . . 8
                          
           ↾t                  
↾t               |
182 | 84, 181 | uneq12d 3580 |
. . . . . . 7
           
                           
              
↾t              ↾t                   ↾t                |
183 | 22, 182 | syl5eq 2517 |
. . . . . 6
                                   
              ↾t              ↾t                   ↾t                |
184 | 18, 183 | eqtrd 2505 |
. . . . 5
                                  ↾t 
             ↾t              ↾t                   ↾t                |
185 | 184 | fveq2d 5883 |
. . . 4
                                     ↾t 
                 ↾t              ↾t                   ↾t                 |
186 | 1, 185 | syl5eqr 2519 |
. . 3
              
                      
↾t                  ↾t              ↾t                   ↾t                 |
187 | 186 | fveq2d 5883 |
. 2
                                         ↾t 
                    ↾t      
      
↾t                   ↾t                  |
188 | | eqid 2471 |
. . . . . 6
           |
189 | 72, 188, 6 | ptval2 20693 |
. . . . 5
                         

                          |
190 | 3, 35, 189 | syl2anc 673 |
. . . 4
                   

                          |
191 | 190 | oveq1d 6323 |
. . 3
      ↾t 
                                          ↾t 
   |
192 | | fvex 5889 |
. . . 4
                                     |
193 | | tgrest 20252 |
. . . 4
             

                       
                                         ↾t 
                                          
↾t     |
194 | 192, 16, 193 | sylancr 676 |
. . 3
                                         ↾t 
                                          
↾t     |
195 | 191, 194 | eqtr4d 2508 |
. 2
      ↾t 
                                         ↾t 
    |
196 | | eqid 2471 |
. . . 4
          ↾t              ↾t     |
197 | 79, 196, 179 | ptval2 20693 |
. . 3
       
↾t                 ↾t                     
↾t              ↾t                   ↾t                  |
198 | 3, 78, 197 | syl2anc 673 |
. 2
          ↾t                      ↾t              ↾t                   ↾t                  |
199 | 187, 195,
198 | 3eqtr4d 2515 |
1
      ↾t 
    
     ↾t      |