Step | Hyp | Ref
| Expression |
1 | | ssid 3463 |
. 2
 |
2 | | simp2 1015 |
. . 3
 

 ↾t     |
3 | | sseq1 3465 |
. . . . . 6


   |
4 | | iuneq1 4306 |
. . . . . . . . 9


   |
5 | | 0iun 4349 |
. . . . . . . . 9
  |
6 | 4, 5 | syl6eq 2512 |
. . . . . . . 8


  |
7 | 6 | oveq2d 6331 |
. . . . . . 7

 ↾t 
  ↾t    |
8 | 7 | eleq1d 2524 |
. . . . . 6

  ↾t    ↾t     |
9 | 3, 8 | imbi12d 326 |
. . . . 5

 
 ↾t    

↾t      |
10 | 9 | imbi2d 322 |
. . . 4

     ↾t     ↾t 
  
 

 ↾t   

↾t       |
11 | | sseq1 3465 |
. . . . . 6
 
   |
12 | | iuneq1 4306 |
. . . . . . . 8
 
   |
13 | 12 | oveq2d 6331 |
. . . . . . 7
  ↾t    ↾t 
   |
14 | 13 | eleq1d 2524 |
. . . . . 6
  
↾t    ↾t      |
15 | 11, 14 | imbi12d 326 |
. . . . 5
   
↾t     
↾t       |
16 | 15 | imbi2d 322 |
. . . 4
   
  ↾t   
 ↾t    
 

 ↾t    
↾t        |
17 | | sseq1 3465 |
. . . . . 6
             |
18 | | iuneq1 4306 |
. . . . . . . 8
              |
19 | 18 | oveq2d 6331 |
. . . . . . 7
      ↾t 
  ↾t          |
20 | 19 | eleq1d 2524 |
. . . . . 6
       ↾t 

 ↾t           |
21 | 17, 20 | imbi12d 326 |
. . . . 5
        ↾t          ↾t            |
22 | 21 | imbi2d 322 |
. . . 4
       

 ↾t     ↾t 
  
 

 ↾t         ↾t             |
23 | | sseq1 3465 |
. . . . . 6
 
   |
24 | | iuneq1 4306 |
. . . . . . . 8
 
   |
25 | 24 | oveq2d 6331 |
. . . . . . 7
  ↾t    ↾t 
   |
26 | 25 | eleq1d 2524 |
. . . . . 6
  
↾t    ↾t      |
27 | 23, 26 | imbi12d 326 |
. . . . 5
   
↾t     
↾t       |
28 | 27 | imbi2d 322 |
. . . 4
   
  ↾t   
 ↾t    
 

 ↾t    
↾t        |
29 | | rest0 20234 |
. . . . . . 7
  ↾t      |
30 | | 0cmp 20458 |
. . . . . . 7
   |
31 | 29, 30 | syl6eqel 2548 |
. . . . . 6
  ↾t    |
32 | 31 | 3ad2ant1 1035 |
. . . . 5
 

 ↾t    ↾t    |
33 | 32 | a1d 26 |
. . . 4
 

 ↾t    
↾t     |
34 | | ssun1 3609 |
. . . . . . . . 9
     |
35 | | id 22 |
. . . . . . . . 9
           |
36 | 34, 35 | syl5ss 3455 |
. . . . . . . 8
    
  |
37 | 36 | imim1i 60 |
. . . . . . 7
 
 ↾t        
 ↾t      |
38 | | simpl1 1017 |
. . . . . . . . . . 11
     ↾t       

↾t       |
39 | | iunxun 4377 |
. . . . . . . . . . . 12
       
      |
40 | | simprr 771 |
. . . . . . . . . . . . . 14
     ↾t       

↾t      ↾t     |
41 | | cmptop 20459 |
. . . . . . . . . . . . . 14
  ↾t   
↾t     |
42 | | restrcl 20222 |
. . . . . . . . . . . . . . 15
  ↾t        |
43 | 42 | simprd 469 |
. . . . . . . . . . . . . 14
  ↾t      |
