Proof of Theorem onfununi
Step | Hyp | Ref
| Expression |
1 | | ssorduni 6631 |
. . . . . . . . . 10

   |
2 | 1 | ad2antrr 740 |
. . . . . . . . 9
    

   |
3 | | nelneq 2573 |
. . . . . . . . . . . . . . . 16
   
   |
4 | | elssuni 4219 |
. . . . . . . . . . . . . . . . . . . 20
    |
5 | 4 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
 
    |
6 | | ssel 3412 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
7 | | eloni 5440 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
8 | 6, 7 | syl6 33 |
. . . . . . . . . . . . . . . . . . . . . 22

    |
9 | 8 | imp 436 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
10 | | ordsseleq 5459 |
. . . . . . . . . . . . . . . . . . . . 21
    

       |
11 | 9, 1, 10 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . 20
              |
12 | 11 | anabss1 830 |
. . . . . . . . . . . . . . . . . . 19
 
 

       |
13 | 5, 12 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
 
  
    |
14 | 13 | ord 384 |
. . . . . . . . . . . . . . . . 17
 
 
     |
15 | 14 | con1d 129 |
. . . . . . . . . . . . . . . 16
 
 
     |
16 | 3, 15 | syl5 32 |
. . . . . . . . . . . . . . 15
 
         |
17 | 16 | exp4b 618 |
. . . . . . . . . . . . . 14

   
      |
18 | 17 | pm2.43d 49 |
. . . . . . . . . . . . 13

        |
19 | 18 | com23 80 |
. . . . . . . . . . . 12

        |
20 | 19 | imp 436 |
. . . . . . . . . . 11
 
  
    |
21 | 20 | ssrdv 3424 |
. . . . . . . . . 10
 
     |
22 | | ssn0 3770 |
. . . . . . . . . 10
 
     |
23 | 21, 22 | sylan 479 |
. . . . . . . . 9
    

   |
24 | 21 | unissd 4214 |
. . . . . . . . . . 11
 
       |
25 | | orduniss 5524 |
. . . . . . . . . . . . 13
 
     |
26 | 1, 25 | syl 17 |
. . . . . . . . . . . 12

     |
27 | 26 | adantr 472 |
. . . . . . . . . . 11
 
       |
28 | 24, 27 | eqssd 3435 |
. . . . . . . . . 10
 
       |
29 | 28 | adantr 472 |
. . . . . . . . 9
    

     |
30 | | df-lim 5435 |
. . . . . . . . 9
 
         |
31 | 2, 23, 29, 30 | syl3anbrc 1214 |
. . . . . . . 8
    

   |
32 | 31 | an32s 821 |
. . . . . . 7
     
   |
33 | 32 | 3adantl1 1186 |
. . . . . 6
  
  
   |
34 | | ssonuni 6632 |
. . . . . . . . . 10
      |
35 | | limeq 5442 |
. . . . . . . . . . . 12
  
    |
36 | | fveq2 5879 |
. . . . . . . . . . . . 13
             |
37 | | iuneq1 4283 |
. . . . . . . . . . . . 13
  
             |
38 | 36, 37 | eqeq12d 2486 |
. . . . . . . . . . . 12
       
                   |
39 | 35, 38 | imbi12d 327 |
. . . . . . . . . . 11
        
    
 
                |
40 | | onfununi.1 |
. . . . . . . . . . 11

    
      |
41 | 39, 40 | vtoclg 3093 |
. . . . . . . . . 10
 
       
         |
42 | 34, 41 | syl6 33 |
. . . . . . . . 9
                    |
43 | 42 | imp 436 |
. . . . . . . 8
   
      
         |
44 | 43 | 3adant3 1050 |
. . . . . . 7
                    |
45 | 44 | adantr 472 |
. . . . . 6
  
          
         |
46 | 33, 45 | mpd 15 |
. . . . 5
  
        
        |
47 | | eluni2 4194 |
. . . . . . . . . . . 12
 

  |
