Step | Hyp | Ref
| Expression |
1 | | sneq 3745 |
. . . . . . . . . . 11
       |
2 | 1 | uneq2d 3419 |
. . . . . . . . . 10
    
      |
3 | 2 | eqeq2d 2364 |
. . . . . . . . 9
 
   
       |
4 | 3 | rexbidv 2636 |
. . . . . . . 8
  
    
       |
5 | 4 | abbidv 2468 |
. . . . . . 7
 
      
        |
6 | 5 | eleq1d 2419 |
. . . . . 6
  
      
         |
7 | 6 | imbi2d 307 |
. . . . 5
  
 
     
  
    
    |
8 | 7 | imbi2d 307 |
. . . 4
  
Nn   
    
   Nn   
    
     |
9 | | nnadjoinlem1 4520 |
. . . . . . 7
  
∼   
        |
10 | | eleq2 2414 |
. . . . . . . . . . 11
 0c   
    
      
0c  |
11 | | el0c 4422 |
. . . . . . . . . . . 12
 


    0c          |
12 | | ab0 3570 |
. . . . . . . . . . . 12
 


     

     |
13 | 11, 12 | bitri 240 |
. . . . . . . . . . 11
 


    0c         |
14 | 10, 13 | syl6bb 252 |
. . . . . . . . . 10
 0c   
    
         |
15 | 14 | imbi2d 307 |
. . . . . . . . 9
 0c   ∼ 
         ∼   
        |
16 | 15 | raleqbi1dv 2816 |
. . . . . . . 8
 0c    ∼ 
        
0c
 ∼            |
17 | | df-ral 2620 |
. . . . . . . . 9
 
0c  ∼   
       
0c

∼  


       |
18 | | el0c 4422 |
. . . . . . . . . . 11
 0c
  |
19 | 18 | imbi1i 315 |
. . . . . . . . . 10
 
0c  ∼ 
        

∼  


       |
20 | 19 | albii 1566 |
. . . . . . . . 9
    0c 
∼  


       

∼  


       |
21 | | 0ex 4111 |
. . . . . . . . . 10
 |
22 | | unieq 3901 |
. . . . . . . . . . . . 13

    |
23 | 22 | compleqd 3246 |
. . . . . . . . . . . 12

∼  ∼    |
24 | 23 | eleq2d 2420 |
. . . . . . . . . . 11


∼  ∼     |
25 | | rexeq 2809 |
. . . . . . . . . . . . 13

 
    
       |
26 | 25 | notbid 285 |
. . . . . . . . . . . 12

              |
27 | 26 | albidv 1625 |
. . . . . . . . . . 11

 


  
 
       |
28 | 24, 27 | imbi12d 311 |
. . . . . . . . . 10

 
∼   
      ∼ 
 
        |
29 | 21, 28 | ceqsalv 2886 |
. . . . . . . . 9
     ∼   
       ∼           |
30 | 17, 20, 29 | 3bitrri 263 |
. . . . . . . 8
  ∼
       
 0c 
∼   
       |
31 | 16, 30 | syl6bbr 254 |
. . . . . . 7
 0c    ∼ 
         ∼            |
32 | | eleq2 2414 |
. . . . . . . . 9
  


    


       |
33 | 32 | imbi2d 307 |
. . . . . . . 8
  
∼   
     
 ∼  


        |
34 | 33 | raleqbi1dv 2816 |
. . . . . . 7
  

∼   
     

 ∼  


        |
35 | | eleq2 2414 |
. . . . . . . . . 10
  1c   
    
        1c   |
36 | 35 | imbi2d 307 |
. . . . . . . . 9
  1c   ∼ 
         ∼   
     
1c    |
37 | 36 | raleqbi1dv 2816 |
. . . . . . . 8
  1c    ∼ 
        
 1c  ∼ 
        1c    |
38 | | unieq 3901 |
. . . . . . . . . . . 12
 
   |
39 | 38 | compleqd 3246 |
. . . . . . . . . . 11
 ∼  ∼    |
