Step | Hyp | Ref
| Expression |
1 | | reldom 7575 |
. . . 4
 |
2 | 1 | brrelex2i 4876 |
. . 3

  |
3 | 2 | adantl 468 |
. 2
     |
4 | 1 | brrelexi 4875 |
. . . 4

  |
5 | | 0sdomg 7701 |
. . . . 5
 
   |
6 | | n0 3741 |
. . . . 5
    |
7 | 5, 6 | syl6bb 265 |
. . . 4
 
    |
8 | 4, 7 | syl 17 |
. . 3


    |
9 | 8 | biimpac 489 |
. 2
      |
10 | | brdomi 7580 |
. . 3

       |
11 | 10 | adantl 468 |
. 2
          |
12 | | difexg 4551 |
. . . . . . . . . 10
     |
13 | | snex 4641 |
. . . . . . . . . 10
   |
14 | | xpexg 6593 |
. . . . . . . . . 10
      
        |
15 | 12, 13, 14 | sylancl 668 |
. . . . . . . . 9
         |
16 | | vex 3048 |
. . . . . . . . . 10
 |
17 | 16 | cnvex 6740 |
. . . . . . . . 9
  |
18 | 15, 17 | jctil 540 |
. . . . . . . 8
  
         |
19 | | unexb 6591 |
. . . . . . . 8
  
      
 
         |
20 | 18, 19 | sylib 200 |
. . . . . . 7
  
         |
21 | | df-f1 5587 |
. . . . . . . . . . . . 13
    
         |
22 | 21 | simprbi 466 |
. . . . . . . . . . . 12
        |
23 | | vex 3048 |
. . . . . . . . . . . . . 14
 |
24 | 23 | fconst 5769 |
. . . . . . . . . . . . 13
               |
25 | | ffun 5731 |
. . . . . . . . . . . . 13
              
        |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . 12
       |
27 | 22, 26 | jctir 541 |
. . . . . . . . . . 11
     
  
       |
28 | | df-rn 4845 |
. . . . . . . . . . . . . 14
  |
29 | 28 | eqcomi 2460 |
. . . . . . . . . . . . 13

 |
30 | 23 | snnz 4090 |
. . . . . . . . . . . . . 14
   |
31 | | dmxp 5053 |
. . . . . . . . . . . . . 14
             |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
         |
33 | 29, 32 | ineq12i 3632 |
. . . . . . . . . . . 12
 
            |
34 | | disjdif 3839 |
. . . . . . . . . . . 12
 
   |
35 | 33, 34 | eqtri 2473 |
. . . . . . . . . . 11
 
        |
36 | | funun 5624 |
. . . . . . . . . . 11
              
                 |
37 | 27, 35, 36 | sylancl 668 |
. . . . . . . . . 10
                |
38 | 37 | adantl 468 |
. . . . . . . . 9
      
 
         |
39 | | dmun 5041 |
. . . . . . . . . . . 12
 
        
        |
40 | 28 | uneq1i 3584 |
. . . . . . . . . . . 12
         
        |
41 | 32 | uneq2i 3585 |
. . . . . . . . . . . 12
             |
42 | 39, 40, 41 | 3eqtr2i 2479 |
. . . . . . . . . . 11
 
            |
43 | | f1f 5779 |
. . . . . . . . . . . . 13
           |
44 | | frn 5735 |
. . . . . . . . . . . . 13
    
  |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . 12
    
  |
46 | | undif 3848 |
. . . . . . . . . . . 12


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

    |
48 | 42, 47 | syl5eq 2497 |
. . . . . . . . . 10
                |
49 | 48 | adantl 468 |
. . . . . . . . 9
      
 
         |
50 | | df-fn 5585 |
. . . . . . . . 9
  
      
  
                   |
51 | 38, 49, 50 | sylanbrc 670 |
. . . . . . . 8
          
       |
52 | | rnun 5244 |
. . . . . . . . 9
 
        
        |
53 | | dfdm4 5027 |
. . . . . . . . . . . 12
  |
54 | | f1dm 5783 |
. . . . . . . . . . . 12
    
  |
55 | 53, 54 | syl5eqr 2499 |
. . . . . . . . . . 11
     
  |
56 | 55 | uneq1d 3587 |
. . . . . . . . . 10
     
  
               |
57 | | xpeq1 4848 |
. . . . . . . . . . . . . . . . 17
         
     |
58 | | 0xp 4915 |
. . . . . . . . . . . . . . . . 17
     |
59 | 57, 58 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
           |
60 | 59 | rneqd 5062 |
. . . . . . . . . . . . . . 15
           |
61 | | rn0 5086 |
. . . . . . . . . . . . . . 15
 |
62 | 60, 61 | syl6eq 2501 |
. . . . . . . . . . . . . 14
           |
63 | | 0ss 3763 |
. . . . . . . . . . . . . 14
 |
64 | 62, 63 | syl6eqss 3482 |
. . . . . . . . . . . . 13
           |
65 | 64 | a1d 26 |
. . . . . . . . . . . 12
             |
66 | | rnxp 5267 |
. . . . . . . . . . . . . . 15
             |
67 | 66 | adantr 467 |
. . . . . . . . . . . . . 14
               |
68 | | snssi 4116 |
. . . . . . . . . . . . . . 15
  
  |
69 | 68 | adantl 468 |
. . . . . . . . . . . . . 14
      
  |
70 | 67, 69 | eqsstrd 3466 |
. . . . . . . . . . . . 13
             |
71 | 70 | ex 436 |
. . . . . . . . . . . 12
             |
72 | 65, 71 | pm2.61ine 2707 |
. . . . . . . . . . 11
         |
73 | | ssequn2 3607 |
. . . . . . . . . . 11
                 |
74 | 72, 73 | sylib 200 |
. . . . . . . . . 10
 
         |
75 | 56, 74 | sylan9eqr 2507 |
. . . . . . . . 9
        
         |
76 | 52, 75 | syl5eq 2497 |
. . . . . . . 8
      
 
         |
77 | | df-fo 5588 |
. . . . . . . 8
  
          
  
        
          |
78 | 51, 76, 77 | sylanbrc 670 |
. . . . . . 7
          
           |
79 | | foeq1 5789 |
. . . . . . . 8
    
    
    
   
            |
80 | 79 | spcegv 3135 |
. . . . . . 7
  
                     
       |
81 | 20, 78, 80 | syl2im 39 |
. . . . . 6
       
        |
82 | 81 | expdimp 439 |
. . . . 5
 
              |
83 | 82 | exlimdv 1779 |
. . . 4
 
       
       |
84 | 83 | ex 436 |
. . 3
        
        |
85 | 84 | exlimdv 1779 |
. 2
  
               |
86 | 3, 9, 11, 85 | syl3c 63 |
1
          |