Step | Hyp | Ref
| Expression |
1 | | fpwwe2.4 |
. . . . 5

 |
2 | | vex 3050 |
. . . . . . . . 9
 |
3 | 2 | eldm 5035 |
. . . . . . . 8

     |
4 | | fpwwe2.1 |
. . . . . . . . . . . . . 14
   
 
              ![]. ].](_drbrack.gif)             |
5 | | fpwwe2.2 |
. . . . . . . . . . . . . 14
   |
6 | 4, 5 | fpwwe2lem2 9062 |
. . . . . . . . . . . . 13
          
         ![]. ].](_drbrack.gif)              |
7 | 6 | simprbda 629 |
. . . . . . . . . . . 12
 
   
     |
8 | 7 | simpld 461 |
. . . . . . . . . . 11
 
     |
9 | | selpw 3960 |
. . . . . . . . . . 11
 
  |
10 | 8, 9 | sylibr 216 |
. . . . . . . . . 10
 
      |
11 | 10 | ex 436 |
. . . . . . . . 9
        |
12 | 11 | exlimdv 1781 |
. . . . . . . 8
         |
13 | 3, 12 | syl5bi 221 |
. . . . . . 7
      |
14 | 13 | ssrdv 3440 |
. . . . . 6
    |
15 | | sspwuni 4370 |
. . . . . 6

 
  |
16 | 14, 15 | sylib 200 |
. . . . 5
    |
17 | 1, 16 | syl5eqss 3478 |
. . . 4

  |
18 | | vex 3050 |
. . . . . . . 8
 |
19 | 18 | elrn 5078 |
. . . . . . 7

     |
20 | 7 | simprd 465 |
. . . . . . . . . . 11
 
       |
21 | 4 | relopabi 4962 |
. . . . . . . . . . . . . . . 16
 |
22 | 21 | releldmi 5074 |
. . . . . . . . . . . . . . 15
     |
23 | 22 | adantl 468 |
. . . . . . . . . . . . . 14
 
     |
24 | | elssuni 4230 |
. . . . . . . . . . . . . 14

   |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . 13
 
   
  |
26 | 25, 1 | syl6sseqr 3481 |
. . . . . . . . . . . 12
 
     |
27 | | xpss12 4943 |
. . . . . . . . . . . 12
 
  
    |
28 | 26, 26, 27 | syl2anc 667 |
. . . . . . . . . . 11
 
         |
29 | 20, 28 | sstrd 3444 |
. . . . . . . . . 10
 
       |
30 | | selpw 3960 |
. . . . . . . . . 10
   

   |
31 | 29, 30 | sylibr 216 |
. . . . . . . . 9
 
        |
32 | 31 | ex 436 |
. . . . . . . 8
     
    |
33 | 32 | exlimdv 1781 |
. . . . . . 7
           |
34 | 19, 33 | syl5bi 221 |
. . . . . 6
   
    |
35 | 34 | ssrdv 3440 |
. . . . 5
  
   |
36 | | sspwuni 4370 |
. . . . 5

  
     |
37 | 35, 36 | sylib 200 |
. . . 4
  
   |
38 | 17, 37 | jca 535 |
. . 3
   
    |
39 | | n0 3743 |
. . . . . . . . 9
    |
40 | | ssel2 3429 |
. . . . . . . . . . . . . 14
 
   |
41 | 40 | adantl 468 |
. . . . . . . . . . . . 13
 
     |
42 | 1 | eleq2i 2523 |
. . . . . . . . . . . . . 14

   |
43 | | eluni2 4205 |
. . . . . . . . . . . . . 14
  
  |
44 | 42, 43 | bitri 253 |
. . . . . . . . . . . . 13

   |
45 | 41, 44 | sylib 200 |
. . . . . . . . . . . 12
 
   
  |
46 | 2 | inex2 4548 |
. . . . . . . . . . . . . . . . . . 19
   |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   
 
         |