40 | 39 | eleq2d 2420 |
. . . . . . . . . 10
 
∼  ∼     |
41 | | rexeq 2809 |
. . . . . . . . . . . 12
  
    
       |
42 | 41 | abbidv 2468 |
. . . . . . . . . . 11
 


    


      |
43 | 42 | eleq1d 2419 |
. . . . . . . . . 10
  


    
1c
        1c   |
44 | 40, 43 | imbi12d 311 |
. . . . . . . . 9
  
∼   
     
1c  ∼  


    
1c    |
45 | 44 | cbvralv 2836 |
. . . . . . . 8
 
 1c  ∼   
     
1c  
1c  ∼ 
        1c   |
46 | 37, 45 | syl6bb 252 |
. . . . . . 7
  1c    ∼ 
        
 1c  ∼ 
        1c    |
47 | | eleq2 2414 |
. . . . . . . . 9
  


    


       |
48 | 47 | imbi2d 307 |
. . . . . . . 8
  
∼   
     
 ∼  


        |
49 | 48 | raleqbi1dv 2816 |
. . . . . . 7
  

∼   
     
  ∼ 
           |
50 | | rex0 3564 |
. . . . . . . . 9

     |
51 | 50 | ax-gen 1546 |
. . . . . . . 8
 
     |
52 | 51 | a1i 10 |
. . . . . . 7
 ∼ 
 
      |
53 | | elsuc 4414 |
. . . . . . . . . 10
  1c 

∼        |
54 | | unieq 3901 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
55 | 54 | compleqd 3246 |
. . . . . . . . . . . . . . . . . . . 20
 ∼  ∼    |
56 | 55 | eleq2d 2420 |
. . . . . . . . . . . . . . . . . . 19
 
∼  ∼     |
57 | | rexeq 2809 |
. . . . . . . . . . . . . . . . . . . . 21
  
    
       |
58 | 57 | abbidv 2468 |
. . . . . . . . . . . . . . . . . . . 20
 


    


      |
59 | 58 | eleq1d 2419 |
. . . . . . . . . . . . . . . . . . 19
  


     
        |
60 | 56, 59 | imbi12d 311 |
. . . . . . . . . . . . . . . . . 18
  
∼   
     
 ∼  


        |
61 | 60 | rspcv 2952 |
. . . . . . . . . . . . . . . . 17
  

∼   
     

∼  


        |
62 | 61 | adantr 451 |
. . . . . . . . . . . . . . . 16
 
∼     ∼ 
         ∼   
         |
63 | 62 | adantl 452 |
. . . . . . . . . . . . . . 15
  Nn  ∼    

∼   
     

∼  


        |
64 | | elin 3220 |
. . . . . . . . . . . . . . . . 17
 ∼  ∼     
∼ 
∼       |
65 | | simp3l 983 |
. . . . . . . . . . . . . . . . . . 19
  Nn  ∼ 

∼ 
∼      ∼    |
66 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
67 | 66 | unisn 3908 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
68 | 67 | compleqi 3245 |
. . . . . . . . . . . . . . . . . . . . . 22
∼    ∼  |
69 | 68 | eleq2i 2417 |
. . . . . . . . . . . . . . . . . . . . 21
 ∼   
∼   |
70 | 69 | anbi2i 675 |
. . . . . . . . . . . . . . . . . . . 20
  ∼

∼      ∼  ∼    |
71 | | simpr 447 |
. . . . . . . . . . . . . . . . . . . . . 22
   Nn  ∼ 

∼ 
∼    
    
  
       |
72 | | simpl2r 1009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   Nn  ∼ 

∼ 
∼    ∼   |
73 | 66 | elcompl 3226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 ∼   |
74 | 72, 73 | sylib 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   Nn  ∼ 

∼ 
∼      |
75 | | eleq1a 2422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
76 | 75 | adantl 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   Nn  ∼ 

∼ 
∼        |
77 | 74, 76 | mtod 168 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   Nn  ∼ 

∼ 
∼      |
78 | | simpl3r 1011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   Nn  ∼ 

