Step | Hyp | Ref
| Expression |
1 | | reldom 7593 |
. . . 4
 |
2 | 1 | brrelex2i 4881 |
. . 3

  |
3 | 2 | adantl 473 |
. 2
     |
4 | 1 | brrelexi 4880 |
. . . 4

  |
5 | | 0sdomg 7719 |
. . . . 5
 
   |
6 | | n0 3732 |
. . . . 5
    |
7 | 5, 6 | syl6bb 269 |
. . . 4
 
    |
8 | 4, 7 | syl 17 |
. . 3


    |
9 | 8 | biimpac 494 |
. 2
      |
10 | | brdomi 7598 |
. . 3

       |
11 | 10 | adantl 473 |
. 2
          |
12 | | difexg 4545 |
. . . . . . . . . 10
     |
13 | | snex 4641 |
. . . . . . . . . 10
   |
14 | | xpexg 6612 |
. . . . . . . . . 10
      
        |
15 | 12, 13, 14 | sylancl 675 |
. . . . . . . . 9
         |
16 | | vex 3034 |
. . . . . . . . . 10
 |
17 | 16 | cnvex 6759 |
. . . . . . . . 9
  |
18 | 15, 17 | jctil 546 |
. . . . . . . 8
  
         |
19 | | unexb 6610 |
. . . . . . . 8
  
      
 
         |
20 | 18, 19 | sylib 201 |
. . . . . . 7
  
         |
21 | | df-f1 5594 |
. . . . . . . . . . . . 13
    
         |
22 | 21 | simprbi 471 |
. . . . . . . . . . . 12
        |
23 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
24 | 23 | fconst 5782 |
. . . . . . . . . . . . 13
               |
25 | | ffun 5742 |
. . . . . . . . . . . . 13
              
        |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . 12
       |
27 | 22, 26 | jctir 547 |
. . . . . . . . . . 11
     
  
       |
28 | | df-rn 4850 |
. . . . . . . . . . . . . 14
  |
29 | 28 | eqcomi 2480 |
. . . . . . . . . . . . 13

 |
30 | 23 | snnz 4081 |
. . . . . . . . . . . . . 14
   |
31 | | dmxp 5059 |
. . . . . . . . . . . . . 14
             |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
         |
33 | 29, 32 | ineq12i 3623 |
. . . . . . . . . . . 12
 
            |
34 | | disjdif 3830 |
. . . . . . . . . . . 12
 
   |
35 | 33, 34 | eqtri 2493 |
. . . . . . . . . . 11
 
        |
36 | | funun 5631 |
. . . . . . . . . . 11
              
                 |
37 | 27, 35, 36 | sylancl 675 |
. . . . . . . . . 10
                |
38 | 37 | adantl 473 |
. . . . . . . . 9
      
 
         |
39 | | dmun 5047 |
. . . . . . . . . . . 12
 
        
        |
40 | 28 | uneq1i 3575 |
. . . . . . . . . . . 12
         
        |
41 | 32 | uneq2i 3576 |
. . . . . . . . . . . 12
             |
42 | 39, 40, 41 | 3eqtr2i 2499 |
. . . . . . . . . . 11
 
            |
43 | | f1f 5792 |
. . . . . . . . . . . . 13
           |
44 | | frn 5747 |
. . . . . . . . . . . . 13
    
  |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . 12
    
  |
46 | | undif 3839 |
. . . . . . . . . . . 12


     |
47 | 45, 46 | sylib 201 |
. . . . . . . . . . 11
     

    |
48 | 42, 47 | syl5eq 2517 |
. . . . . . . . . 10
                |
49 | 48 | adantl 473 |
. . . . . . . . 9
      
 
         |
50 | | df-fn 5592 |
. . . . . . . . 9
  
      
  
                   |
51 | 38, 49, 50 | sylanbrc 677 |
. . . . . . . 8
          
       |
52 | | rnun 5250 |
. . . . . . . . 9
 
        
        |
53 | | dfdm4 5032 |
. . . . . . . . . . . 12
  |
54 | | f1dm 5796 |
. . . . . . . . . . . 12
    
  |
55 | 53, 54 | syl5eqr 2519 |
. . . . . . . . . . 11
     
  |
56 | 55 | uneq1d 3578 |
. . . . . . . . . 10
     
  
               |
57 | | xpeq1 4853 |
. . . . . . . . . . . . . . . . 17
         
     |
58 | | 0xp 4920 |
. . . . . . . . . . . . . . . . 17
     |
59 | 57, 58 | syl6eq 2521 |
. . . . . . . . . . . . . . . 16
           |
60 | 59 | rneqd 5068 |
. . . . . . . . . . . . . . 15
           |
61 | | rn0 5092 |
. . . . . . . . . . . . . . 15
 |
62 | 60, 61 | syl6eq 2521 |
. . . . . . . . . . . . . 14
           |
63 | | 0ss 3766 |
. . . . . . . . . . . . . 14
 |
64 | 62, 63 | syl6eqss 3468 |
. . . . . . . . . . . . 13
           |
65 | 64 | a1d 25 |
. . . . . . . . . . . 12
             |
66 | | rnxp 5273 |
. . . . . . . . . . . . . . 15
             |
67 | 66 | adantr 472 |
. . . . . . . . . . . . . 14
               |
68 | | snssi 4107 |
. . . . . . . . . . . . . . 15
  
  |
69 | 68 | adantl 473 |
. . . . . . . . . . . . . 14
      
  |
70 | 67, 69 | eqsstrd 3452 |
. . . . . . . . . . . . 13
             |
71 | 70 | ex 441 |
. . . . . . . . . . . 12
             |
72 | 65, 71 | pm2.61ine 2726 |
. . . . . . . . . . 11
         |
73 | | ssequn2 3598 |
. . . . . . . . . . 11
                 |
74 | 72, 73 | sylib 201 |
. . . . . . . . . 10
 
         |
75 | 56, 74 | sylan9eqr 2527 |
. . . . . . . . 9
        
         |
76 | 52, 75 | syl5eq 2517 |
. . . . . . . 8
      
 
         |
77 | | df-fo 5595 |
. . . . . . . 8
  
          
  
        
          |
78 | 51, 76, 77 | sylanbrc 677 |
. . . . . . 7
          
           |
79 | | foeq1 5802 |
. . . . . . . 8
    
    
    
   
            |
80 | 79 | spcegv 3121 |
. . . . . . 7
  
                     
       |
81 | 20, 78, 80 | syl2im 38 |
. . . . . 6
       
        |
82 | 81 | expdimp 444 |
. . . . 5
 
              |
83 | 82 | exlimdv 1787 |
. . . 4
 
       
       |
84 | 83 | ex 441 |
. . 3
        
        |
85 | 84 | exlimdv 1787 |
. 2
  
               |
86 | 3, 9, 11, 85 | syl3c 62 |
1
          |