48 | 6 | simplbda 630 |
. . . . . . . . . . . . . . . . . . . . 21
 
              ![]. ].](_drbrack.gif)            |
49 | 48 | simpld 461 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
50 | 49 | ad2ant2r 754 |
. . . . . . . . . . . . . . . . . . 19
   
 
       |
51 | | wefr 4827 |
. . . . . . . . . . . . . . . . . . 19
   |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   
 
       |
53 | | inss2 3655 |
. . . . . . . . . . . . . . . . . . 19
   |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   
 
      
  |
55 | | simplrr 772 |
. . . . . . . . . . . . . . . . . . 19
   
 
       |
56 | | simprr 767 |
. . . . . . . . . . . . . . . . . . 19
   
 
       |
57 | | inelcm 3821 |
. . . . . . . . . . . . . . . . . . 19
 
     |
58 | 55, 56, 57 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
   
 
         |
59 | | fri 4799 |
. . . . . . . . . . . . . . . . . 18
                        |
60 | 47, 52, 54, 58, 59 | syl22anc 1270 |
. . . . . . . . . . . . . . . . 17
   
 
     

  

     |
61 | | inss1 3654 |
. . . . . . . . . . . . . . . . . . . . 21
   |
62 | | simprl 765 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
                   |
63 | 61, 62 | sseldi 3432 |
. . . . . . . . . . . . . . . . . . . 20
    
 
                 |
64 | | simplrr 772 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
    
 
  
      
        |
65 | | ralnex 2836 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   
        |
66 | 64, 65 | sylib 200 |
. . . . . . . . . . . . . . . . . . . . . 22
     
    
 
  
      
         |
67 | | df-br 4406 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
68 | | eluni2 4205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
       |
69 | 67, 68 | bitri 253 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      |
70 | | vex 3050 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
71 | 70 | elrn 5078 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

     |
72 | | df-br 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
  
  
  |
73 | | simprll 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
    
 
  
                  |
74 | 73 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
                                    |
75 | | simprr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     
    
 
  
                    |
76 | | simp-4l 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
     
    
 
  
                  |
77 | | simprl 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
   
 
         |
78 | 77 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
     
    
 
  
                    |
79 | | simprlr 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
     
    
 
  
                    |
80 | | simprr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
           |
81 | 4, 5 | fpwwe2lem2 9062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
          
         ![]. ].](_drbrack.gif)              |
82 | 81 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
                          ![]. ].](_drbrack.gif)              |
83 | 80, 82 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 
                       ![]. ].](_drbrack.gif)             |
84 | 83 | simpld 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 
             |
85 | 84 | simprd 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 
           |
86 | 76, 78, 79, 85 | syl12anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
     
    
 
  
                    |
87 | 86 | ssbrd 4447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
     
    
 
  
                  
       |
88 | 75, 87 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
     
    
 
  
                      |
89 | | brxp 4868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
    

   |
90 | 89 | simplbi 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       |
91 | 88, 90 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     
    
 
  
                  |
92 | 91 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     
                                    |
93 | 53, 62 | sseldi 3432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
 
                 |
94 | 93 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     
                                    |
95 | | simplrr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     
                                      |
96 | | brinxp2 4899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
      

     |
97 | 92, 94, 95, 96 | syl3anbrc 1193 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
                                          |
98 | | simprr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     
                                        |
99 | 98 | breqd 4416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
                                              |
100 | 97, 99 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
                                      |
101 | 76, 78, 20 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     
    
 
  
                    |
102 | 101 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     
                                      |
103 | 102 | ssbrd 4447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
                                    
       |
104 | 100, 103 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
                                        |
105 | | brxp 4868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    

   |
106 | 105 | simplbi 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
       |
107 | 104, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
                                    |
108 | 74, 107 | elind 3620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
                                      |
109 | | breq1 4408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
     |
110 | 109 | rspcev 3152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
               |
111 | 108, 100,
110 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                                          |
112 | 73 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
                                    |
113 | | simprl 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
                                    |
