Step | Hyp | Ref
| Expression |
1 | | dffi2 7937 |
. . . 4
       
 

     |
2 | | fr0g 7153 |
. . . . . . . 8
             |
3 | | frfnom 7152 |
. . . . . . . . 9
       |
4 | | peano1 6712 |
. . . . . . . . 9
 |
5 | | fnfvelrn 6019 |
. . . . . . . . 9
       
              
    |
6 | 3, 4, 5 | mp2an 678 |
. . . . . . . 8
                 |
7 | 2, 6 | syl6eqelr 2538 |
. . . . . . 7
    
    |
8 | | elssuni 4227 |
. . . . . . 7
                |
9 | 7, 8 | syl 17 |
. . . . . 6
 
        |
10 | | reeanv 2958 |
. . . . . . . . 9
  
               
     
 
    
    
              |
11 | | eliun 4283 |
. . . . . . . . . 10
           
             |
12 | | eliun 4283 |
. . . . . . . . . 10
           
             |
13 | 11, 12 | anbi12i 703 |
. . . . . . . . 9
                  
     
 
    
    
              |
14 | | fniunfv 6152 |
. . . . . . . . . . . 12
      
                    |
15 | 14 | eleq2d 2514 |
. . . . . . . . . . 11
      
      
               |
16 | | fniunfv 6152 |
. . . . . . . . . . . 12
      
                    |
17 | 16 | eleq2d 2514 |
. . . . . . . . . . 11
      
      
               |
18 | 15, 17 | anbi12d 717 |
. . . . . . . . . 10
      
                  
     
       
           |
19 | 3, 18 | ax-mp 5 |
. . . . . . . . 9
                  
     
       
          |
20 | 10, 13, 19 | 3bitr2i 277 |
. . . . . . . 8
  
               
     
       
          |
21 | | ordom 6701 |
. . . . . . . . . . . . . . . 16
 |
22 | | ordunel 6654 |
. . . . . . . . . . . . . . . 16
       |
23 | 21, 22 | mp3an1 1351 |
. . . . . . . . . . . . . . 15
 
     |
24 | 23 | adantl 468 |
. . . . . . . . . . . . . 14
  
 
    |
25 | | simprl 764 |
. . . . . . . . . . . . . 14
  
 
  |
26 | 24, 25 | jca 535 |
. . . . . . . . . . . . 13
  
 
      |
27 | | nnon 6698 |
. . . . . . . . . . . . . . . . . . 19
   |
28 | 27 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
  
    |
29 | | nnon 6698 |
. . . . . . . . . . . . . . . . . . 19
   |
30 | 29 | ad2antlr 733 |
. . . . . . . . . . . . . . . . . 18
  
    |
31 | | onsseleq 5464 |
. . . . . . . . . . . . . . . . . 18
 
       |
32 | 28, 30, 31 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
  
   
    |
33 | | rzal 3871 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26


                      |
34 | 33 | biantrud 510 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

              
               
                        |
35 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

                      |
36 | 35 | sseq1d 3459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

              
         
       |
37 | 34, 36 | bitr3d 259 |
. . . . . . . . . . . . . . . . . . . . . . . 24

      
    
    
                    
         
       |
38 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                       |
39 | 38 | sseq1d 3459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
    
   
                 |
40 | 38 | sseq2d 3460 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
    
         
                       |
41 | 40 | raleqbi1dv 2995 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
    
    
         

                       |
42 | 39, 41 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                      
               
                        |
43 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
                 |
44 | 43 | sseq1d 3459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               
                 |
45 | 43 | sseq2d 3460 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                          
    
             |
46 | 45 | raleqbi1dv 2995 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                       
                        |
47 | 44, 46 | anbi12d 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                      
          
    
                         |
48 | | ssfii 7933 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
49 | 2, 48 | eqsstrd 3466 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
50 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
               
       |
51 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
             |
52 | | ineq1 3627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
     |
53 | 52 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   

    |
54 | | ineq2 3628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 
     |
55 | | inidm 3641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   |
56 | 54, 55 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
   |
57 | 56 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
   
   |
58 | 53, 57 | rspc2ev 3161 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                
    
      
           
          |
59 | 50, 50, 51, 58 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                
           
          |
60 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                              
          
         |
61 | 60 | rnmpt2 6406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                                      |
62 | 61 | abeq2i 2563 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                          
                           |
63 | 59, 62 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                
          
          |
64 | 63 | ssriv 3436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                    |
65 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
    
    
  |
66 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           |
67 | 66 | uniex 6587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
            |
68 | 67 | pwex 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
      
      |
69 | | inss1 3652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   |
70 | | elssuni 4227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
                        |
71 | 70 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                
                   |