∼ 
∼    ∼   |
79 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
80 | 79 | elcompl 3226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 ∼   |
81 | 78, 80 | sylib 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   Nn  ∼ 

∼ 
∼      |
82 | | simp3l 983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  Nn  ∼ 

∼ 
∼   ∼    |
83 | 79 | elcompl 3226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 ∼     |
84 | 82, 83 | sylib 188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  Nn  ∼ 

∼ 
∼      |
85 | | elunii 3897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
    |
86 | 85 | expcom 424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
    |
87 | 86 | con3d 125 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
    |
88 | 84, 87 | mpan9 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   Nn  ∼ 

∼ 
∼      |
89 | | adj11 3890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
       |
90 | 81, 88, 89 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   Nn  ∼ 

∼ 
∼        
       |
91 | 77, 90 | mtbird 292 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   Nn  ∼ 

∼ 
∼       
      |
92 | 91 | nrexdv 2718 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  Nn  ∼ 

∼ 
∼   
          |
93 | | eqeq1 2359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
               |
94 | 93 | rexbidv 2636 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                       |
95 | 94 | elabg 2987 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
           
                   |
96 | 95 | ibi 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       
          |
97 | 92, 96 | nsyl 113 |
. . . . . . . . . . . . . . . . . . . . . . 23
  Nn  ∼ 

∼ 
∼      
         |
98 | 97 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . 22
   Nn  ∼ 

∼ 
∼    
    
     


      |
99 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 |
100 | 66, 99 | unex 4107 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 |
101 | 100 | elsuci 4415 |
. . . . . . . . . . . . . . . . . . . . . 22
   
        
         


     
     
1c  |
102 | 71, 98, 101 | syl2anc 642 |
. . . . . . . . . . . . . . . . . . . . 21
   Nn  ∼ 

∼ 
∼    
    
   
            
1c  |
103 | 102 | ex 423 |
. . . . . . . . . . . . . . . . . . . 20
  Nn  ∼ 

∼ 
∼             
            
1c   |
104 | 70, 103 | syl3an3b 1220 |
. . . . . . . . . . . . . . . . . . 19
  Nn  ∼ 

∼ 
∼       


      
            
1c   |
105 | 65, 104 | embantd 50 |
. . . . . . . . . . . . . . . . . 18
  Nn  ∼ 

∼ 
∼       
∼   
     
 


     
     
1c   |
106 | 105 | 3expia 1153 |
. . . . . . . . . . . . . . . . 17
  Nn  ∼    
∼ 
∼      
∼   
     
 


     
     
1c    |
107 | 64, 106 | syl5bi 208 |
. . . . . . . . . . . . . . . 16
  Nn  ∼   
∼  ∼       ∼ 
          
            
1c    |
108 | 107 | com23 72 |
. . . . . . . . . . . . . . 15
  Nn  ∼    
∼   
     

∼  ∼       
            
1c    |
109 | 63, 108 | syld 40 |
. . . . . . . . . . . . . 14
  Nn  ∼    

∼   
     

∼  ∼       
            
1c    |
110 | 109 | imp 418 |
. . . . . . . . . . . . 13
   Nn  ∼   

∼  


      
∼  ∼       
            
1c   |
111 | 110 | an32s 779 |
. . . . . . . . . . . 12
   Nn   ∼ 
          ∼   
∼  ∼
   
 


     
     
1c   |
112 | | unieq 3901 |
. . . . . . . . . . . . . . . 16
     
 
     |
113 | 112 | compleqd 3246 |
. . . . . . . . . . . . . . 15
     ∼  ∼        |
114 | | uniun 3911 |
. . . . . . . . . . . . . . . . 17
    
       |
115 | 114 | compleqi 3245 |
. . . . . . . . . . . . . . . 16
∼     
∼        |
116 | | iunin 3548 |
. . . . . . . . . . . . . . . 16
∼      
∼  ∼
     |
117 | 115, 116 | eqtri 2373 |
. . . . . . . . . . . . . . 15
∼     
∼  ∼      |
118 | 113, 117 | syl6eq 2401 |
. . . . . . . . . . . . . 14
     ∼  ∼  ∼       |