114 | 91 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
                                    |
115 | 113, 114 | sseldd 3435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
                                    |
116 | 112, 115 | elind 3620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
                                      |
117 | | simplrr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
                                      |
118 | | simprr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
                                        |
119 | | inss1 3654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
120 | 118, 119 | syl6eqss 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
                                    |
121 | 120 | ssbrd 4447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
                                    
     |
122 | 117, 121 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
                                      |
123 | 116, 122,
110 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                                          |
124 | 5 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
         |
125 | | fpwwe2.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
 

        |
126 | 125 | adantlr 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                     |
127 | | simprl 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
           |
128 | 4, 124, 126, 127, 80 | fpwwe2lem10 9069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
              

       |
129 | 76, 78, 79, 128 | syl12anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
    
 
  
                       

       |
130 | 111, 123,
129 | mpjaodan 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
    
 
  
                        |
131 | 130 | expr 620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
    
 
  
       
   
            |
132 | 72, 131 | syl5bir 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
    
 
  
       
   
             |
133 | 132 | expr 620 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
    
 
  
      
                  |
134 | 133 | exlimdv 1781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
    
 
  
      
        
          |
135 | 71, 134 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
    
 
  
      
                |
136 | 135 | rexlimdv 2879 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
    
 
  
      
                |
137 | 69, 136 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . . . 22
     
    
 
  
      
   
         |
138 | 66, 137 | mtod 181 |
. . . . . . . . . . . . . . . . . . . . 21
     
    
 
  
      
     |
139 | 138 | ralrimiva 2804 |
. . . . . . . . . . . . . . . . . . . 20
    
 
               
    |
140 | 63, 139 | jca 535 |
. . . . . . . . . . . . . . . . . . 19
    
 
                      |
141 | 140 | ex 436 |
. . . . . . . . . . . . . . . . . 18
   
 
        
              |
142 | 141 | reximdv2 2860 |
. . . . . . . . . . . . . . . . 17
   
 
              


     |
143 | 60, 142 | mpd 15 |
. . . . . . . . . . . . . . . 16
   
 
     

    |
144 | 143 | exp32 610 |
. . . . . . . . . . . . . . 15
 
      


      |
145 | 144 | exlimdv 1781 |
. . . . . . . . . . . . . 14
 
        

      |
146 | 3, 145 | syl5bi 221 |
. . . . . . . . . . . . 13
 
    


      |
147 | 146 | rexlimdv 2879 |
. . . . . . . . . . . 12
 
    
 
     |
148 | 45, 147 | mpd 15 |
. . . . . . . . . . 11
 
   

    |
149 | 148 | expr 620 |
. . . . . . . . . 10
 




     |
150 | 149 | exlimdv 1781 |
. . . . . . . . 9
 

 
 
     |
151 | 39, 150 | syl5bi 221 |
. . . . . . . 8
 




     |
152 | 151 | expimpd 608 |
. . . . . . 7
    

     |
153 | 152 | alrimiv 1775 |
. . . . . 6
    
 

     |
154 | | df-fr 4796 |
. . . . . 6
 
     

     |
155 | 153, 154 | sylibr 216 |
. . . . 5
    |
156 | 1 | eleq2i 2523 |
. . . . . . . . . 10

   |
157 | | eluni2 4205 |
. . . . . . . . . 10
  
  |
158 | 156, 157 | bitri 253 |
. . . . . . . . 9

   |
159 | 44, 158 | anbi12i 704 |
. . . . . . . 8
 
   
   |
160 | | reeanv 2960 |
. . . . . . . 8
   
         |
161 | 159, 160 | bitr4i 256 |
. . . . . . 7
 
   
     |
162 | | vex 3050 |
. . . . . . . . . . . 12
 |
163 | 162 | eldm 5035 |
. . . . . . . . . . 11

     |
164 | 3, 163 | anbi12i 704 |
. . . . . . . . . 10
 
           |
