Step | Hyp | Ref
| Expression |
1 | | simp2 1009 |
. . 3
 
   |
2 | | sucelon 6644 |
. . . . . 6

  |
3 | 1, 2 | sylib 200 |
. . . . 5
 
   |
4 | | simp1 1008 |
. . . . 5
 
   |
5 | | on0eln0 5478 |
. . . . . . 7
 
   |
6 | 5 | biimpar 488 |
. . . . . 6
     |
7 | 6 | 3adant2 1027 |
. . . . 5
 
   |
8 | | omword2 7275 |
. . . . 5
    

   |
9 | 3, 4, 7, 8 | syl21anc 1267 |
. . . 4
 
     |
10 | | sucidg 5501 |
. . . . 5
   |
11 | | ssel 3426 |
. . . . 5

        |
12 | 10, 11 | syl5 33 |
. . . 4

        |
13 | 9, 1, 12 | sylc 62 |
. . 3
 
     |
14 | | suceq 5488 |
. . . . . 6

  |
15 | 14 | oveq2d 6306 |
. . . . 5
       |
16 | 15 | eleq2d 2514 |
. . . 4
 
 

    |
17 | 16 | rspcev 3150 |
. . 3
 
   
    |
18 | 1, 13, 17 | syl2anc 667 |
. 2
 
      |
19 | | suceq 5488 |
. . . . . 6

  |
20 | 19 | oveq2d 6306 |
. . . . 5
       |
21 | 20 | eleq2d 2514 |
. . . 4
 
 

    |
22 | 21 | onminex 6634 |
. . 3
        
     |
23 | | vex 3048 |
. . . . . . . . . . . . . . 15
 |
24 | 23 | elon 5432 |
. . . . . . . . . . . . . 14

  |
25 | | ordzsl 6672 |
. . . . . . . . . . . . . 14
  
   |
26 | 24, 25 | bitri 253 |
. . . . . . . . . . . . 13

 
   |
27 | | noel 3735 |
. . . . . . . . . . . . . . . 16
 |
28 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . 18

      |
29 | | om0x 7221 |
. . . . . . . . . . . . . . . . . 18
   |
30 | 28, 29 | syl6eq 2501 |
. . . . . . . . . . . . . . . . 17

    |
31 | 30 | eleq2d 2514 |
. . . . . . . . . . . . . . . 16

  
   |
32 | 27, 31 | mtbiri 305 |
. . . . . . . . . . . . . . 15

    |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . 14
    
   

    |
34 | | simp3 1010 |
. . . . . . . . . . . . . . . . 17
    
 
   |
35 | | simp2 1009 |
. . . . . . . . . . . . . . . . . 18
    
 
 
    |
36 | | raleq 2987 |
. . . . . . . . . . . . . . . . . . 19
    
      |
37 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . 21
 |
38 | 37 | sucid 5502 |
. . . . . . . . . . . . . . . . . . . 20
 |
39 | | suceq 5488 |
. . . . . . . . . . . . . . . . . . . . . . . 24

  |
40 | 39 | oveq2d 6306 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
41 | 40 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . . . . 22
 
 

    |
42 | 41 | notbid 296 |
. . . . . . . . . . . . . . . . . . . . 21
 
 
     |
43 | 42 | rspcv 3146 |
. . . . . . . . . . . . . . . . . . . 20
    
     |
44 | 38, 43 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
 
 
    |
45 | 36, 44 | syl6bi 232 |
. . . . . . . . . . . . . . . . . 18
    
     |
46 | 34, 35, 45 | sylc 62 |
. . . . . . . . . . . . . . . . 17
    
 


   |
47 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . 20
       |
48 | 47 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . 19
         |
49 | 48 | notbid 296 |
. . . . . . . . . . . . . . . . . 18
   

    |
50 | 49 | biimpar 488 |
. . . . . . . . . . . . . . . . 17
    
    |
51 | 34, 46, 50 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
    
 


   |
52 | 51 | 3expia 1210 |
. . . . . . . . . . . . . . 15
    
   
     |
53 | 52 | rexlimdvw 2882 |
. . . . . . . . . . . . . 14
    
    

    |
54 | | ralnex 2834 |
. . . . . . . . . . . . . . . . . 18
 
 


   |
55 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
56 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
57 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
58 | | omlim 7235 |
. . . . . . . . . . . . . . . . . . . . . 22
  
    
    |
59 | 55, 56, 57, 58 | syl12anc 1266 |
. . . . . . . . . . . . . . . . . . . . 21
      
   |
60 | 59 | eleq2d 2514 |
. . . . . . . . . . . . . . . . . . . 20
   
 
      |
61 | | eliun 4283 |
. . . . . . . . . . . . . . . . . . . . 21
   


   |
62 | | limord 5482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
63 | 62 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
64 | 63, 24 | sylibr 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
65 | | simp3 1010 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
66 | | onelon 5448 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
67 | 64, 65, 66 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
68 | | suceloni 6640 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
  |
