Step | Hyp | Ref
| Expression |
1 | | xmetxp.p |
. . 3
                                       |
2 | | xmetxp.1 |
. . 3
        |
3 | | xmetxp.2 |
. . 3
        |
4 | | xmettx.j |
. . 3
     |
5 | | xmettx.k |
. . 3
     |
6 | | xmettx.l |
. . 3
     |
7 | 1, 2, 3, 4, 5, 6 | xmettxlem 13979 |
. 2

    |
8 | | eqid 2177 |
. . . . . . . . . . . 12
           |
9 | 8 | elrnmpog 5986 |
. . . . . . . . . . 11
        
     |
10 | 9 | elv 2741 |
. . . . . . . . . 10
      

    |
11 | 10 | biimpi 120 |
. . . . . . . . 9
       
    |
12 | 11 | adantl 277 |
. . . . . . . 8
 
 
    

    |
13 | | xpeq1 4640 |
. . . . . . . . . 10
       |
14 | 13 | eqeq2d 2189 |
. . . . . . . . 9
   

    |
15 | | xpeq2 4641 |
. . . . . . . . . 10
       |
16 | 15 | eqeq2d 2189 |
. . . . . . . . 9
   

    |
17 | 14, 16 | cbvrex2v 2717 |
. . . . . . . 8
  
 



   |
18 | 12, 17 | sylib 122 |
. . . . . . 7
 
 
    

    |
19 | | simpr 110 |
. . . . . . . . . 10
   
        
  
    |
20 | | simplll 533 |
. . . . . . . . . . 11
   
        
     |
21 | | simplrl 535 |
. . . . . . . . . . 11
   
        
  
  |
22 | | simplrr 536 |
. . . . . . . . . . 11
   
        
     |
23 | 4 | mopntopon 13913 |
. . . . . . . . . . . . . . . . . 18
      TopOn    |
24 | 2, 23 | syl 14 |
. . . . . . . . . . . . . . . . 17
 TopOn    |
25 | 24 | adantr 276 |
. . . . . . . . . . . . . . . 16
 

 
TopOn    |
26 | | simprl 529 |
. . . . . . . . . . . . . . . 16
 

 
  |
27 | | toponss 13496 |
. . . . . . . . . . . . . . . 16
  TopOn     |
28 | 25, 26, 27 | syl2anc 411 |
. . . . . . . . . . . . . . 15
 

    |
29 | 5 | mopntopon 13913 |
. . . . . . . . . . . . . . . . . 18
      TopOn    |
30 | 3, 29 | syl 14 |
. . . . . . . . . . . . . . . . 17
 TopOn    |
31 | 30 | adantr 276 |
. . . . . . . . . . . . . . . 16
 

 
TopOn    |
32 | | simprr 531 |
. . . . . . . . . . . . . . . 16
 

    |
33 | | toponss 13496 |
. . . . . . . . . . . . . . . 16
  TopOn     |
34 | 31, 32, 33 | syl2anc 411 |
. . . . . . . . . . . . . . 15
 

 
  |
35 | | xpss12 4733 |
. . . . . . . . . . . . . . 15
 
  
    |
36 | 28, 34, 35 | syl2anc 411 |
. . . . . . . . . . . . . 14
 

   
    |
37 | 1, 2, 3 | xmetxp 13977 |
. . . . . . . . . . . . . . . 16
          |
38 | | unirnbl 13893 |
. . . . . . . . . . . . . . . 16
                 |
39 | 37, 38 | syl 14 |
. . . . . . . . . . . . . . 15
          |
40 | 39 | adantr 276 |
. . . . . . . . . . . . . 14
 

           |
41 | 36, 40 | sseqtrrd 3194 |
. . . . . . . . . . . . 13
 

   
       |
42 | 2 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
   
 

         |
43 | | simplrl 535 |
. . . . . . . . . . . . . . . 16
   
 

    |
44 | | xp1st 6165 |
. . . . . . . . . . . . . . . . 17
         |
45 | 44 | adantl 277 |
. . . . . . . . . . . . . . . 16
   
 

        |
46 | 4 | mopni2 13953 |
. . . . . . . . . . . . . . . 16
                           |
47 | 42, 43, 45, 46 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
   
 

                 |
48 | 3 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
   
 

         |
49 | | simplrr 536 |
. . . . . . . . . . . . . . . . . 18
   
 

    |