165 | | eeanv 2080 |
. . . . . . . . . 10
          
          |
166 | 164, 165 | bitr4i 256 |
. . . . . . . . 9
 
             |
167 | 83 | simprd 465 |
. . . . . . . . . . . . . . . . 17
 
        
         ![]. ].](_drbrack.gif)            |
168 | 167 | simpld 461 |
. . . . . . . . . . . . . . . 16
 
         |
169 | 168 | ad2antrr 733 |
. . . . . . . . . . . . . . 15
           
 
         |
170 | | weso 4828 |
. . . . . . . . . . . . . . 15
   |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . 14
           
 
         |
172 | | simprl 765 |
. . . . . . . . . . . . . . 15
           
 
      
  |
173 | | simplrl 771 |
. . . . . . . . . . . . . . 15
           
 
         |
174 | 172, 173 | sseldd 3435 |
. . . . . . . . . . . . . 14
           
 
         |
175 | | simplrr 772 |
. . . . . . . . . . . . . 14
           
 
      
  |
176 | | solin 4781 |
. . . . . . . . . . . . . 14
             |
177 | 171, 174,
175, 176 | syl12anc 1267 |
. . . . . . . . . . . . 13
           
 
               |
178 | 21 | relelrni 5075 |
. . . . . . . . . . . . . . . . . 18
     |
179 | 178 | ad2antll 736 |
. . . . . . . . . . . . . . . . 17
 
         |
180 | 179 | ad2antrr 733 |
. . . . . . . . . . . . . . . 16
           
 
         |
181 | | elssuni 4230 |
. . . . . . . . . . . . . . . 16

   |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . . . . 15
           
 
      
   |
183 | 182 | ssbrd 4447 |
. . . . . . . . . . . . . 14
           
 
               |
184 | | idd 25 |
. . . . . . . . . . . . . 14
           
 
           |
185 | 182 | ssbrd 4447 |
. . . . . . . . . . . . . 14
           
 
               |
186 | 183, 184,
185 | 3orim123d 1349 |
. . . . . . . . . . . . 13
           
 
                
      |
187 | 177, 186 | mpd 15 |
. . . . . . . . . . . 12
           
 
               |
188 | 49 | adantrr 724 |
. . . . . . . . . . . . . . . 16
 
         |
189 | 188 | ad2antrr 733 |
. . . . . . . . . . . . . . 15
           
 
         |
190 | | weso 4828 |
. . . . . . . . . . . . . . 15
   |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . 14
           
 
         |
192 | | simplrl 771 |
. . . . . . . . . . . . . 14
           
 
         |
193 | | simprl 765 |
. . . . . . . . . . . . . . 15
           
 
      
  |
194 | | simplrr 772 |
. . . . . . . . . . . . . . 15
           
 
      
  |
195 | 193, 194 | sseldd 3435 |
. . . . . . . . . . . . . 14
           
 
      
  |
196 | | solin 4781 |
. . . . . . . . . . . . . 14
             |
197 | 191, 192,
195, 196 | syl12anc 1267 |
. . . . . . . . . . . . 13
           
 
               |
198 | 21 | relelrni 5075 |
. . . . . . . . . . . . . . . . . 18
     |
199 | 198 | ad2antrl 735 |
. . . . . . . . . . . . . . . . 17
 
         |
200 | 199 | ad2antrr 733 |
. . . . . . . . . . . . . . . 16
           
 
         |
201 | | elssuni 4230 |
. . . . . . . . . . . . . . . 16

   |
202 | 200, 201 | syl 17 |
. . . . . . . . . . . . . . 15
           
 
      
   |
203 | 202 | ssbrd 4447 |
. . . . . . . . . . . . . 14
           
 
               |
204 | | idd 25 |
. . . . . . . . . . . . . 14
           
 
           |
205 | 202 | ssbrd 4447 |
. . . . . . . . . . . . . 14
           
 
               |
206 | 203, 204,
205 | 3orim123d 1349 |
. . . . . . . . . . . . 13
           
 
                
      |
