Step | Hyp | Ref
| Expression |
1 | | pstmval.1 |
. . . . 5
~Met   |
2 | 1 | pstmval 28698 |
. . . 4
 PsMet 
pstoMet           
        |
3 | 2 | 3ad2ant1 1029 |
. . 3
  PsMet 
 pstoMet          

        |
4 | 3 | oveqd 6307 |
. 2
  PsMet 
    pstoMet        
       

           |
5 | | fvex 5875 |
. . . . . 6
~Met   |
6 | 1, 5 | eqeltri 2525 |
. . . . 5
 |
7 | 6 | ecelqsi 7419 |
. . . 4
       |
8 | 7 | 3ad2ant2 1030 |
. . 3
  PsMet 
       |
9 | 6 | ecelqsi 7419 |
. . . 4
       |
10 | 9 | 3ad2ant3 1031 |
. . 3
  PsMet 
       |
11 | | rexeq 2988 |
. . . . . 6
    

     

       |
12 | 11 | abbidv 2569 |
. . . . 5
     
       

       |
13 | 12 | unieqd 4208 |
. . . 4
      
                 |
14 | | rexeq 2988 |
. . . . . . 7
    
     
       |
15 | 14 | rexbidv 2901 |
. . . . . 6
          
           |
16 | 15 | abbidv 2569 |
. . . . 5
     

                 |
17 | 16 | unieqd 4208 |
. . . 4
      

       
  
       |
18 | | eqid 2451 |
. . . 4
         
               
       |
19 | | ecexg 7367 |
. . . . . . 7
    |
20 | 6, 19 | ax-mp 5 |
. . . . . 6
   |
21 | | ecexg 7367 |
. . . . . . 7
    |
22 | 6, 21 | ax-mp 5 |
. . . . . 6
   |
23 | 20, 22 | ab2rexex 6784 |
. . . . 5
           |
24 | 23 | uniex 6587 |
. . . 4
            |
25 | 13, 17, 18, 24 | ovmpt2 6432 |
. . 3
                      

        
             |
26 | 8, 10, 25 | syl2anc 667 |
. 2
  PsMet 
            

        
             |
27 | | simpr3 1016 |
. . . . . . . . . . 11
   PsMet 
           
      |
28 | | simpl1 1011 |
. . . . . . . . . . . 12
   PsMet 
           
PsMet    |
29 | | simpr1 1014 |
. . . . . . . . . . . . . 14
   PsMet 
           
   |
30 | | metidss 28694 |
. . . . . . . . . . . . . . . . . . . 20
 PsMet 
~Met 
    |
31 | 1, 30 | syl5eqss 3476 |
. . . . . . . . . . . . . . . . . . 19
 PsMet 
    |
32 | | xpss 4941 |
. . . . . . . . . . . . . . . . . . 19
  
  |
33 | 31, 32 | syl6ss 3444 |
. . . . . . . . . . . . . . . . . 18
 PsMet 
    |
34 | | df-rel 4841 |
. . . . . . . . . . . . . . . . . 18

    |
35 | 33, 34 | sylibr 216 |
. . . . . . . . . . . . . . . . 17
 PsMet 
 |
36 | 35 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . 16
  PsMet 
  |
37 | 36 | adantr 467 |
. . . . . . . . . . . . . . 15
   PsMet 
           
 |
38 | | relelec 7404 |
. . . . . . . . . . . . . . 15
       |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . 14
   PsMet 
           
      |
40 | 29, 39 | mpbid 214 |
. . . . . . . . . . . . 13
   PsMet 
           
  |
41 | 1 | breqi 4408 |
. . . . . . . . . . . . 13

 ~Met     |
42 | 40, 41 | sylib 200 |
. . . . . . . . . . . 12
   PsMet 
           
 ~Met     |
43 | | simpr2 1015 |
. . . . . . . . . . . . . 14
   PsMet 
           
   |
44 | | relelec 7404 |
. . . . . . . . . . . . . . 15
       |
45 | 37, 44 | syl 17 |
. . . . . . . . . . . . . 14
   PsMet 
           
      |
46 | 43, 45 | mpbid 214 |
. . . . . . . . . . . . 13
   PsMet 
           
  |
47 | 1 | breqi 4408 |
. . . . . . . . . . . . 13

 ~Met     |
48 | 46, 47 | sylib 200 |
. . . . . . . . . . . 12
   PsMet 
           
 ~Met     |
49 | | metideq 28696 |
. . . . . . . . . . . 12
  PsMet    ~Met  
 ~Met    
          |