44 | 40, 41, 43 | 3syl 18 |
. . . . . . . . . . . . 13
     ↾t       

↾t     
  |
45 | | nfcv 2603 |
. . . . . . . . . . . . . . . 16
   |
46 | | nfcsb1v 3391 |
. . . . . . . . . . . . . . . 16
  
 ![]_ ]_](_urbrack.gif)  |
47 | | csbeq1a 3384 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   |
48 | 45, 46, 47 | cbviun 4329 |
. . . . . . . . . . . . . . 15
          ![]_ ]_](_urbrack.gif)  |
49 | | vex 3060 |
. . . . . . . . . . . . . . . 16
 |
50 | | csbeq1 3378 |
. . . . . . . . . . . . . . . 16
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
51 | 49, 50 | iunxsn 4375 |
. . . . . . . . . . . . . . 15
      ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)  |
52 | 48, 51 | eqtri 2484 |
. . . . . . . . . . . . . 14
      ![]_ ]_](_urbrack.gif)  |
53 | | ssun2 3610 |
. . . . . . . . . . . . . . . . . 18
 
     |
54 | | simprl 769 |
. . . . . . . . . . . . . . . . . 18
     ↾t       

↾t           |
55 | 53, 54 | syl5ss 3455 |
. . . . . . . . . . . . . . . . 17
     ↾t       

↾t      
  |
56 | 49 | snss 4109 |
. . . . . . . . . . . . . . . . 17

    |
57 | 55, 56 | sylibr 217 |
. . . . . . . . . . . . . . . 16
     ↾t       

↾t       |
58 | | simpl3 1019 |
. . . . . . . . . . . . . . . . 17
     ↾t       

↾t     
 ↾t    |
59 | | nfv 1772 |
. . . . . . . . . . . . . . . . . 18
  
↾t   |
60 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . 20
   |
61 | | nfcv 2603 |
. . . . . . . . . . . . . . . . . . . 20
 ↾t |
62 | 60, 61, 46 | nfov 6341 |
. . . . . . . . . . . . . . . . . . 19
  
↾t   ![]_ ]_](_urbrack.gif)   |
63 | 62 | nfel1 2617 |
. . . . . . . . . . . . . . . . . 18
  
↾t   ![]_ ]_](_urbrack.gif)   |
64 | 47 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . . 19
  ↾t   ↾t   ![]_ ]_](_urbrack.gif)    |
65 | 64 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . 18
  
↾t   ↾t   ![]_ ]_](_urbrack.gif)     |
66 | 59, 63, 65 | cbvral 3027 |
. . . . . . . . . . . . . . . . 17
 
 ↾t  
 ↾t   ![]_ ]_](_urbrack.gif)    |
67 | 58, 66 | sylib 201 |
. . . . . . . . . . . . . . . 16
     ↾t       

↾t     
 ↾t   ![]_ ]_](_urbrack.gif)    |
68 | 50 | oveq2d 6331 |
. . . . . . . . . . . . . . . . . 18
  ↾t   ![]_ ]_](_urbrack.gif)   ↾t   ![]_ ]_](_urbrack.gif)    |
69 | 68 | eleq1d 2524 |
. . . . . . . . . . . . . . . . 17
  
↾t   ![]_ ]_](_urbrack.gif)   ↾t   ![]_ ]_](_urbrack.gif)     |
70 | 69 | rspcv 3158 |
. . . . . . . . . . . . . . . 16
  

↾t   ![]_ ]_](_urbrack.gif)  
↾t   ![]_ ]_](_urbrack.gif)     |
71 | 57, 67, 70 | sylc 62 |
. . . . . . . . . . . . . . 15
     ↾t       

↾t      ↾t   ![]_ ]_](_urbrack.gif)    |
72 | | cmptop 20459 |
. . . . . . . . . . . . . . 15
  ↾t   ![]_ ]_](_urbrack.gif)  
↾t   ![]_ ]_](_urbrack.gif)    |
73 | | restrcl 20222 |
. . . . . . . . . . . . . . . 16
  ↾t   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)
   |