207 | 197, 206 | mpd 15 |
. . . . . . . . . . . 12
           
 
               |
208 | 128 | adantr 467 |
. . . . . . . . . . . 12
                             |
209 | 187, 207,
208 | mpjaodan 796 |
. . . . . . . . . . 11
                     |
210 | 209 | exp31 609 |
. . . . . . . . . 10
          
          |
211 | 210 | exlimdvv 1782 |
. . . . . . . . 9
              
          |
212 | 166, 211 | syl5bi 221 |
. . . . . . . 8
  
      
       |
213 | 212 | rexlimdvv 2887 |
. . . . . . 7
          
      |
214 | 161, 213 | syl5bi 221 |
. . . . . 6
      
      |
215 | 214 | ralrimivv 2810 |
. . . . 5
  
        |
216 | | dfwe2 6613 |
. . . . 5
 
   
  
      |
217 | 155, 215,
216 | sylanbrc 671 |
. . . 4
    |
218 | 4 | fpwwe2cbv 9060 |
. . . . . . . . . . . . 13
   
 
              ![]. ].](_drbrack.gif)             |
219 | 5 | adantr 467 |
. . . . . . . . . . . . 13
 
     |
220 | | simpr 463 |
. . . . . . . . . . . . 13
 
       |
221 | 218, 219,
220 | fpwwe2lem3 9063 |
. . . . . . . . . . . 12
     
                                |
222 | 221 | anasss 653 |
. . . . . . . . . . 11
 
                                    |
223 | | cnvimass 5191 |
. . . . . . . . . . . . 13
  
       |
224 | 5, 17 | ssexd 4553 |
. . . . . . . . . . . . . . . . 17
   |
225 | | xpexg 6598 |
. . . . . . . . . . . . . . . . 17
 
     |
226 | 224, 224,
225 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
     |
227 | 226, 37 | ssexd 4553 |
. . . . . . . . . . . . . . 15
    |
228 | 227 | adantr 467 |
. . . . . . . . . . . . . 14
 
        |
229 | | dmexg 6729 |
. . . . . . . . . . . . . 14
     |
230 | 228, 229 | syl 17 |
. . . . . . . . . . . . 13
 
        |
231 | | ssexg 4552 |
. . . . . . . . . . . . 13
         
             |
232 | 223, 230,
231 | sylancr 670 |
. . . . . . . . . . . 12
 
               |
233 | | id 22 |
. . . . . . . . . . . . . . 15
                   |
234 | | olc 386 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
235 | | df-br 4406 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
  |
236 | | eluni2 4205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
    
  |
237 | 235, 236 | bitri 253 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
      |
238 | | df-br 4406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  
  
  |
239 | 85 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                  

    
    |
240 | 239 | ssbrd 4447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
                  

    
          |
241 | | brxp 4868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
    

   |
242 | 241 | simplbi 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
       |
243 | 240, 242 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                  

    
      |
244 | 20 | adantrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
 
           |
245 | 244 | ssbrd 4447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
 
         
       |
246 | 245 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
            
      |
247 | | brxp 4868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
    

   |
248 | 247 | simplbi 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
       |
249 | 246, 248 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
            
  |
250 | 249 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
            

   |
251 | | elequ1 1896 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
 
   |
252 | 251 | biimprd 227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
 
   |
253 | 252 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
          

   |
254 | 250, 253 | jaodan 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
                   |
255 | 254 | impr 625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
              
 
  |
256 | 255 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
                  

    
  |
257 | 243, 256 | jctird 547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                  

    
   
    |
258 | | brxp 4868 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    

   |
259 | 257, 258 | syl6ibr 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                  

    
          |
260 | 259 | ancld 556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                  

    
              |
261 | | simprr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                  

    
      |
262 | 261 | breqd 4416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                  

    
  
 
       |
263 | | brin 4455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
      
          |
264 | 262, 263 | syl6bb 265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                  

    
  
           |
