Step | Hyp | Ref
| Expression |
1 | | prdsbl.y |
. . . . . . . . 9
  s    |
2 | | prdsbl.b |
. . . . . . . . 9
     |
3 | | prdsbl.s |
. . . . . . . . 9
   |
4 | | prdsbl.i |
. . . . . . . . 9
   |
5 | | prdsbl.r |
. . . . . . . . . 10
 
   |
6 | 5 | ralrimiva 2809 |
. . . . . . . . 9
 
  |
7 | | prdsbl.v |
. . . . . . . . 9
     |
8 | 1, 2, 3, 4, 6, 7 | prdsbas3 15457 |
. . . . . . . 8
 
  |
9 | 8 | eleq2d 2534 |
. . . . . . 7
      |
10 | 9 | biimpa 492 |
. . . . . 6
 
    |
11 | | ixpfn 7546 |
. . . . . 6
    |
12 | | vex 3034 |
. . . . . . . 8
 |
13 | 12 | elixp 7547 |
. . . . . . 7
                                   |
14 | 13 | baib 919 |
. . . . . 6
  
           

                   |
15 | 10, 11, 14 | 3syl 18 |
. . . . 5
 
  
           

                   |
16 | | prdsbl.m |
. . . . . . . 8
 
        |
17 | 16 | adantlr 729 |
. . . . . . 7
            |
18 | | prdsbl.a |
. . . . . . . 8
   |
19 | 18 | ad2antrr 740 |
. . . . . . 7
       |
20 | | prdsbl.p |
. . . . . . . . . 10
   |
21 | 1, 2, 3, 4, 6, 7, 20 | prdsbascl 15459 |
. . . . . . . . 9
        |
22 | 21 | adantr 472 |
. . . . . . . 8
 
 
      |
23 | 22 | r19.21bi 2776 |
. . . . . . 7
           |
24 | 3 | adantr 472 |
. . . . . . . . 9
 
   |
25 | 4 | adantr 472 |
. . . . . . . . 9
 
   |
26 | 6 | adantr 472 |
. . . . . . . . 9
 
 
  |
27 | | simpr 468 |
. . . . . . . . 9
 
   |
28 | 1, 2, 24, 25, 26, 7, 27 | prdsbascl 15459 |
. . . . . . . 8
 
 
      |
29 | 28 | r19.21bi 2776 |
. . . . . . 7
           |
30 | | elbl2 21483 |
. . . . . . 7
       
                            
               |
31 | 17, 19, 23, 29, 30 | syl22anc 1293 |
. . . . . 6
                     
               |
32 | 31 | ralbidva 2828 |
. . . . 5
 
  
               

               |
33 | | xmetcl 21424 |
. . . . . . . . . 10
                              |
34 | 17, 23, 29, 33 | syl3anc 1292 |
. . . . . . . . 9
                   |
35 | 34 | ralrimiva 2809 |
. . . . . . . 8
 
 
              |
36 | | eqid 2471 |
. . . . . . . . 9
                             |
37 | | breq1 4398 |
. . . . . . . . 9
             
               |
38 | 36, 37 | ralrnmpt 6046 |
. . . . . . . 8
 
           
 
              

               |
39 | 35, 38 | syl 17 |
. . . . . . 7
 
  

                              |
40 | | prdsbl.g |
. . . . . . . . . 10
   |
41 | 40 | adantr 472 |
. . . . . . . . 9
 
   |
42 | | c0ex 9655 |
. . . . . . . . . 10
 |
43 | | breq1 4398 |
. . . . . . . . . 10
 
   |
44 | 42, 43 | ralsn 4001 |
. . . . . . . . 9
 
     |
45 | 41, 44 | sylibr 217 |
. . . . . . . 8
 
       |
46 | | ralunb 3606 |
. . . . . . . . 9
 
 
                
 
                      |
47 | 20 | adantr 472 |
. . . . . . . . . . . 12
 
   |
48 | | prdsbl.e |
. . . . . . . . . . . 12
         |
49 | | prdsbl.d |
. . . . . . . . . . . 12
     |
50 | 1, 2, 24, 25, 26, 47, 27, 7, 48, 49 | prdsdsval3 15461 |
. . . . . . . . . . 11
 
                          
  |
51 | | xrltso 11463 |
. . . . . . . . . . . . 13
 |
52 | 51 | a1i 11 |
. . . . . . . . . . . 12
 
   |
53 | 36 | rnmpt 5086 |
. . . . . . . . . . . . . . 15
                              |
54 | | abrexfi 7892 |
. . . . . . . . . . . . . . 15
                  |
55 | 53, 54 | syl5eqel 2553 |
. . . . . . . . . . . . . 14
 
               |
56 | 25, 55 | syl 17 |
. . . . . . . . . . . . 13
 
 
               |
57 | | snfi 7668 |
. . . . . . . . . . . . 13
   |
58 | | unfi 7856 |
. . . . . . . . . . . . 13
               
 
                     |
59 | 56, 57, 58 | sylancl 675 |
. . . . . . . . . . . 12
 
                     |