50 | | xp2nd 6166 |
. . . . . . . . . . . . . . . . . . 19
         |
51 | 50 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
   
 

        |
52 | 5 | mopni2 13953 |
. . . . . . . . . . . . . . . . . 18
                           |
53 | 48, 49, 51, 52 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
   
 

                 |
54 | 53 | adantr 276 |
. . . . . . . . . . . . . . . 16
    
                    
              |
55 | | blf 13880 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
56 | 37, 55 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
                  |
57 | 56 | ffnd 5366 |
. . . . . . . . . . . . . . . . . . 19
           |
58 | 57 | ad4antr 494 |
. . . . . . . . . . . . . . . . . 18
     
                    
                        |
59 | 36 | sselda 3155 |
. . . . . . . . . . . . . . . . . . 19
   
 

      |
60 | 59 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
     
                    
                  |
61 | | rpxr 9660 |
. . . . . . . . . . . . . . . . . . . . 21

  |
62 | 61 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . . 20
    
                   
  |
63 | 62 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
     
                    
             
  |
64 | | rpxr 9660 |
. . . . . . . . . . . . . . . . . . . 20

  |
65 | 64 | ad2antrl 490 |
. . . . . . . . . . . . . . . . . . 19
     
                    
             
  |
66 | | xrmincl 11273 |
. . . . . . . . . . . . . . . . . . 19
   inf        |
67 | 63, 65, 66 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
     
                    
              inf    
   |
68 | | fnovrn 6021 |
. . . . . . . . . . . . . . . . . 18
           
inf             inf             |
69 | 58, 60, 67, 68 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
     
                    
                    inf             |
70 | | eleq2 2241 |
. . . . . . . . . . . . . . . . . . 19
       inf    
 

      inf          |
71 | | sseq1 3178 |
. . . . . . . . . . . . . . . . . . 19
       inf    
 
         inf    
 
     |
72 | 70, 71 | anbi12d 473 |
. . . . . . . . . . . . . . . . . 18
       inf    
 
    
       inf      
      inf    
 
      |
73 | 72 | adantl 277 |
. . . . . . . . . . . . . . . . 17
     

 
   
              
             
      inf    
               inf      
      inf    
 
      |
74 | 37 | ad4antr 494 |
. . . . . . . . . . . . . . . . . . 19
     
                    
             
         |
75 | | simplrl 535 |
. . . . . . . . . . . . . . . . . . . 20
     
                    
             
  |
76 | | simprl 529 |
. . . . . . . . . . . . . . . . . . . 20
     
                    
             
  |
77 | | xrminrpcl 11281 |
. . . . . . . . . . . . . . . . . . . 20
   inf        |
78 | 75, 76, 77 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
     
                    
              inf    
   |
79 | | blcntr 13886 |
. . . . . . . . . . . . . . . . . . 19
           inf             inf         |
80 | 74, 60, 78, 79 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . 18
     
                    
                    inf         |
81 | 42 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
     
                    
             
       |
82 | 48 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . 20
     
                    
             
       |
83 | 1, 81, 82, 67, 60 | xmetxpbl 13978 |
. . . . . . . . . . . . . . . . . . 19
     
                    
                    inf                  inf                 inf          |
84 | 28 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 

    |
85 | 84, 45 | sseldd 3156 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 

        |
86 | 85 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                    
                    |
87 | | xrmin1inf 11274 |
. . . . . . . . . . . . . . . . . . . . . . 23
   inf        |
88 | 63, 65, 87 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                    
              inf    
   |
89 | | ssbl 13896 |
. . . . . . . . . . . . . . . . . . . . . 22
       
    
inf    

 inf    
            inf                     |
90 | 81, 86, 67, 63, 88, 89 | syl221anc 1249 |
. . . . . . . . . . . . . . . . . . . . 21
     
                    
                        inf                     |
91 | | simplrr 536 |
. . . . . . . . . . . . . . . . . . . . 21
     
                    
                            |
92 | 90, 91 | sstrd 3165 |
. . . . . . . . . . . . . . . . . . . 20
     
                    
                        inf         |
93 | 34 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 

    |
94 | 93, 51 | sseldd 3156 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
 

        |
95 | 94 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                    
                    |
96 | | xrmin2inf 11275 |
. . . . . . . . . . . . . . . . . . . . . . 23
   inf        |