265 | 260, 264 | sylibrd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                  

    
        |
266 | | simprr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                  

    
      |
267 | 266, 119 | syl6eqss 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                  

    
  |
268 | 267 | ssbrd 4447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                  

    
        |
269 | 128 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
              
 
 
     

       |
270 | 265, 268,
269 | mpjaodan 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
              
 
        |
271 | 238, 270 | syl5bir 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              
 
         |
272 | 271 | exp32 610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
                
       |
273 | 272 | expr 620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
                        |
274 | 273 | com24 90 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
                        |
275 | 274 | impr 625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
                        |
276 | 275 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
 
       
          |
277 | 276 | exlimdv 1781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
 
                   |
278 | 71, 277 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
 
     
   
      |
279 | 278 | rexlimdv 2879 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
 
          
     |
280 | 237, 279 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 
             |
281 | 234, 280 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . 21
     
 
         |
282 | 281 | ex 436 |
. . . . . . . . . . . . . . . . . . . 20
 
               |
283 | 282 | alrimiv 1775 |
. . . . . . . . . . . . . . . . . . 19
 
       
         |
284 | | vex 3050 |
. . . . . . . . . . . . . . . . . . . 20
 |
285 | | breq2 4409 |
. . . . . . . . . . . . . . . . . . . . 21
         |
286 | | breq2 4409 |
. . . . . . . . . . . . . . . . . . . . 21
   
     |
287 | 285, 286 | imbi12d 322 |
. . . . . . . . . . . . . . . . . . . 20
    
  
         |
288 | 284, 287 | ceqsalv 3077 |
. . . . . . . . . . . . . . . . . . 19
   
               |
289 | 283, 288 | sylib 200 |
. . . . . . . . . . . . . . . . . 18
 
       
     |
290 | 198 | ad2antrl 735 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
291 | 290, 201 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
 
    
   |
292 | 291 | ssbrd 4447 |
. . . . . . . . . . . . . . . . . 18
 
             |
293 | 289, 292 | impbid 194 |
. . . . . . . . . . . . . . . . 17
 
             |
294 | | vex 3050 |
. . . . . . . . . . . . . . . . . . 19
 |
295 | 294 | eliniseg 5200 |
. . . . . . . . . . . . . . . . . 18
    
    
     |
296 | 284, 295 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
        
    |
297 | 294 | eliniseg 5200 |
. . . . . . . . . . . . . . . . . 18
        
     |
298 | 284, 297 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
            |
299 | 293, 296,
298 | 3bitr4g 292 |
. . . . . . . . . . . . . . . 16
 
                        |
300 | 299 | eqrdv 2451 |
. . . . . . . . . . . . . . 15
 
                      |
301 | 233, 300 | sylan9eqr 2509 |
. . . . . . . . . . . . . 14
     
 
        
         |
302 | 301 | sqxpeqd 4863 |
. . . . . . . . . . . . . . . 16
     
 
        
                    |
303 | 302 | ineq2d 3636 |
. . . . . . . . . . . . . . 15
     
 
        
                          |
304 | | inss2 3655 |
. . . . . . . . . . . . . . . . . 18
                                    |
305 | | relxp 4945 |
. . . . . . . . . . . . . . . . . 18
                 |
306 | | relss 4925 |
. . . . . . . . . . . . . . . . . 18
                                                                           |
307 | 304, 305,
306 | mp2 9 |
. . . . . . . . . . . . . . . . 17
                    |
308 | | inss2 3655 |
. . . . . . . . . . . . . . . . . 18
                 
                 |
309 | | relss 4925 |
. . . . . . . . . . . . . . . . . 18
                                                                         |
310 | 308, 305,
309 | mp2 9 |
. . . . . . . . . . . . . . . . 17

                  |
311 | | vex 3050 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
312 | 311 | eliniseg 5200 |
. . . . . . . . . . . . . . . . . . . . . 22
        
     |