60 | | ssun2 3589 |
. . . . . . . . . . . . . 14
 
 
                 |
61 | 42 | snss 4087 |
. . . . . . . . . . . . . 14
                  
                      |
62 | 60, 61 | mpbir 214 |
. . . . . . . . . . . . 13
                   |
63 | | ne0i 3728 |
. . . . . . . . . . . . 13
                                       |
64 | 62, 63 | mp1i 13 |
. . . . . . . . . . . 12
 
                     |
65 | 34, 36 | fmptd 6061 |
. . . . . . . . . . . . . 14
 
                     |
66 | | frn 5747 |
. . . . . . . . . . . . . 14
                                   |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . 13
 
 
               |
68 | | 0xr 9705 |
. . . . . . . . . . . . . . 15
 |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
70 | 69 | snssd 4108 |
. . . . . . . . . . . . 13
 
  
  |
71 | 67, 70 | unssd 3601 |
. . . . . . . . . . . 12
 
                     |
72 | | fisupcl 8003 |
. . . . . . . . . . . 12
  

                                                                                                |
73 | 52, 59, 64, 71, 72 | syl13anc 1294 |
. . . . . . . . . . 11
 
                                           |
74 | 50, 73 | eqeltrd 2549 |
. . . . . . . . . 10
 
                         |
75 | | breq1 4398 |
. . . . . . . . . . 11
     
       |
76 | 75 | rspcv 3132 |
. . . . . . . . . 10
                        
                          |
77 | 74, 76 | syl 17 |
. . . . . . . . 9
 
  
                          |
78 | 46, 77 | syl5bir 226 |
. . . . . . . 8
 
                   
   
       |
79 | 45, 78 | mpan2d 688 |
. . . . . . 7
 
  

             
       |
80 | 39, 79 | sylbird 243 |
. . . . . 6
 
  
                   |
81 | 71 | adantr 472 |
. . . . . . . . . 10
                         |
82 | | ssun1 3588 |
. . . . . . . . . . 11
             
 
                 |
83 | | ovex 6336 |
. . . . . . . . . . . . . 14
             |
84 | 83 | elabrex 6166 |
. . . . . . . . . . . . 13
                              |
85 | 84 | adantl 473 |
. . . . . . . . . . . 12
                                  |
86 | 85, 53 | syl6eleqr 2560 |
. . . . . . . . . . 11
                                 |
87 | 82, 86 | sseldi 3416 |
. . . . . . . . . 10
                                     |
88 | | supxrub 11635 |
. . . . . . . . . 10
                   
                                          
  

                    |
89 | 81, 87, 88 | syl2anc 673 |
. . . . . . . . 9
                                      
  |
90 | 50 | adantr 472 |
. . . . . . . . 9
                              
  |
91 | 89, 90 | breqtrrd 4422 |
. . . . . . . 8
                       |
92 | 1, 2, 7, 48, 49, 3, 4, 5, 16 | prdsxmet 21462 |
. . . . . . . . . . 11
        |
93 | 92 | ad2antrr 740 |
. . . . . . . . . 10
            |
94 | 20 | ad2antrr 740 |
. . . . . . . . . 10
       |
95 | 27 | adantr 472 |
. . . . . . . . . 10
       |
96 | | xmetcl 21424 |
. . . . . . . . . 10
      

      |
97 | 93, 94, 95, 96 | syl3anc 1292 |
. . . . . . . . 9
           |
98 | | xrlelttr 11476 |
. . . . . . . . 9
                 

             
                        |
99 | 34, 97, 19, 98 | syl3anc 1292 |
. . . . . . . 8
                                           |
100 | 91, 99 | mpand 689 |
. . . . . . 7
                         |
101 | 100 | ralrimdva 2812 |
. . . . . 6
 
      
               |
102 | 80, 101 | impbid 195 |
. . . . 5
 
  
           
       |
103 | 15, 32, 102 | 3bitrrd 288 |
. . . 4
 
     
                |
104 | 103 | pm5.32da 653 |
. . 3
       

                 |
105 | | elbl 21481 |
. . . 4
      
         

        |
106 | 92, 20, 18, 105 | syl3anc 1292 |
. . 3
         

        |
107 | 21 | r19.21bi 2776 |
. . . . . . . . 9
 
       |
108 | 18 | adantr 472 |
. . . . . . . . 9
 
   |
109 | | blssm 21511 |
. . . . . . . . 9
          
               |
110 | 16, 107, 108, 109 | syl3anc 1292 |
. . . . . . . 8
 
               |
111 | 110 | ralrimiva 2809 |
. . . . . . 7
                |
112 | | ss2ixp 7553 |
. . . . . . 7
 
                            |
113 | 111, 112 | syl 17 |
. . . . . 6
                 |
114 | 113, 8 | sseqtr4d 3455 |
. . . . 5
                |
115 | 114 | sseld 3417 |
. . . 4
  
               |
116 | 115 | pm4.71rd 647 |
. . 3
  
           

                 |
117 | 104, 106,
116 | 3bitr4d 293 |
. 2
         
                |
118 | 117 | eqrdv 2469 |
1
                        |