97 | 63, 65, 96 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                    
              inf    
   |
98 | | ssbl 13896 |
. . . . . . . . . . . . . . . . . . . . . 22
       
    
inf    

 inf    
            inf                     |
99 | 82, 95, 67, 65, 97, 98 | syl221anc 1249 |
. . . . . . . . . . . . . . . . . . . . 21
     
                    
                        inf                     |
100 | | simprr 531 |
. . . . . . . . . . . . . . . . . . . . 21
     
                    
                            |
101 | 99, 100 | sstrd 3165 |
. . . . . . . . . . . . . . . . . . . 20
     
                    
                        inf         |
102 | | xpss12 4733 |
. . . . . . . . . . . . . . . . . . . 20
            inf                 inf      
            inf                 inf            |
103 | 92, 101, 102 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
     
                    
                         inf                 inf            |
104 | 83, 103 | eqsstrd 3191 |
. . . . . . . . . . . . . . . . . 18
     
                    
                    inf      
    |
105 | 80, 104 | jca 306 |
. . . . . . . . . . . . . . . . 17
     
                    
                     inf             inf      
     |
106 | 69, 73, 105 | rspcedvd 2847 |
. . . . . . . . . . . . . . . 16
     
                    
              
           |
107 | 54, 106 | rexlimddv 2599 |
. . . . . . . . . . . . . . 15
    
                    
           |
108 | 47, 107 | rexlimddv 2599 |
. . . . . . . . . . . . . 14
   
 

         
    |
109 | 108 | ralrimiva 2550 |
. . . . . . . . . . . . 13
 

  
               |
110 | 41, 109 | jca 306 |
. . . . . . . . . . . 12
 

                           |
111 | | blex 13857 |
. . . . . . . . . . . . . . 15
              |
112 | 37, 111 | syl 14 |
. . . . . . . . . . . . . 14
       |
113 | 112 | adantr 276 |
. . . . . . . . . . . . 13
 

        |
114 | | rnexg 4892 |
. . . . . . . . . . . . 13
    
      |
115 | | eltg2 13523 |
. . . . . . . . . . . . 13
               
        
          
      |
116 | 113, 114,
115 | 3syl 17 |
. . . . . . . . . . . 12
 

            
        
          
      |
117 | 110, 116 | mpbird 167 |
. . . . . . . . . . 11
 

              |
118 | 20, 21, 22, 117 | syl12anc 1236 |
. . . . . . . . . 10
   
        
               |
119 | 19, 118 | eqeltrd 2254 |
. . . . . . . . 9
   
        
  
          |
120 | 119 | ex 115 |
. . . . . . . 8
                          |
121 | 120 | rexlimdvva 2602 |
. . . . . . 7
 
 
                    |
122 | 18, 121 | mpd 13 |
. . . . . 6
 
 
   
          |
123 | 122 | ex 115 |
. . . . 5
   
              |
124 | 123 | ssrdv 3161 |
. . . 4
                |
125 | 4 | mopntop 13914 |
. . . . . . . 8
        |
126 | 2, 125 | syl 14 |
. . . . . . 7
   |
127 | 5 | mopntop 13914 |
. . . . . . . 8
        |
128 | 3, 127 | syl 14 |
. . . . . . 7
   |
129 | | mpoexga 6212 |
. . . . . . 7
 
  
     |
130 | 126, 128,
129 | syl2anc 411 |
. . . . . 6
  
     |
131 | | rnexg 4892 |
. . . . . 6
       
     |
132 | 130, 131 | syl 14 |
. . . . 5
        |
133 | 37, 111, 114 | 3syl 17 |
. . . . 5
       |
134 | | tgss3 13548 |
. . . . 5
      
                                       |
135 | 132, 133,
134 | syl2anc 411 |
. . . 4
      
           
                |
136 | 124, 135 | mpbird 167 |
. . 3
         
          |
137 | | eqid 2177 |
. . . . 5
           |
138 | 137 | txval 13725 |
. . . 4
 
              |
139 | 126, 128,
138 | syl2anc 411 |
. . 3
              |
140 | 6 | mopnval 13912 |
. . . 4
                  |
141 | 37, 140 | syl 14 |
. . 3
           |
142 | 136, 139,
141 | 3sstr4d 3200 |
. 2
  
  |
143 | 7, 142 | eqssd 3172 |
1
     |