313 | 297, 312 | anbi12d 718 |
. . . . . . . . . . . . . . . . . . . . 21
         
       
         |
314 | 284, 313 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
                         |
315 | | orc 387 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
316 | 315, 280 | sylan2 477 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 
           |
317 | 316 | adantrl 723 |
. . . . . . . . . . . . . . . . . . . . 21
     
 
               |
318 | 291 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
     
 
          |
319 | 318 | ssbrd 4447 |
. . . . . . . . . . . . . . . . . . . . 21
     
 
         
     |
320 | 317, 319 | impbid 194 |
. . . . . . . . . . . . . . . . . . . 20
     
 
         
     |
321 | 314, 320 | sylan2b 478 |
. . . . . . . . . . . . . . . . . . 19
     
 
                
  
     |
322 | 321 | pm5.32da 647 |
. . . . . . . . . . . . . . . . . 18
 
                         
                       |
323 | | brinxp2 4899 |
. . . . . . . . . . . . . . . . . . 19
                                          |
324 | | df-br 4406 |
. . . . . . . . . . . . . . . . . . 19
                                              |
325 | | df-3an 988 |
. . . . . . . . . . . . . . . . . . 19
                  
                      |
326 | 323, 324,
325 | 3bitr3i 279 |
. . . . . . . . . . . . . . . . . 18
                                             |
327 | | brinxp2 4899 |
. . . . . . . . . . . . . . . . . . 19
                            
            |
328 | | df-br 4406 |
. . . . . . . . . . . . . . . . . . 19
                                            |
329 | | df-3an 988 |
. . . . . . . . . . . . . . . . . . 19
                                         |
330 | 327, 328,
329 | 3bitr3i 279 |
. . . . . . . . . . . . . . . . . 18
                     
                      |
331 | 322, 326,
330 | 3bitr4g 292 |
. . . . . . . . . . . . . . . . 17
 
                                                    |
332 | 307, 310,
331 | eqrelrdv 4934 |
. . . . . . . . . . . . . . . 16
 
                                            |
333 | 332 | adantr 467 |
. . . . . . . . . . . . . . 15
     
 
        
                                       |
334 | 303, 333 | eqtrd 2487 |
. . . . . . . . . . . . . 14
     
 
        
                         |
335 | 301, 334 | oveq12d 6313 |
. . . . . . . . . . . . 13
     
 
        
                                        |
336 | 335 | eqeq1d 2455 |
. . . . . . . . . . . 12
     
 
        
         
                                |
337 | 232, 336 | sbcied 3306 |
. . . . . . . . . . 11
 
                ![]. ].](_drbrack.gif)      
                                   |
338 | 222, 337 | mpbird 236 |
. . . . . . . . . 10
 
               ![]. ].](_drbrack.gif)      
     |
339 | 338 | exp32 610 |
. . . . . . . . 9
    
   
      ![]. ].](_drbrack.gif)              |
340 | 339 | exlimdv 1781 |
. . . . . . . 8
                ![]. ].](_drbrack.gif)      
       |
341 | 3, 340 | syl5bi 221 |
. . . . . . 7
  
   
      ![]. ].](_drbrack.gif)              |
342 | 341 | rexlimdv 2879 |
. . . . . 6
  
          ![]. ].](_drbrack.gif)      
      |
343 | 44, 342 | syl5bi 221 |
. . . . 5
            ![]. ].](_drbrack.gif)      
      |
344 | 343 | ralrimiv 2802 |
. . . 4
            ![]. ].](_drbrack.gif)      
     |
345 | 217, 344 | jca 535 |
. . 3
  

   
      ![]. ].](_drbrack.gif)             |
346 | 4, 5 | fpwwe2lem2 9062 |
. . 3
       
         
      ![]. ].](_drbrack.gif)               |
347 | 38, 345, 346 | mpbir2and 934 |
. 2
      |
348 | 21 | releldmi 5074 |
. 2
      |
349 | 347, 348 | syl 17 |
1
   |