Step | Hyp | Ref
| Expression |
1 | | relres 5132 |
. . 3
  |
2 | 1 | a1i 11 |
. 2
  PsMet  
   |
3 | | vex 3048 |
. . . . . . . . . . . . . . 15
 |
4 | 3 | brres 5111 |
. . . . . . . . . . . . . 14
        |
5 | | df-br 4403 |
. . . . . . . . . . . . . 14
          |
6 | 3 | ideq 4987 |
. . . . . . . . . . . . . . 15

  |
7 | 6 | anbi1i 701 |
. . . . . . . . . . . . . 14
 
 
   |
8 | 4, 5, 7 | 3bitr3i 279 |
. . . . . . . . . . . . 13
   
     |
9 | 8 | biimpi 198 |
. . . . . . . . . . . 12
   
     |
10 | 9 | ad2antlr 733 |
. . . . . . . . . . 11
    PsMet 

  
       |
11 | 10 | simpld 461 |
. . . . . . . . . 10
    PsMet 

  
     |
12 | | df-ov 6293 |
. . . . . . . . . . 11
            |
13 | | opeq2 4167 |
. . . . . . . . . . . 12
   
     |
14 | 13 | fveq2d 5869 |
. . . . . . . . . . 11
                 |
15 | 12, 14 | syl5eq 2497 |
. . . . . . . . . 10
              |
16 | 11, 15 | syl 17 |
. . . . . . . . 9
    PsMet 

  
                |
17 | | simplll 768 |
. . . . . . . . . 10
    PsMet 

  
   PsMet    |
18 | 10 | simprd 465 |
. . . . . . . . . 10
    PsMet 

  
     |
19 | | psmet0 21324 |
. . . . . . . . . 10
  PsMet         |
20 | 17, 18, 19 | syl2anc 667 |
. . . . . . . . 9
    PsMet 

  
         |
21 | 16, 20 | eqtr3d 2487 |
. . . . . . . 8
    PsMet 

  
            |
22 | | 0xr 9687 |
. . . . . . . . . . 11
 |
23 | 22 | a1i 11 |
. . . . . . . . . 10

  |
24 | | rpxr 11309 |
. . . . . . . . . 10

  |
25 | | rpgt0 11313 |
. . . . . . . . . 10

  |
26 | | lbico1 11689 |
. . . . . . . . . 10
         |
27 | 23, 24, 25, 26 | syl3anc 1268 |
. . . . . . . . 9

      |
28 | 27 | adantl 468 |
. . . . . . . 8
    PsMet 

  
         |
29 | 21, 28 | eqeltrd 2529 |
. . . . . . 7
    PsMet 

  
                |
30 | | psmetf 21322 |
. . . . . . . . . 10
 PsMet 
        |
31 | | ffun 5731 |
. . . . . . . . . 10
         |
32 | 30, 31 | syl 17 |
. . . . . . . . 9
 PsMet 
  |
33 | 32 | ad3antrrr 736 |
. . . . . . . 8
    PsMet 

  
  
  |
34 | 11, 18 | eqeltrrd 2530 |
. . . . . . . . . 10
    PsMet 

  
     |
35 | | opelxpi 4866 |
. . . . . . . . . 10
 
        |
36 | 18, 34, 35 | syl2anc 667 |
. . . . . . . . 9
    PsMet 

  
          |
37 | | fdm 5733 |
. . . . . . . . . . 11
           |
38 | 30, 37 | syl 17 |
. . . . . . . . . 10
 PsMet 
    |
39 | 38 | ad3antrrr 736 |
. . . . . . . . 9
    PsMet 

  
  

   |
40 | 36, 39 | eleqtrrd 2532 |
. . . . . . . 8
    PsMet 

  
        |
41 | | fvimacnv 5997 |
. . . . . . . 8
     
                           |
42 | 33, 40, 41 | syl2anc 667 |
. . . . . . 7
    PsMet 

  
          
                   |
43 | 29, 42 | mpbid 214 |
. . . . . 6
    PsMet 

  
                 |
44 | 43 | adantr 467 |
. . . . 5
     PsMet 
   
 
                         |
45 | | simpr 463 |
. . . . 5
     PsMet 
   
 
          
           |
46 | 44, 45 | eleqtrrd 2532 |
. . . 4
     PsMet 
   
 
                |
47 | | simplr 762 |
. . . . 5
   PsMet     
 
  |
48 | | metust.1 |
. . . . . . 7
            |
49 | 48 | metustel 21565 |
. . . . . 6
 PsMet 

             |
50 | 49 | ad2antrr 732 |
. . . . 5
   PsMet     
 

             |
51 | 47, 50 | mpbid 214 |
. . . 4
   PsMet     
 
            |
52 | 46, 51 | r19.29a 2932 |
. . 3
   PsMet     
 
  
  |
53 | 52 | ex 436 |
. 2
  PsMet      
       |
54 | 2, 53 | relssdv 4927 |
1
  PsMet      |