72 | 69, 71 | syl5ss 3443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                
      
              |
73 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
 |
74 | 73 | inex1 4544 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
   |
75 | 74 | elpw 3957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                
             |
76 | 72, 75 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                
      
               |
77 | 76 | rgen2a 2815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     
           
              
      |
78 | 60 | fmpt2 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
                
              
          
          
                                                |
79 | 77, 78 | mpbi 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                                                |
80 | | frn 5735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                                               
     
          
                      |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                      |
82 | 68, 81 | ssexi 4548 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                          |
83 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
84 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
85 | | nfcv 2592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                            |
86 | | dffi3.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
  
     |
87 | | mpt2eq12 6351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 
  
          |
88 | 87 | anidms 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
             |
89 | | ineq1 3627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 
     |
90 | | ineq2 3628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 
     |
91 | 89, 90 | cbvmpt2v 6371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
           |
92 | 88, 91 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
             |
93 | 92 | rneqd 5062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
  
          |
94 | 93 | cbvmptv 4495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
               |
95 | 86, 94 | eqtri 2473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
        |
96 | | rdgeq1 7129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
            
          |
97 | 95, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
  
             |
98 | 97 | reseq1i 5101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                    |
99 | | mpt2eq12 6351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                                                       |
100 | 99 | anidms 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                                           |
101 | 100 | rneqd 5062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                                           |
102 | 83, 84, 85, 98, 101 | frsucmpt 7155 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                                                                 |
103 | 65, 82, 102 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      
    
         
                                |
104 | 64, 103 | syl5sseqr 3481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      
    
         
    
            |
105 | | sstr2 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                          
    
                                 |
106 | 104, 105 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      
    
                                                 |
107 | 106 | ralimdv 2798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
    
                                
    
             |
108 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 |
109 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                       |
110 | 109 | sseq1d 3459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      
    
         
                       |
111 | 108, 110 | ralsn 4010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
                                            |
112 | 104, 111 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
    
     
                        |
113 | 107, 112 | jctird 547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
    
                            
                   
                           |
114 | | df-suc 5429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
115 | 114 | raleqi 2991 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
                    
                            |
116 | | ralunb 3615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
         
    
         
 
                    
                         |
117 | 115, 116 | bitri 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
                    
 
                    
                         |
118 | 113, 117 | syl6ibr 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
    
                                                    |
119 | | fiin 7936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
             |
120 | 119 | rgen2a 2815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                   |
121 | | ssralv 3493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                
                
               |
122 | 121 | ralimdv 2798 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                
     
          
           
               |
123 | | ssralv 3493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                
     
                
     
           
               |
124 | 122, 123 | syld 45 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                
     
          
     
           
               |
125 | 120, 124 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                    
           
              |
126 | 60 | fmpt2 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
                
                                            
                        |
127 | 125, 126 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                                                        |
128 | | frn 5735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                                                                       |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                                              |
130 | 129 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
    
                                    |
131 | 103, 130 | eqsstrd 3466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
    
         
           |
132 | 118, 131 | jctild 546 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
    
                                                                    |
133 | 132 | expimpd 608 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                                            
    
              |
134 | 133 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                                                           
    
               |
135 | 37, 42, 47, 49, 134 | finds2 6721 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     
    
    
                        |
136 | 135 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                                        |
137 | 136 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . 21
 
      
    
            |
138 | 137 | r19.21bi 2757 |
. . . . . . . . . . . . . . . . . . . 20
  
 
                      |
139 | 138 | ex 436 |
. . . . . . . . . . . . . . . . . . 19
 
      
    
             |
140 | 139 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
  
  
                       |
141 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . 20
                       |
142 | | eqimss 3484 |
. . . . . . . . . . . . . . . . . . . 20
                                           |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
                       |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
  
  
                       |
145 | 140, 144 | jaod 382 |
. . . . . . . . . . . . . . . . 17
  
                            |
146 | 32, 145 | sylbid 219 |
. . . . . . . . . . . . . . . 16
  
                          |
147 | 146 | ralrimiva 2802 |
. . . . . . . . . . . . . . 15
 
       
    
             |
148 | 147 | ralrimiva 2802 |
. . . . . . . . . . . . . 14
                           |
149 | 148 | adantr 467 |
. . . . . . . . . . . . 13
  
 
                          |
150 | | ssun1 3597 |
. . . . . . . . . . . . . 14

  |
151 | 150 | a1i 11 |
. . . . . . . . . . . . 13
  
 
    |
152 | | sseq2 3454 |
. . . . . . . . . . . . . . 15
   

    |
153 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
                      
    |
154 | 153 | sseq2d 3460 |
. . . . . . . . . . . . . . 15
        
    
         
                         |
