Step | Hyp | Ref
| Expression |
1 | | pssss 3540 |
. . . 4
   |
2 | | ssexg 4563 |
. . . 4
 
   |
3 | 1, 2 | sylan 478 |
. . 3
 
   |
4 | 3 | ancoms 459 |
. 2
  
  |
5 | | psseq2 3533 |
. . . . . . . 8


   |
6 | | rexeq 3000 |
. . . . . . . 8

 
    |
7 | 5, 6 | imbi12d 326 |
. . . . . . 7

 
 
      |
8 | 7 | albidv 1778 |
. . . . . 6

              |
9 | | psseq2 3533 |
. . . . . . . 8
 
   |
10 | | rexeq 3000 |
. . . . . . . 8
  

   |
11 | 9, 10 | imbi12d 326 |
. . . . . . 7
           |
12 | 11 | albidv 1778 |
. . . . . 6
               |
13 | | psseq2 3533 |
. . . . . . . 8
 
   |
14 | | rexeq 3000 |
. . . . . . . 8
    
   |
15 | 13, 14 | imbi12d 326 |
. . . . . . 7
       
    |
16 | 15 | albidv 1778 |
. . . . . 6
    
 
    
    |
17 | | psseq2 3533 |
. . . . . . . 8
 
   |
18 | | rexeq 3000 |
. . . . . . . 8
  

   |
19 | 17, 18 | imbi12d 326 |
. . . . . . 7
           |
20 | 19 | albidv 1778 |
. . . . . 6
               |
21 | | npss0 3815 |
. . . . . . . 8
 |
22 | 21 | pm2.21i 136 |
. . . . . . 7

   |
23 | 22 | ax-gen 1680 |
. . . . . 6
      |
24 | | nfv 1772 |
. . . . . . 7

 |
25 | | nfa1 1990 |
. . . . . . 7
        |
26 | | elequ1 1905 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
27 | 26 | biimpcd 232 |
. . . . . . . . . . . . . . . . . . . . 21
     |
28 | 27 | con3d 140 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
29 | 28 | adantl 472 |
. . . . . . . . . . . . . . . . . . 19
 
 
   |
30 | | pssss 3540 |
. . . . . . . . . . . . . . . . . . . . . 22

  |
31 | 30 | sseld 3443 |
. . . . . . . . . . . . . . . . . . . . 21

    |
32 | | elsuci 5508 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
33 | 32 | ord 383 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
34 | 33 | con1d 129 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
35 | 31, 34 | syl6 34 |
. . . . . . . . . . . . . . . . . . . 20

 
    |
36 | 35 | imp 435 |
. . . . . . . . . . . . . . . . . . 19
 
 
   |
37 | 29, 36 | syld 45 |
. . . . . . . . . . . . . . . . . 18
 
 
   |
38 | 37 | impancom 446 |
. . . . . . . . . . . . . . . . 17
 


   |
39 | 38 | ssrdv 3450 |
. . . . . . . . . . . . . . . 16
 

  |
40 | 39 | anim1i 576 |
. . . . . . . . . . . . . . 15
   
     |
41 | | dfpss2 3530 |
. . . . . . . . . . . . . . 15

    |
42 | 40, 41 | sylibr 217 |
. . . . . . . . . . . . . 14
   
   |
43 | | elelsuc 5514 |
. . . . . . . . . . . . . . . 16
   |
44 | 43 | anim1i 576 |
. . . . . . . . . . . . . . 15
       |
45 | 44 | reximi2 2866 |
. . . . . . . . . . . . . 14
      |
46 | 42, 45 | imim12i 59 |
. . . . . . . . . . . . 13
 
    

 

   |
47 | 46 | exp4c 617 |
. . . . . . . . . . . 12
 
   

 
     |
48 | 47 | sps 1954 |
. . . . . . . . . . 11
      
 
       |
49 | 48 | adantl 472 |
. . . . . . . . . 10
       
 

       |
50 | 49 | com4t 88 |
. . . . . . . . 9
 
       
        |
51 | | anidm 654 |
. . . . . . . . . . . . . 14
 

  |
