Step | Hyp | Ref
| Expression |
1 | | pssss 3528 |
. . . . . . . . . . . . . . . . 17
   |
2 | | ssralv 3493 |
. . . . . . . . . . . . . . . . 17
  
      
         |
3 | 1, 2 | syl 17 |
. . . . . . . . . . . . . . . 16
  
      
         |
4 | 3 | impcom 432 |
. . . . . . . . . . . . . . 15
          
        |
5 | 4 | adantrr 723 |
. . . . . . . . . . . . . 14
         
  
        |
6 | 5 | ad2ant2lr 754 |
. . . . . . . . . . . . 13
                  
        |
7 | | psseq2 3521 |
. . . . . . . . . . . . . . . . 17
 
   |
8 | 7 | anbi1d 711 |
. . . . . . . . . . . . . . . 16
   
     |
9 | | elequ2 1901 |
. . . . . . . . . . . . . . . 16
 
   |
10 | 8, 9 | imbi12d 322 |
. . . . . . . . . . . . . . 15
             |
11 | 10 | albidv 1767 |
. . . . . . . . . . . . . 14
       
         |
12 | 11 | rspccv 3147 |
. . . . . . . . . . . . 13
 
                |
13 | 6, 12 | syl 17 |
. . . . . . . . . . . 12
                            |
14 | 13 | imp 431 |
. . . . . . . . . . 11
                            |
15 | | eldifi 3555 |
. . . . . . . . . . . . . . . 16
     |
16 | | psseq2 3521 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
17 | 16 | anbi1d 711 |
. . . . . . . . . . . . . . . . . . 19
   
     |
18 | | elequ2 1901 |
. . . . . . . . . . . . . . . . . . 19
 
   |
19 | 17, 18 | imbi12d 322 |
. . . . . . . . . . . . . . . . . 18
             |
20 | 19 | albidv 1767 |
. . . . . . . . . . . . . . . . 17
       
         |
21 | 20 | rspcv 3146 |
. . . . . . . . . . . . . . . 16
  
               |
22 | 15, 21 | syl 17 |
. . . . . . . . . . . . . . 15
    
               |
23 | | psseq1 3520 |
. . . . . . . . . . . . . . . . . 18
 
   |
24 | | treq 4503 |
. . . . . . . . . . . . . . . . . 18
 
   |
25 | 23, 24 | anbi12d 717 |
. . . . . . . . . . . . . . . . 17
   
     |
26 | | elequ1 1894 |
. . . . . . . . . . . . . . . . 17
 
   |
27 | 25, 26 | imbi12d 322 |
. . . . . . . . . . . . . . . 16
             |
28 | 27 | cbvalv 2116 |
. . . . . . . . . . . . . . 15
      
        |
29 | 22, 28 | syl6ib 230 |
. . . . . . . . . . . . . 14
    
               |
30 | 29 | impcom 432 |
. . . . . . . . . . . . 13
                    |
31 | 30 | ad2ant2l 752 |
. . . . . . . . . . . 12
                          |
32 | 31 | adantr 467 |
. . . . . . . . . . 11
                            |
33 | | vex 3048 |
. . . . . . . . . . . . 13
 |
34 | | vex 3048 |
. . . . . . . . . . . . 13
 |
35 | 33, 34 | dfon2lem5 30433 |
. . . . . . . . . . . 12
     
             |
36 | | 3orrot 991 |
. . . . . . . . . . . . . 14
   
   |
37 | | 3orass 988 |
. . . . . . . . . . . . . 14
         |
38 | 36, 37 | bitri 253 |
. . . . . . . . . . . . 13
         |
39 | | eleq1a 2524 |
. . . . . . . . . . . . . . . . . 18
   
     |
40 | | elndif 3557 |
. . . . . . . . . . . . . . . . . 18

    |
41 | 39, 40 | nsyli 147 |
. . . . . . . . . . . . . . . . 17
   
   |
42 | 41 | imp 431 |
. . . . . . . . . . . . . . . 16
   
   |
43 | 42 | adantll 720 |
. . . . . . . . . . . . . . 15
        
  |
44 | 43 | adantll 720 |
. . . . . . . . . . . . . 14
                   
  |
45 | | orel1 384 |
. . . . . . . . . . . . . . 15
      
    |
46 | | trss 4506 |
. . . . . . . . . . . . . . . . . . . 20


   |