48 | | ssel 3412 |
. . . . . . . . . . . . . . . . . 18

    |
49 | 48 | anim1d 574 |
. . . . . . . . . . . . . . . . 17

 
      |
50 | | onelon 5455 |
. . . . . . . . . . . . . . . . 17
 
   |
51 | 49, 50 | syl6 33 |
. . . . . . . . . . . . . . . 16

 
    |
52 | 48 | adantrd 475 |
. . . . . . . . . . . . . . . 16

 
    |
53 | | eloni 5440 |
. . . . . . . . . . . . . . . . . 18
   |
54 | 48, 53 | syl6 33 |
. . . . . . . . . . . . . . . . 17

    |
55 | | ordelss 5446 |
. . . . . . . . . . . . . . . . . 18
     |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . 17

      |
57 | 54, 56 | syland 489 |
. . . . . . . . . . . . . . . 16

 

   |
58 | 51, 52, 57 | 3jcad 1211 |
. . . . . . . . . . . . . . 15

 
      |
59 | | onfununi.2 |
. . . . . . . . . . . . . . 15
 
           |
60 | 58, 59 | syl6 33 |
. . . . . . . . . . . . . 14

 
    
       |
61 | 60 | expd 443 |
. . . . . . . . . . . . 13

     
        |
62 | 61 | reximdvai 2856 |
. . . . . . . . . . . 12

  
           |
63 | 47, 62 | syl5bi 225 |
. . . . . . . . . . 11

  
           |
64 | | ssiun 4311 |
. . . . . . . . . . 11
                     |
65 | 63, 64 | syl6 33 |
. . . . . . . . . 10

     
        |
66 | 65 | ralrimiv 2808 |
. . . . . . . . 9

              |
67 | | iunss 4310 |
. . . . . . . . 9
 
           
     
       |
68 | 66, 67 | sylibr 217 |
. . . . . . . 8

              |
69 | | fveq2 5879 |
. . . . . . . . 9
           |
70 | 69 | cbviunv 4308 |
. . . . . . . 8

    
     |
71 | 68, 70 | syl6sseq 3464 |
. . . . . . 7

              |
72 | 71 | 3ad2ant2 1052 |
. . . . . 6
                 |
73 | 72 | adantr 472 |
. . . . 5
  
          
      |
74 | 46, 73 | eqsstrd 3452 |
. . . 4
  
        
      |
75 | 74 | ex 441 |
. . 3
          
       |
76 | | fveq2 5879 |
. . . 4
             |
77 | 76 | ssiun2s 4313 |
. . 3
 
    
       |
78 | 75, 77 | pm2.61d2 165 |
. 2
               |
79 | 34 | imp 436 |
. . . . . 6
   
  |
80 | 79 | 3adant3 1050 |
. . . . 5
      |
81 | 6 | 3ad2ant2 1052 |
. . . . . 6
   
   |
82 | 4 | a1i 11 |
. . . . . 6
        |
83 | 81, 82 | jcad 542 |
. . . . 5
    
     |
84 | | sseq2 3440 |
. . . . . . . 8
       |
85 | 84 | anbi2d 718 |
. . . . . . 7
    
      |
86 | 36 | sseq2d 3446 |
. . . . . . 7
                       |
87 | 85, 86 | imbi12d 327 |
. . . . . 6
              
                 |
88 | 59 | 3com12 1235 |
. . . . . . 7
 
           |
89 | 88 | 3expib 1234 |
. . . . . 6
  
    
       |
90 | 87, 89 | vtoclga 3099 |
. . . . 5
 
 
              |
91 | 80, 83, 90 | sylsyld 57 |
. . . 4
       
        |
92 | 91 | ralrimiv 2808 |
. . 3
   
           |
93 | | iunss 4310 |
. . 3
 
        

           |
94 | 92, 93 | sylibr 217 |
. 2
   
           |
95 | 78, 94 | eqssd 3435 |
1
               |