155 | 152, 154 | imbi12d 322 |
. . . . . . . . . . . . . 14
         
    
          
  
                          |
156 | | sseq1 3453 |
. . . . . . . . . . . . . . 15
 
 
     |
157 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
                       |
158 | 157 | sseq1d 3459 |
. . . . . . . . . . . . . . 15
      
    
         
 
                         |
159 | 156, 158 | imbi12d 322 |
. . . . . . . . . . . . . 14
                             

                          |
160 | 155, 159 | rspc2v 3159 |
. . . . . . . . . . . . 13
   
         
    
                                        |
161 | 26, 149, 151, 160 | syl3c 63 |
. . . . . . . . . . . 12
  
 
                        |
162 | 161 | sseld 3431 |
. . . . . . . . . . 11
  
 
     
    
    
          |
163 | | simprr 766 |
. . . . . . . . . . . . . 14
  
 
  |
164 | 24, 163 | jca 535 |
. . . . . . . . . . . . 13
  
 
      |
165 | | ssun2 3598 |
. . . . . . . . . . . . . 14

  |
166 | 165 | a1i 11 |
. . . . . . . . . . . . 13
  
 
    |
167 | | sseq1 3453 |
. . . . . . . . . . . . . . 15
 
 
     |
168 | 109 | sseq1d 3459 |
. . . . . . . . . . . . . . 15
      
    
         
 
                         |
169 | 167, 168 | imbi12d 322 |
. . . . . . . . . . . . . 14
                             

                          |
170 | 155, 169 | rspc2v 3159 |
. . . . . . . . . . . . 13
   
         
    
                                        |
171 | 164, 149,
166, 170 | syl3c 63 |
. . . . . . . . . . . 12
  
 
                        |
172 | 171 | sseld 3431 |
. . . . . . . . . . 11
  
 
     
    
    
          |
173 | 23 | ad2antlr 733 |
. . . . . . . . . . . . . . 15
     
     
           
             |
174 | | peano2 6713 |
. . . . . . . . . . . . . . 15
   
   |
175 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
       
                   |
176 | 175 | ssiun2s 4322 |
. . . . . . . . . . . . . . 15
              
             |
177 | 173, 174,
176 | 3syl 18 |
. . . . . . . . . . . . . 14
     
     
           
             
    
               |
178 | | simprl 764 |
. . . . . . . . . . . . . . . . . 18
     
     
           
                       |
179 | | simprr 766 |
. . . . . . . . . . . . . . . . . 18
     
     
           
                       |
180 | | eqidd 2452 |
. . . . . . . . . . . . . . . . . 18
     
     
           
               |
181 | | ineq1 3627 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
182 | 181 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . . 19
     
       |
183 | | ineq2 3628 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
184 | 183 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . . 19
     
       |
185 | 182, 184 | rspc2ev 3161 |
. . . . . . . . . . . . . . . . . 18
                  
                 
             
              |
186 | 178, 179,
180, 185 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
     
     
           
         
                                 |
187 | | vex 3048 |
. . . . . . . . . . . . . . . . . . 19
 |
188 | 187 | inex1 4544 |
. . . . . . . . . . . . . . . . . 18
   |
189 | | eqeq1 2455 |
. . . . . . . . . . . . . . . . . . 19
     
       |
190 | 189 | 2rexbidv 2908 |
. . . . . . . . . . . . . . . . . 18
    
                            
     
             
               |
191 | 188, 190 | elab 3185 |
. . . . . . . . . . . . . . . . 17
                                   
                                 |
192 | 186, 191 | sylibr 216 |
. . . . . . . . . . . . . . . 16
     
     
           
                                             |
193 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
          
            
          
            
           |
194 | 193 | rnmpt2 6406 |
. . . . . . . . . . . . . . . 16
                       
                                      |
195 | 192, 194 | syl6eleqr 2540 |
. . . . . . . . . . . . . . 15
     
     
           
                                  
       |
196 | | fvex 5875 |
. . . . . . . . . . . . . . . . . . 19
             |
197 | 196 | uniex 6587 |
. . . . . . . . . . . . . . . . . 18
              |
198 | 197 | pwex 4586 |
. . . . . . . . . . . . . . . . 17
      
        |
199 | | elssuni 4227 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
            
    |
200 | 69, 199 | syl5ss 3443 |
. . . . . . . . . . . . . . . . . . . . . 22
          
  
           
    |
201 | 74 | elpw 3957 |
. . . . . . . . . . . . . . . . . . . . . 22
                  
               |
202 | 200, 201 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . 21
          
  
                 |
203 | 202 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
                  
        
                 |