50 | 28, 42, 48, 49 | syl12anc 1266 |
. . . . . . . . . . 11
   PsMet 
           
          |
51 | 27, 50 | eqtr4d 2488 |
. . . . . . . . . 10
   PsMet 
           
      |
52 | 51 | adantlr 721 |
. . . . . . . . 9
    PsMet 

             
            |
53 | 52 | 3anassrs 1232 |
. . . . . . . 8
      PsMet 
 
  
      
             |
54 | | oveq1 6297 |
. . . . . . . . . . . 12
           |
55 | 54 | eqeq2d 2461 |
. . . . . . . . . . 11
     
       |
56 | | oveq2 6298 |
. . . . . . . . . . . 12
           |
57 | 56 | eqeq2d 2461 |
. . . . . . . . . . 11
     
       |
58 | 55, 57 | cbvrex2v 3028 |
. . . . . . . . . 10
    
   
          |
59 | 58 | biimpi 198 |
. . . . . . . . 9
    
    
  
      |
60 | 59 | adantl 468 |
. . . . . . . 8
   PsMet 
 
  
      
 
      |
61 | 53, 60 | r19.29vva 2934 |
. . . . . . 7
   PsMet 
 
  
           |
62 | | simpl1 1011 |
. . . . . . . . . 10
   PsMet 
     
PsMet    |
63 | | simpl2 1012 |
. . . . . . . . . 10
   PsMet 
     
  |
64 | | psmet0 21324 |
. . . . . . . . . 10
  PsMet         |
65 | 62, 63, 64 | syl2anc 667 |
. . . . . . . . 9
   PsMet 
            |
66 | | relelec 7404 |
. . . . . . . . . . 11
       |
67 | 62, 35, 66 | 3syl 18 |
. . . . . . . . . 10
   PsMet 
        
   |
68 | 1 | a1i 11 |
. . . . . . . . . . 11
   PsMet 
     
~Met    |
69 | 68 | breqd 4413 |
. . . . . . . . . 10
   PsMet 
        ~Met      |
70 | | metidv 28695 |
. . . . . . . . . . 11
  PsMet  
 
  ~Met          |
71 | 62, 63, 63, 70 | syl12anc 1266 |
. . . . . . . . . 10
   PsMet 
        ~Met  
       |
72 | 67, 69, 71 | 3bitrd 283 |
. . . . . . . . 9
   PsMet 
        
       |
73 | 65, 72 | mpbird 236 |
. . . . . . . 8
   PsMet 
     
   |
74 | | simpl3 1013 |
. . . . . . . . . 10
   PsMet 
     
  |
75 | | psmet0 21324 |
. . . . . . . . . 10
  PsMet         |
76 | 62, 74, 75 | syl2anc 667 |
. . . . . . . . 9
   PsMet 
            |
77 | | relelec 7404 |
. . . . . . . . . . 11
       |
78 | 62, 35, 77 | 3syl 18 |
. . . . . . . . . 10
   PsMet 
        
   |
79 | 68 | breqd 4413 |
. . . . . . . . . 10
   PsMet 
        ~Met      |
80 | | metidv 28695 |
. . . . . . . . . . 11
  PsMet  
 
  ~Met          |
81 | 62, 74, 74, 80 | syl12anc 1266 |
. . . . . . . . . 10
   PsMet 
        ~Met  
       |
82 | 78, 79, 81 | 3bitrd 283 |
. . . . . . . . 9
   PsMet 
        
       |
83 | 76, 82 | mpbird 236 |
. . . . . . . 8
   PsMet 
     
   |
84 | | simpr 463 |
. . . . . . . 8
   PsMet 
            |
85 | | rspceov 6329 |
. . . . . . . 8
            
 
      |
86 | 73, 83, 84, 85 | syl3anc 1268 |
. . . . . . 7
   PsMet 
      
  
      |
87 | 61, 86 | impbida 843 |
. . . . . 6
  PsMet 
  
  
   
       |
88 | 87 | abbidv 2569 |
. . . . 5
  PsMet 
                   |
89 | | df-sn 3969 |
. . . . 5
             |
90 | 88, 89 | syl6eqr 2503 |
. . . 4
  PsMet 
                   |
91 | 90 | unieqd 4208 |
. . 3
  PsMet 
                     |
92 | | ovex 6318 |
. . . 4
     |
93 | 92 | unisn 4213 |
. . 3
            |
94 | 91, 93 | syl6eq 2501 |
. 2
  PsMet 
                  |
95 | 4, 26, 94 | 3eqtrd 2489 |
1
  PsMet 
    pstoMet           |