52 | | ssdif 3580 |
. . . . . . . . . . . . . . . . 17

    
     |
53 | | nnord 6727 |
. . . . . . . . . . . . . . . . . . 19
   |
54 | | orddif 5535 |
. . . . . . . . . . . . . . . . . . 19

      |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
56 | 55 | sseq2d 3472 |
. . . . . . . . . . . . . . . . 17
                 |
57 | 52, 56 | syl5ibr 229 |
. . . . . . . . . . . . . . . 16
 
       |
58 | 30, 57 | syl5 33 |
. . . . . . . . . . . . . . 15
 
       |
59 | | pssnel 3844 |
. . . . . . . . . . . . . . . 16

  
   |
60 | | eleq2 2529 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
   |
61 | | eldifi 3567 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
62 | 60, 61 | syl6bir 237 |
. . . . . . . . . . . . . . . . . . . . . 22
     
   |
63 | 62 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
   

   |
64 | | eleq1a 2535 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
65 | 33, 64 | sylan9r 668 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 
   |
66 | 65 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . 21
  
 
   

   |
67 | 63, 66 | pm2.61d 163 |
. . . . . . . . . . . . . . . . . . . 20
  
 
   
  |
68 | 67 | ex 440 |
. . . . . . . . . . . . . . . . . . 19
 
         |
69 | 68 | con3d 140 |
. . . . . . . . . . . . . . . . . 18
 
 

      |
70 | 69 | expimpd 612 |
. . . . . . . . . . . . . . . . 17
    
      |
71 | 70 | exlimdv 1790 |
. . . . . . . . . . . . . . . 16
    
        |
72 | 59, 71 | syl5 33 |
. . . . . . . . . . . . . . 15
 
       |
73 | 58, 72 | im2anan9r 852 |
. . . . . . . . . . . . . 14
 
  
      
       |
74 | 51, 73 | syl5bir 226 |
. . . . . . . . . . . . 13
 
       
       |
75 | | dfpss2 3530 |
. . . . . . . . . . . . 13
                 |
76 | 74, 75 | syl6ibr 235 |
. . . . . . . . . . . 12
 
         |
77 | | psseq1 3532 |
. . . . . . . . . . . . . . 15
 
   |
78 | | breq1 4419 |
. . . . . . . . . . . . . . . 16
 
   |
79 | 78 | rexbidv 2913 |
. . . . . . . . . . . . . . 15
  

   |
80 | 77, 79 | imbi12d 326 |
. . . . . . . . . . . . . 14
           |
81 | 80 | cbvalv 2127 |
. . . . . . . . . . . . 13
             |
82 | | vex 3060 |
. . . . . . . . . . . . . . 15
 |
83 | | difss 3572 |
. . . . . . . . . . . . . . 15
   
 |
84 | 82, 83 | ssexi 4562 |
. . . . . . . . . . . . . 14
     |
85 | | psseq1 3532 |
. . . . . . . . . . . . . . 15
             |
86 | | breq1 4419 |
. . . . . . . . . . . . . . . 16
             |
87 | 86 | rexbidv 2913 |
. . . . . . . . . . . . . . 15
      
        |
88 | 85, 87 | imbi12d 326 |
. . . . . . . . . . . . . 14
       

 
            |
89 | 84, 88 | spcv 3152 |
. . . . . . . . . . . . 13
          
        |
90 | 81, 89 | sylbi 200 |
. . . . . . . . . . . 12
          
        |
91 | 76, 90 | sylan9 667 |
. . . . . . . . . . 11
  
   
   

       |
92 | | ordsucelsuc 6676 |
. . . . . . . . . . . . . . . . . . . 20


   |
93 | 92 | biimpd 212 |
. . . . . . . . . . . . . . . . . . 19


   |
94 | 53, 93 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     |
95 | 94 | adantl 472 |
. . . . . . . . . . . . . . . . 17
 
 
   |
96 | 95 | adantrd 474 |
. . . . . . . . . . . . . . . 16
 
       
   |
