Step | Hyp | Ref
| Expression |
1 | | metidss 28687 |
. . . 4
 PsMet 
~Met 
    |
2 | | xpss 4940 |
. . . 4
  
  |
3 | 1, 2 | syl6ss 3443 |
. . 3
 PsMet 
~Met 
    |
4 | | df-rel 4840 |
. . 3
 ~Met  ~Met      |
5 | 3, 4 | sylibr 216 |
. 2
 PsMet 
~Met    |
6 | 1 | ssbrd 4443 |
. . . . 5
 PsMet 
  ~Met  
       |
7 | 6 | imp 431 |
. . . 4
  PsMet   ~Met          |
8 | | brxp 4864 |
. . . 4
    

   |
9 | 7, 8 | sylib 200 |
. . 3
  PsMet   ~Met    
   |
10 | | psmetsym 21319 |
. . . . . . . 8
  PsMet 
           |
11 | 10 | 3expb 1208 |
. . . . . . 7
  PsMet  
 
          |
12 | 11 | eqeq1d 2452 |
. . . . . 6
  PsMet  
 
    
       |
13 | | metidv 28688 |
. . . . . 6
  PsMet  
 
  ~Met          |
14 | | metidv 28688 |
. . . . . . 7
  PsMet  
 
  ~Met          |
15 | 14 | ancom2s 810 |
. . . . . 6
  PsMet  
 
  ~Met          |
16 | 12, 13, 15 | 3bitr4d 289 |
. . . . 5
  PsMet  
 
  ~Met    ~Met      |
17 | 16 | biimpd 211 |
. . . 4
  PsMet  
 
  ~Met  
 ~Met      |
18 | 17 | impancom 442 |
. . 3
  PsMet   ~Met     

 ~Met      |
19 | 9, 18 | mpd 15 |
. 2
  PsMet   ~Met     ~Met     |
20 | | simpl 459 |
. . . . . 6
  PsMet    ~Met    ~Met    
PsMet    |
21 | | simprr 765 |
. . . . . . . 8
  PsMet    ~Met    ~Met      ~Met     |
22 | 1 | ssbrd 4443 |
. . . . . . . . . 10
 PsMet 
  ~Met  
       |
23 | 22 | imp 431 |
. . . . . . . . 9
  PsMet   ~Met          |
24 | | brxp 4864 |
. . . . . . . . 9
    

   |
25 | 23, 24 | sylib 200 |
. . . . . . . 8
  PsMet   ~Met    
   |
26 | 21, 25 | syldan 473 |
. . . . . . 7
  PsMet    ~Met    ~Met     
   |
27 | 26 | simpld 461 |
. . . . . 6
  PsMet    ~Met    ~Met       |
28 | | simprl 763 |
. . . . . . . 8
  PsMet    ~Met    ~Met      ~Met     |
29 | 28, 9 | syldan 473 |
. . . . . . 7
  PsMet    ~Met    ~Met     
   |
30 | 29 | simpld 461 |
. . . . . 6
  PsMet    ~Met    ~Met    
  |
31 | 26 | simprd 465 |
. . . . . 6
  PsMet    ~Met    ~Met       |
32 | | psmettri2 21318 |
. . . . . 6
  PsMet  
 
                   |
33 | 20, 27, 30, 31, 32 | syl13anc 1269 |
. . . . 5
  PsMet    ~Met    ~Met        
               |
34 | 29, 11 | syldan 473 |
. . . . . . . 8
  PsMet    ~Met    ~Met               |
35 | 29, 13 | syldan 473 |
. . . . . . . . 9
  PsMet    ~Met    ~Met       ~Met  
       |
36 | 28, 35 | mpbid 214 |
. . . . . . . 8
  PsMet    ~Met    ~Met           |
37 | 34, 36 | eqtr3d 2486 |
. . . . . . 7
  PsMet    ~Met    ~Met           |
38 | | metidv 28688 |
. . . . . . . . 9
  PsMet  
 
  ~Met          |
39 | 26, 38 | syldan 473 |
. . . . . . . 8
  PsMet    ~Met    ~Met       ~Met  
       |
40 | 21, 39 | mpbid 214 |
. . . . . . 7
  PsMet    ~Met    ~Met           |
41 | 37, 40 | oveq12d 6306 |
. . . . . 6
  PsMet    ~Met    ~Met                         |
42 | | 0xr 9684 |
. . . . . . 7
 |
43 | | xaddid1 11529 |
. . . . . . 7

       |
44 | 42, 43 | ax-mp 5 |
. . . . . 6
      |
45 | 41, 44 | syl6eq 2500 |
. . . . 5
  PsMet    ~Met    ~Met                    |
46 | 33, 45 | breqtrd 4426 |
. . . 4
  PsMet    ~Met    ~Met        
  |
47 | | psmetge0 21321 |
. . . . 5
  PsMet 
       |
48 | 20, 30, 31, 47 | syl3anc 1267 |
. . . 4
  PsMet    ~Met    ~Met    
      |
49 | | psmetcl 21316 |
. . . . . 6
  PsMet 
       |
50 | 20, 30, 31, 49 | syl3anc 1267 |
. . . . 5
  PsMet    ~Met    ~Met           |
51 | | xrletri3 11448 |
. . . . 5
                
        |
52 | 50, 42, 51 | sylancl 667 |
. . . 4
  PsMet    ~Met    ~Met              
        |
53 | 46, 48, 52 | mpbir2and 932 |
. . 3
  PsMet    ~Met    ~Met           |
54 | | metidv 28688 |
. . . 4
  PsMet  
 
  ~Met          |
55 | 20, 30, 31, 54 | syl12anc 1265 |
. . 3
  PsMet    ~Met    ~Met       ~Met  
       |
56 | 53, 55 | mpbird 236 |
. 2
  PsMet    ~Met    ~Met      ~Met     |
57 | | psmet0 21317 |
. . . 4
  PsMet         |
58 | | metidv 28688 |
. . . . 5
  PsMet  
 
  ~Met          |
59 | 58 | anabsan2 830 |
. . . 4
  PsMet     ~Met  
       |
60 | 57, 59 | mpbird 236 |
. . 3
  PsMet    ~Met     |
61 | 1 | ssbrd 4443 |
. . . . . 6
 PsMet 
  ~Met  
       |
62 | 61 | imp 431 |
. . . . 5
  PsMet   ~Met          |
63 | | brxp 4864 |
. . . . 5
    

   |
64 | 62, 63 | sylib 200 |
. . . 4
  PsMet   ~Met    
   |
65 | 64 | simpld 461 |
. . 3
  PsMet   ~Met      |
66 | 60, 65 | impbida 842 |
. 2
 PsMet 

 ~Met      |
67 | 5, 19, 56, 66 | iserd 7386 |
1
 PsMet 
~Met    |