74 | 73 | simprd 469 |
. . . . . . . . . . . . . . 15
  ↾t   ![]_ ]_](_urbrack.gif)    ![]_ ]_](_urbrack.gif)
  |
75 | 71, 72, 74 | 3syl 18 |
. . . . . . . . . . . . . 14
     ↾t       

↾t       ![]_ ]_](_urbrack.gif)   |
76 | 52, 75 | syl5eqel 2544 |
. . . . . . . . . . . . 13
     ↾t       

↾t           |
77 | | unexg 6619 |
. . . . . . . . . . . . 13
         
       |
78 | 44, 76, 77 | syl2anc 671 |
. . . . . . . . . . . 12
     ↾t       

↾t      
       |
79 | 39, 78 | syl5eqel 2544 |
. . . . . . . . . . 11
     ↾t       

↾t             |
80 | | resttop 20225 |
. . . . . . . . . . 11
          ↾t          |
81 | 38, 79, 80 | syl2anc 671 |
. . . . . . . . . 10
     ↾t       

↾t      ↾t          |
82 | | eqid 2462 |
. . . . . . . . . . . . . . 15
   |
83 | 82 | restin 20231 |
. . . . . . . . . . . . . 14
          ↾t         ↾t             |
84 | 38, 79, 83 | syl2anc 671 |
. . . . . . . . . . . . 13
     ↾t       

↾t      ↾t        
↾t             |
85 | 84 | unieqd 4222 |
. . . . . . . . . . . 12
     ↾t       

↾t       ↾t          ↾t  
          |
86 | | inss2 3665 |
. . . . . . . . . . . . . 14
 
      
  |
87 | | fiuncmp.1 |
. . . . . . . . . . . . . 14
  |
88 | 86, 87 | sseqtr4i 3477 |
. . . . . . . . . . . . 13
 
      
 |
89 | 87 | restuni 20227 |
. . . . . . . . . . . . 13
           
 
         ↾t             |
90 | 38, 88, 89 | sylancl 673 |
. . . . . . . . . . . 12
     ↾t       

↾t      
        
↾t             |
91 | 85, 90 | eqtr4d 2499 |
. . . . . . . . . . 11
     ↾t       

↾t       ↾t                   |
92 | 52 | uneq2i 3597 |
. . . . . . . . . . . . . 14
 
      
  ![]_ ]_](_urbrack.gif)   |
93 | 39, 92 | eqtri 2484 |
. . . . . . . . . . . . 13
       
  ![]_ ]_](_urbrack.gif)   |
94 | 93 | ineq1i 3642 |
. . . . . . . . . . . 12
 
            ![]_ ]_](_urbrack.gif)     |
95 | | indir 3703 |
. . . . . . . . . . . 12
     ![]_ ]_](_urbrack.gif)      
     ![]_ ]_](_urbrack.gif)     |
96 | 94, 95 | eqtri 2484 |
. . . . . . . . . . 11
 
               ![]_ ]_](_urbrack.gif)     |
97 | 91, 96 | syl6eq 2512 |
. . . . . . . . . 10
     ↾t       

↾t       ↾t          
   
 ![]_ ]_](_urbrack.gif)
     |
98 | | inss1 3664 |
. . . . . . . . . . . . . . 15
 
    |
99 | | ssun1 3609 |
. . . . . . . . . . . . . . . 16

 
      |
100 | 99, 39 | sseqtr4i 3477 |
. . . . . . . . . . . . . . 15

       |
101 | 98, 100 | sstri 3453 |
. . . . . . . . . . . . . 14
 
         |
102 | 101 | a1i 11 |
. . . . . . . . . . . . 13
     ↾t       

↾t      
          |
103 | | restabs 20230 |
. . . . . . . . . . . . 13
     
               ↾t        ↾t      
↾t  
     |
104 | 38, 102, 79, 103 | syl3anc 1276 |
. . . . . . . . . . . 12
     ↾t       

↾t      
↾t        ↾t       ↾t        |
105 | 82 | restin 20231 |
. . . . . . . . . . . . 13
    
↾t    ↾t        |
106 | 38, 44, 105 | syl2anc 671 |
. . . . . . . . . . . 12
     ↾t       

