Step | Hyp | Ref
| Expression |
1 | | ptcmp.1 |
. . 3
 
                 |
2 | | ptcmp.2 |
. . 3
       |
3 | | ptcmp.3 |
. . 3
   |
4 | | ptcmp.4 |
. . 3
       |
5 | | ptcmp.5 |
. . 3
 UFL    |
6 | | ptcmplem2.5 |
. . 3

  |
7 | | ptcmplem2.6 |
. . 3
    |
8 | | ptcmplem2.7 |
. . 3
         |
9 | | ptcmplem3.8 |
. . 3
                  |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | ptcmplem3 21069 |
. 2
    
               |
11 | | simprl 764 |
. . . . . . . . 9
 


                |
12 | | eldifi 3555 |
. . . . . . . . . . . 12
                        |
13 | 12 | ralimi 2781 |
. . . . . . . . . . 11
 
            
           |
14 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
15 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
16 | 15 | unieqd 4208 |
. . . . . . . . . . . . 13
             |
17 | 14, 16 | eleq12d 2523 |
. . . . . . . . . . . 12
                       |
18 | 17 | cbvralv 3019 |
. . . . . . . . . . 11
 
        

           |
19 | 13, 18 | sylibr 216 |
. . . . . . . . . 10
 
            
           |
20 | 19 | ad2antll 735 |
. . . . . . . . 9
 


                          |
21 | | vex 3048 |
. . . . . . . . . 10
 |
22 | 21 | elixp 7529 |
. . . . . . . . 9
        
            |
23 | 11, 20, 22 | sylanbrc 670 |
. . . . . . . 8
 


              
       |
24 | 23, 2 | syl6eleqr 2540 |
. . . . . . 7
 


                |
25 | 7 | adantr 467 |
. . . . . . 7
 


                 |
26 | 24, 25 | eleqtrd 2531 |
. . . . . 6
 


                 |
27 | | eluni2 4202 |
. . . . . 6
 

  |
28 | 26, 27 | sylib 200 |
. . . . 5
 


              
  |
29 | | simplrr 771 |
. . . . . . . . . . . . . . . . 17
   
 
                
  |
30 | 29 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                            |
31 | | simprr 766 |
. . . . . . . . . . . . . . . 16
                                                       |
32 | 30, 31 | eleqtrd 2531 |
. . . . . . . . . . . . . . 15
                                                       |
33 | | fveq1 5864 |
. . . . . . . . . . . . . . . . . 18
           |
34 | 33 | eleq1d 2513 |
. . . . . . . . . . . . . . . . 17
     
       |
35 | | eqid 2451 |
. . . . . . . . . . . . . . . . . 18
             |
36 | 35 | mptpreima 5328 |
. . . . . . . . . . . . . . . . 17
           
      |
37 | 34, 36 | elrab2 3198 |
. . . . . . . . . . . . . . . 16
                    |
38 | 37 | simprbi 466 |
. . . . . . . . . . . . . . 15
                  |
39 | 32, 38 | syl 17 |
. . . . . . . . . . . . . 14
                                                |
40 | | simprl 764 |
. . . . . . . . . . . . . . . 16
                                                |
41 | | simplrl 770 |
. . . . . . . . . . . . . . . . . 18
   
 
                
  |
42 | 41 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                                            |
43 | 31, 42 | eqeltrrd 2530 |
. . . . . . . . . . . . . . . 16
                                                       |
44 | | rabid 2967 |
. . . . . . . . . . . . . . . 16
                                     |
45 | 40, 43, 44 | sylanbrc 670 |
. . . . . . . . . . . . . . 15
                                                             |
46 | 45, 9 | syl6eleqr 2540 |
. . . . . . . . . . . . . 14
                                            |
47 | | elunii 4203 |
. . . . . . . . . . . . . 14
     
        |
48 | 39, 46, 47 | syl2anc 667 |
. . . . . . . . . . . . 13
                                                 |
49 | 48 | rexlimdvaa 2880 |
. . . . . . . . . . . 12
   
 
                
 
                        |
50 | 49 | expr 620 |
. . . . . . . . . . 11
   
 
                                           |
51 | 50 | ralimdva 2796 |
. . . . . . . . . 10
    
 
 
            
 
                         |
52 | 51 | ex 436 |
. . . . . . . . 9
 
  

 
            
 
                          |
53 | 52 | com23 81 |
. . . . . . . 8
 
  
               
 
                          |
54 | 53 | impr 625 |
. . . . . . 7
 


                 
 
                         |
55 | 54 | imp 431 |
. . . . . 6
                      
                 
        |
56 | 6 | adantr 467 |
. . . . . . . . . 10
 


                |
57 | 56 | sselda 3432 |
. . . . . . . . 9
                      |
58 | 57 | adantrr 723 |
. . . . . . . 8
                        |
59 | 1 | rnmpt2 6406 |
. . . . . . . 8
 

                  |
60 | 58, 59 | syl6eleq 2539 |
. . . . . . 7
                                            |
61 | | abid 2439 |
. . . . . . 7
   
                

                   |
62 | 60, 61 | sylib 200 |
. . . . . 6
                      

                  |
63 | | rexim 2852 |
. . . . . 6
 
 
               
       

               

        |
64 | 55, 62, 63 | sylc 62 |
. . . . 5
                      
       |
65 | 28, 64 | rexlimddv 2883 |
. . . 4
 


                      |
66 | | eldifn 3556 |
. . . . . . 7
                    |
67 | 66 | ralimi 2781 |
. . . . . 6
 
            
       |
68 | 67 | ad2antll 735 |
. . . . 5
 


                      |
69 | | ralnex 2834 |
. . . . 5
 
             |
70 | 68, 69 | sylib 200 |
. . . 4
 


             

       |
71 | 65, 70 | pm2.65da 580 |
. . 3
  
               |
72 | 71 | nexdv 1782 |
. 2
                    |
73 | 10, 72 | pm2.65i 177 |
1
 |