204 | 203 | rgen2a 2815 |
. . . . . . . . . . . . . . . . . . 19
     
             
                
        |
205 | 193 | fmpt2 6860 |
. . . . . . . . . . . . . . . . . . 19
 
         
        
                
            
            
                      
                                 |
206 | 204, 205 | mpbi 212 |
. . . . . . . . . . . . . . . . . 18
          
            
                                                  |
207 | | frn 5735 |
. . . . . . . . . . . . . . . . . 18
                        
                                                
     
            
                     
    |
208 | 206, 207 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
                       
                    |
209 | 198, 208 | ssexi 4548 |
. . . . . . . . . . . . . . . 16
                       
      |
210 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
     |
211 | | nfcv 2592 |
. . . . . . . . . . . . . . . . 17
                                |
212 | | mpt2eq12 6351 |
. . . . . . . . . . . . . . . . . . 19
                       
                               
       |
213 | 212 | anidms 651 |
. . . . . . . . . . . . . . . . . 18
          
                 
            
       |
214 | 213 | rneqd 5062 |
. . . . . . . . . . . . . . . . 17
          
                                      |
215 | 83, 210, 211, 98, 214 | frsucmpt 7155 |
. . . . . . . . . . . . . . . 16
                                                                             |
216 | 173, 209,
215 | sylancl 668 |
. . . . . . . . . . . . . . 15
     
     
           
             
    
                                 |
217 | 195, 216 | eleqtrrd 2532 |
. . . . . . . . . . . . . 14
     
     
           
                         |
218 | 177, 217 | sseldd 3433 |
. . . . . . . . . . . . 13
     
     
           
                        |
219 | | fniunfv 6152 |
. . . . . . . . . . . . . 14
      
                    |
220 | 3, 219 | ax-mp 5 |
. . . . . . . . . . . . 13
                   |
221 | 218, 220 | syl6eleq 2539 |
. . . . . . . . . . . 12
     
     
           
                    |
222 | 221 | ex 436 |
. . . . . . . . . . 11
  
 
                  
        
           |
223 | 162, 172,
222 | syl2and 486 |
. . . . . . . . . 10
  
 
                
      
           |
224 | 223 | rexlimdvva 2886 |
. . . . . . . . 9
  
                
      
           |
225 | 224 | imp 431 |
. . . . . . . 8
   
               
                  |
226 | 20, 225 | sylan2br 479 |
. . . . . . 7
         
        
           |
227 | 226 | ralrimivva 2809 |
. . . . . 6
          
                   |
228 | 136 | simpld 461 |
. . . . . . . . . . . 12
 
     
    
      |
229 | | fvex 5875 |
. . . . . . . . . . . . 13
     |
230 | 229 | elpw2 4567 |
. . . . . . . . . . . 12
               
                |
231 | 228, 230 | sylibr 216 |
. . . . . . . . . . 11
 
     
            |
232 | 231 | ralrimiva 2802 |
. . . . . . . . . 10
                   |
233 | | fnfvrnss 6051 |
. . . . . . . . . 10
       
                
             |
234 | 3, 232, 233 | sylancr 669 |
. . . . . . . . 9
              |
235 | | sspwuni 4367 |
. . . . . . . . 9
      
    
             |
236 | 234, 235 | sylib 200 |
. . . . . . . 8
              |
237 | | ssexg 4549 |
. . . . . . . 8
                           |
238 | 236, 229,
237 | sylancl 668 |
. . . . . . 7
          |
239 | | sseq2 3454 |
. . . . . . . . 9
                   |
240 | | eleq2 2518 |
. . . . . . . . . . 11
                       |
241 | 240 | raleqbi1dv 2995 |
. . . . . . . . . 10
                                 |
242 | 241 | raleqbi1dv 2995 |
. . . . . . . . 9
                      
                    |
243 | 239, 242 | anbi12d 717 |
. . . . . . . 8
                    
  
        
                     |
244 | 243 | elabg 3186 |
. . . . . . 7
       
         
 

  
 
      
        
                     |
245 | 238, 244 | syl 17 |
. . . . . 6
      
    


  
 
      
        
                     |
246 | 9, 227, 245 | mpbir2and 933 |
. . . . 5
         
 

     |
247 | | intss1 4249 |
. . . . 5
       
                          |
248 | 246, 247 | syl 17 |
. . . 4
                   |
249 | 1, 248 | eqsstrd 3466 |
. . 3
         
    |
250 | 249, 236 | eqssd 3449 |
. 2
     
        |
251 | | df-ima 4847 |
. . 3
           
   |
252 | 251 | unieqi 4207 |
. 2
                 |
253 | 250, 252 | syl6eqr 2503 |
1
         
      |