↾t      ↾t    ↾t        |
107 | 104, 106 | eqtr4d 2499 |
. . . . . . . . . . 11
     ↾t       

↾t      
↾t        ↾t       ↾t     |
108 | 107, 40 | eqeltrd 2540 |
. . . . . . . . . 10
     ↾t       

↾t      
↾t        ↾t        |
109 | | inss1 3664 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)     ![]_ ]_](_urbrack.gif)  |
110 | | ssun2 3610 |
. . . . . . . . . . . . . . . . 17
      
     |
111 | 110, 39 | sseqtr4i 3477 |
. . . . . . . . . . . . . . . 16
           |
112 | 52, 111 | eqsstr3i 3475 |
. . . . . . . . . . . . . . 15
  ![]_ ]_](_urbrack.gif)        |
113 | 109, 112 | sstri 3453 |
. . . . . . . . . . . . . 14
   ![]_ ]_](_urbrack.gif)          |
114 | 113 | a1i 11 |
. . . . . . . . . . . . 13
     ↾t       

↾t      
 ![]_ ]_](_urbrack.gif)
 
        |
115 | | restabs 20230 |
. . . . . . . . . . . . 13
     ![]_ ]_](_urbrack.gif)
 
               ↾t        ↾t    ![]_ ]_](_urbrack.gif)    
↾t    ![]_ ]_](_urbrack.gif)      |
116 | 38, 114, 79, 115 | syl3anc 1276 |
. . . . . . . . . . . 12
     ↾t       

↾t      
↾t        ↾t    ![]_ ]_](_urbrack.gif)
    ↾t    ![]_ ]_](_urbrack.gif)      |
117 | 82 | restin 20231 |
. . . . . . . . . . . . 13
    ![]_ ]_](_urbrack.gif)
 
↾t   ![]_ ]_](_urbrack.gif)   ↾t    ![]_ ]_](_urbrack.gif)      |
118 | 38, 75, 117 | syl2anc 671 |
. . . . . . . . . . . 12
     ↾t       

↾t      ↾t   ![]_ ]_](_urbrack.gif)   ↾t    ![]_ ]_](_urbrack.gif)      |
119 | 116, 118 | eqtr4d 2499 |
. . . . . . . . . . 11
     ↾t       

↾t      
↾t        ↾t    ![]_ ]_](_urbrack.gif)
    ↾t   ![]_ ]_](_urbrack.gif)    |
120 | 119, 71 | eqeltrd 2540 |
. . . . . . . . . 10
     ↾t       

↾t      
↾t        ↾t    ![]_ ]_](_urbrack.gif)
     |
121 | | eqid 2462 |
. . . . . . . . . . 11
  ↾t          ↾t         |
122 | 121 | uncmp 20467 |
. . . . . . . . . 10
    ↾t         
↾t          
     ![]_ ]_](_urbrack.gif)        ↾t        ↾t        ↾t        ↾t    ![]_ ]_](_urbrack.gif)      
↾t          |
123 | 81, 97, 108, 120, 122 | syl22anc 1277 |
. . . . . . . . 9
     ↾t       

↾t      ↾t          |
124 | 123 | exp32 614 |
. . . . . . . 8
 

 ↾t       
 
↾t   
↾t            |
125 | 124 | a2d 29 |
. . . . . . 7
 

 ↾t         
↾t        
 ↾t            |
126 | 37, 125 | syl5 33 |
. . . . . 6
 

 ↾t      ↾t          ↾t            |
127 | 126 | a2i 14 |
. . . . 5
     ↾t     ↾t 
    
  ↾t         ↾t            |
128 | 127 | a1i 11 |
. . . 4
   
  ↾t   
 ↾t         ↾t       
 ↾t             |
129 | 10, 16, 22, 28, 33, 128 | findcard2 7837 |
. . 3
     ↾t     ↾t 
     |
130 | 2, 129 | mpcom 37 |
. 2
 

 ↾t     ↾t 
    |
131 | 1, 130 | mpi 20 |
1
 

 ↾t    ↾t 
   |