47 | | eldifn 3556 |
. . . . . . . . . . . . . . . . . . . . 21
  
  |
48 | | ssel 3426 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
49 | 48 | con3d 139 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
50 | 47, 49 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . 20
   
   |
51 | 46, 50 | syl9 73 |
. . . . . . . . . . . . . . . . . . 19

  

    |
52 | 51 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
 
    
    |
53 | 52 | imp31 434 |
. . . . . . . . . . . . . . . . 17
        
  |
54 | 53 | adantll 720 |
. . . . . . . . . . . . . . . 16
                   
  |
55 | | orel1 384 |
. . . . . . . . . . . . . . . 16
       |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . 15
                     

   |
57 | 45, 56 | syl9r 74 |
. . . . . . . . . . . . . 14
                    
    
    |
58 | 44, 57 | mpd 15 |
. . . . . . . . . . . . 13
                        
   |
59 | 38, 58 | syl5bi 221 |
. . . . . . . . . . . 12
                      
   |
60 | 35, 59 | syl5 33 |
. . . . . . . . . . 11
                                  
   |
61 | 14, 32, 60 | mp2and 685 |
. . . . . . . . . 10
                      |
62 | 61 | ex 436 |
. . . . . . . . 9
                  
   |
63 | 62 | ssrdv 3438 |
. . . . . . . 8
                    |
64 | | dfpss2 3518 |
. . . . . . . . 9

    |
65 | | psseq1 3520 |
. . . . . . . . . . . . . . . . . . 19
 
   |
66 | | treq 4503 |
. . . . . . . . . . . . . . . . . . 19
 
   |
67 | 65, 66 | anbi12d 717 |
. . . . . . . . . . . . . . . . . 18
   
     |
68 | | elequ1 1894 |
. . . . . . . . . . . . . . . . . 18
 
   |
69 | 67, 68 | imbi12d 322 |
. . . . . . . . . . . . . . . . 17
             |
70 | 69 | spv 2104 |
. . . . . . . . . . . . . . . 16
             |
71 | 70 | expd 438 |
. . . . . . . . . . . . . . 15
       
     |
72 | 71 | com23 81 |
. . . . . . . . . . . . . 14
       
     |
73 | 22, 72 | syl6 34 |
. . . . . . . . . . . . 13
    
      
      |
74 | 73 | com3l 84 |
. . . . . . . . . . . 12
 
      
   
     |
75 | 74 | adantld 469 |
. . . . . . . . . . 11
 
                  |
76 | 75 | adantl 468 |
. . . . . . . . . 10
  
            

     |
77 | 76 | imp32 435 |
. . . . . . . . 9
                  
   |
78 | 64, 77 | syl5bir 222 |
. . . . . . . 8
                    
   |
79 | 63, 78 | mpand 681 |
. . . . . . 7
                  
   |
80 | 79 | orrd 380 |
. . . . . 6
                      |
81 | 80 | anassrs 654 |
. . . . 5
                 

   |
82 | 81 | ralrimiva 2802 |
. . . 4
                      |
83 | | pssdif 3828 |
. . . . . . 7
     |
84 | | r19.2z 3858 |
. . . . . . . 8
    
      
       |
85 | 84 | ex 436 |
. . . . . . 7
  
 
              |
86 | 83, 85 | syl 17 |
. . . . . 6
  
              |
87 | 86 | ad2antrl 734 |
. . . . 5
                              |
88 | | eleq1 2517 |
. . . . . . . . . 10
 
   |
89 | 15, 88 | syl5ibr 225 |
. . . . . . . . 9
       |
90 | 89 | a1i 11 |
. . . . . . . 8
              
  
    |
91 | | trel 4504 |
. . . . . . . . . . 11

 
    |
92 | 91 | expd 438 |
. . . . . . . . . 10


     |
93 | 15, 92 | syl7 70 |
. . . . . . . . 9


       |
94 | 93 | ad2antrr 732 |
. . . . . . . 8
              
  
    |
95 | 90, 94 | jaod 382 |
. . . . . . 7
                        |
96 | 95 | com23 81 |
. . . . . 6
                
       |
97 | 96 | rexlimdv 2877 |
. . . . 5
                        |
98 | 87, 97 | syld 45 |
. . . 4
                        |
99 | 82, 98 | mpd 15 |
. . 3
                |
100 | 99 | ex 436 |
. 2
  
             |
101 | 100 | alrimiv 1773 |
1
  
               |