97 | | elnn 6729 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
98 | | snex 4655 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      |
99 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
100 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
101 | 99, 100 | f1osn 5875 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              |
102 | | f1oen3g 7611 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                           |
103 | 98, 101, 102 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
104 | 103 | jctr 549 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
105 | | nnord 6727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
106 | | orddisj 5480 |
. . . . . . . . . . . . . . . . . . . . . . . 24

      |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
108 | | incom 3637 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
             |
109 | | disjdif 3851 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
     |
110 | 108, 109 | eqtr3i 2486 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
111 | 107, 110 | jctil 544 |
. . . . . . . . . . . . . . . . . . . . . 22
          
      |
112 | | unen 7678 |
. . . . . . . . . . . . . . . . . . . . . 22
                                         |
113 | 104, 111,
112 | syl2an 484 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
114 | | difsnid 4131 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
115 | 114 | eqcomd 2468 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
116 | | df-suc 5448 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
117 | 116 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22

      |
118 | 115, 117 | breq12d 4429 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
      
      |
119 | 113, 118 | syl5ibr 229 |
. . . . . . . . . . . . . . . . . . . 20
           |
120 | 97, 119 | sylan2i 665 |
. . . . . . . . . . . . . . . . . . 19
       
 
   |
121 | 120 | exp4d 618 |
. . . . . . . . . . . . . . . . . 18
      

     |
122 | 121 | com24 90 |
. . . . . . . . . . . . . . . . 17
             |
123 | 122 | imp4b 599 |
. . . . . . . . . . . . . . . 16
 
           |
124 | 96, 123 | jcad 540 |
. . . . . . . . . . . . . . 15
 
             |
125 | | breq2 4420 |
. . . . . . . . . . . . . . . 16
 
   |
126 | 125 | rspcev 3162 |
. . . . . . . . . . . . . . 15
       |
127 | 124, 126 | syl6 34 |
. . . . . . . . . . . . . 14
 
         
   |
128 | 127 | exlimdv 1790 |
. . . . . . . . . . . . 13
 
     
   
     |
129 | | df-rex 2755 |
. . . . . . . . . . . . 13
                |
130 | | breq2 4420 |
. . . . . . . . . . . . . 14
 
   |
131 | 130 | cbvrexv 3032 |
. . . . . . . . . . . . 13
  
    |
132 | 128, 129,
131 | 3imtr4g 278 |
. . . . . . . . . . . 12
 
            |
133 | 132 | adantr 471 |
. . . . . . . . . . 11
  
   
    
         |
134 | 91, 133 | syld 45 |
. . . . . . . . . 10
  
   
   
     |
135 | 134 | expl 628 |
. . . . . . . . 9
      
    
    |
136 | 82 | eqelsuc 5523 |
. . . . . . . . . . 11
   |
137 | 82 | enref 7628 |
. . . . . . . . . . 11
 |
138 | | breq2 4420 |
. . . . . . . . . . . 12
 
   |
139 | 138 | rspcev 3162 |
. . . . . . . . . . 11
 
  
  |
140 | 136, 137,
139 | sylancl 673 |
. . . . . . . . . 10
     |
141 | 140 | 2a1d 27 |
. . . . . . . . 9
      
    
    |
142 | 50, 135, 141 | pm2.61ii 170 |
. . . . . . . 8
       
      |
143 | 142 | ex 440 |
. . . . . . 7
       
      |
144 | 24, 25, 143 | alrimd 1970 |
. . . . . 6
         
 
    |
145 | 8, 12, 16, 20, 23, 144 | finds 6746 |
. . . . 5
        |
146 | | psseq1 3532 |
. . . . . . 7
 
   |
147 | | breq1 4419 |
. . . . . . . 8
 
   |
148 | 147 | rexbidv 2913 |
. . . . . . 7
  

   |
149 | 146, 148 | imbi12d 326 |
. . . . . 6
    


    |
150 | 149 | spcgv 3146 |
. . . . 5
             |
151 | 145, 150 | syl5 33 |
. . . 4
 

     |
152 | 151 | com3l 84 |
. . 3
  
     |
153 | 152 | imp 435 |
. 2
        |
154 | 4, 153 | mpd 15 |
1
   
  |