70 | | simp2 1009 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
71 | | sssucid 5500 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
72 | | omwordi 7272 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
 
  
    |
73 | 71, 72 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
74 | 67, 69, 70, 73 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
   |
75 | 74 | sseld 3431 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
       |
76 | 75 | 3expia 1210 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
77 | 76 | reximdvai 2859 |
. . . . . . . . . . . . . . . . . . . . 21
    
  

    |
78 | 61, 77 | syl5bi 221 |
. . . . . . . . . . . . . . . . . . . 20
   
   

    |
79 | 60, 78 | sylbid 219 |
. . . . . . . . . . . . . . . . . . 19
   
  

    |
80 | 79 | con3d 139 |
. . . . . . . . . . . . . . . . . 18
    
 
     |
81 | 54, 80 | syl5bi 221 |
. . . . . . . . . . . . . . . . 17
    
 

    |
82 | 81 | expimpd 608 |
. . . . . . . . . . . . . . . 16

 

  

    |
83 | 82 | com12 32 |
. . . . . . . . . . . . . . 15
  
         |
84 | 83 | 3ad2antl1 1170 |
. . . . . . . . . . . . . 14
    
         |
85 | 33, 53, 84 | 3jaod 1332 |
. . . . . . . . . . . . 13
    
    



    |
86 | 26, 85 | syl5bi 221 |
. . . . . . . . . . . 12
    
   
     |
87 | 86 | impr 625 |
. . . . . . . . . . 11
     
   
    |
88 | | simpl1 1011 |
. . . . . . . . . . . . 13
     
      |
89 | | simprr 766 |
. . . . . . . . . . . . 13
     
      |
90 | | omcl 7238 |
. . . . . . . . . . . . 13
 
     |
91 | 88, 89, 90 | syl2anc 667 |
. . . . . . . . . . . 12
     
        |
92 | | simpl2 1012 |
. . . . . . . . . . . 12
     
      |
93 | | ontri1 5457 |
. . . . . . . . . . . 12
   
         |
94 | 91, 92, 93 | syl2anc 667 |
. . . . . . . . . . 11
     
      
     |
95 | 87, 94 | mpbird 236 |
. . . . . . . . . 10
     
        |
96 | | oawordex 7258 |
. . . . . . . . . . 11
   
            |
97 | 91, 92, 96 | syl2anc 667 |
. . . . . . . . . 10
     
      
        |
98 | 95, 97 | mpbid 214 |
. . . . . . . . 9
     
           |
99 | 98 | 3adantr1 1167 |
. . . . . . . 8
    
  
 
 
       |
100 | | simp3r 1037 |
. . . . . . . . . . . . 13
    
  
 
       
      |
101 | | simp21 1041 |
. . . . . . . . . . . . . 14
    
  
 
       

   |
102 | | simp11 1038 |
. . . . . . . . . . . . . . 15
    
  
 
       
  |
103 | | simp23 1043 |
. . . . . . . . . . . . . . 15
    
  
 
       
  |
104 | | omsuc 7228 |
. . . . . . . . . . . . . . 15
 
         |
105 | 102, 103,
104 | syl2anc 667 |
. . . . . . . . . . . . . 14
    
  
 
       
        |
106 | 101, 105 | eleqtrd 2531 |
. . . . . . . . . . . . 13
    
  
 
       
      |
107 | 100, 106 | eqeltrd 2529 |
. . . . . . . . . . . 12
    
  
 
       
          |
108 | | simp3l 1036 |
. . . . . . . . . . . . 13
    
  
 
       
  |
109 | 102, 103,
90 | syl2anc 667 |
. . . . . . . . . . . . 13
    
  
 
       
    |
110 | | oaord 7248 |
. . . . . . . . . . . . 13
 
   
           |
111 | 108, 102,
109, 110 | syl3anc 1268 |
. . . . . . . . . . . 12
    
  
 
       

           |
112 | 107, 111 | mpbird 236 |
. . . . . . . . . . 11
    
  
 
       
  |
113 | 112, 100 | jca 535 |
. . . . . . . . . 10
    
  
 
       

       |
114 | 113 | 3expia 1210 |
. . . . . . . . 9
    
  
 
 
                |
115 | 114 | reximdv2 2858 |
. . . . . . . 8
    
  
 
 
 
    
       |
116 | 99, 115 | mpd 15 |
. . . . . . 7
    
  
 
 

      |
117 | 116 | expcom 437 |
. . . . . 6
           
       |
118 | 117 | 3expia 1210 |
. . . . 5
           

        |
119 | 118 | com13 83 |
. . . 4
 
     

   
        |
120 | 119 | reximdvai 2859 |
. . 3
 
  

      
        |
121 | 22, 120 | syl5 33 |
. 2
 
  
  
        |
122 | 18, 121 | mpd 15 |
1
 
         |