119 | 118 | eleq2d 2420 |
. . . . . . . . . . . . 13
     
∼ 
∼  ∼        |
120 | | rexeq 2809 |
. . . . . . . . . . . . . . . 16
                        |
121 | 120 | abbidv 2468 |
. . . . . . . . . . . . . . 15
     


    
             |
122 | | unab 3522 |
. . . . . . . . . . . . . . . 16
 


    

     
 
   
       |
123 | | df-sn 3742 |
. . . . . . . . . . . . . . . . 17
      
      |
124 | 123 | uneq2i 3416 |
. . . . . . . . . . . . . . . 16
 


     
       
     
       |
125 | | rexun 3444 |
. . . . . . . . . . . . . . . . . 18
 
    
                     |
126 | | uneq1 3412 |
. . . . . . . . . . . . . . . . . . . . 21
    
      |
127 | 126 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . . . . 20
 
   
       |
128 | 66, 127 | rexsn 3769 |
. . . . . . . . . . . . . . . . . . 19
 
  
          |
129 | 128 | orbi2i 505 |
. . . . . . . . . . . . . . . . . 18
  
              
           |
130 | 125, 129 | bitri 240 |
. . . . . . . . . . . . . . . . 17
 
    
                 |
131 | 130 | abbii 2466 |
. . . . . . . . . . . . . . . 16
            
 
           |
132 | 122, 124,
131 | 3eqtr4ri 2384 |
. . . . . . . . . . . . . . 15
              
             |
133 | 121, 132 | syl6eq 2401 |
. . . . . . . . . . . . . 14
     


      
              |
134 | 133 | eleq1d 2419 |
. . . . . . . . . . . . 13
       
     
1c
 


     
     
1c   |
135 | 119, 134 | imbi12d 311 |
. . . . . . . . . . . 12
       ∼   
     
1c  ∼  ∼       
            
1c    |
136 | 111, 135 | syl5ibrcom 213 |
. . . . . . . . . . 11
   Nn   ∼ 
          ∼   
     ∼ 
        1c    |
137 | 136 | rexlimdvva 2746 |
. . . . . . . . . 10
  Nn   ∼ 
          

∼      
∼  


    
1c    |
138 | 53, 137 | syl5bi 208 |
. . . . . . . . 9
  Nn   ∼ 
           1c  ∼   
     
1c    |
139 | 138 | ralrimiv 2697 |
. . . . . . . 8
  Nn   ∼ 
          
1c  ∼ 
        1c   |
140 | 139 | ex 423 |
. . . . . . 7
 Nn    ∼ 
         
1c  ∼ 
        1c    |
141 | 9, 31, 34, 46, 49, 52, 140 | finds 4412 |
. . . . . 6
 Nn  
∼   
        |
142 | | unieq 3901 |
. . . . . . . . . 10
 
   |
143 | 142 | compleqd 3246 |
. . . . . . . . 9
 ∼  ∼    |
144 | 143 | eleq2d 2420 |
. . . . . . . 8
 
∼  ∼     |
145 | | rexeq 2809 |
. . . . . . . . . 10
  
    
       |
146 | 145 | abbidv 2468 |
. . . . . . . . 9
 


    
        |
147 | 146 | eleq1d 2419 |
. . . . . . . 8
  


    
         |
148 | 144, 147 | imbi12d 311 |
. . . . . . 7
  
∼   
     
 ∼  
          |
149 | 148 | rspccv 2953 |
. . . . . 6
 

∼  


       ∼ 
 
    
    |
150 | 141, 149 | syl 15 |
. . . . 5
 Nn   ∼   
         |
151 | 150 | com3r 73 |
. . . 4
 ∼  
Nn   
         |
152 | 8, 151 | vtoclga 2921 |
. . 3
 ∼  
Nn   
         |
153 | 152 | com3l 75 |
. 2
 Nn   ∼   
         |
154 | 153 | 3imp 1145 |
1
  Nn ∼
   
       |