Proof of Theorem tfrcllembxssdm
Step | Hyp | Ref
| Expression |
1 | | tfrcllembacc.5 |
. . . 4
         
             |
2 | | fveq2 5511 |
. . . . . . . . 9
           |
3 | | reseq2 4898 |
. . . . . . . . . 10
       |
4 | 3 | fveq2d 5515 |
. . . . . . . . 9
               |
5 | 2, 4 | eqeq12d 2192 |
. . . . . . . 8
           
             |
6 | 5 | cbvralv 2703 |
. . . . . . 7
 
         

            |
7 | 6 | anbi2i 457 |
. . . . . 6
                       
             |
8 | 7 | exbii 1605 |
. . . . 5
        
          
       
             |
9 | 8 | ralbii 2483 |
. . . 4
 
       
          

       
             |
10 | 1, 9 | sylib 122 |
. . 3
         
             |
11 | | simp1 997 |
. . . . . . . 8
 
     
              |
12 | | simp2 998 |
. . . . . . . . 9
 
     
              |
13 | | tfrcllembacc.4 |
. . . . . . . . . 10
   |
14 | 11, 13 | syl 14 |
. . . . . . . . 9
 
     
              |
15 | | tfrcl.x |
. . . . . . . . . . 11
   |
16 | | ordtr1 4385 |
. . . . . . . . . . 11

 
    |
17 | 15, 16 | syl 14 |
. . . . . . . . . 10
       |
18 | 17 | imp 124 |
. . . . . . . . 9
 

    |
19 | 11, 12, 14, 18 | syl12anc 1236 |
. . . . . . . 8
 
     
              |
20 | | simp3l 1025 |
. . . . . . . 8
 
     
                  |
21 | | feq2 5345 |
. . . . . . . . . . . . 13
     
       |
22 | 21 | imbi1d 231 |
. . . . . . . . . . . 12
      
                  |
23 | 22 | albidv 1824 |
. . . . . . . . . . 11
             
      
        |
24 | | tfrcl.ex |
. . . . . . . . . . . . . . 15
 
           |
25 | 24 | 3expia 1205 |
. . . . . . . . . . . . . 14
 
             |
26 | 25 | alrimiv 1874 |
. . . . . . . . . . . . 13
 
       
       |
27 | 26 | ralrimiva 2550 |
. . . . . . . . . . . 12
                |
28 | 27 | adantr 276 |
. . . . . . . . . . 11
 
 
      
       |
29 | | simpr 110 |
. . . . . . . . . . 11
 
   |
30 | 23, 28, 29 | rspcdva 2846 |
. . . . . . . . . 10
 
       
       |
31 | | feq1 5344 |
. . . . . . . . . . . 12
             |
32 | | fveq2 5511 |
. . . . . . . . . . . . 13
           |
33 | 32 | eleq1d 2246 |
. . . . . . . . . . . 12
     
       |
34 | 31, 33 | imbi12d 234 |
. . . . . . . . . . 11
      
                  |
35 | 34 | spv 1860 |
. . . . . . . . . 10
                         |
36 | 30, 35 | syl 14 |
. . . . . . . . 9
 
             |
37 | 36 | imp 124 |
. . . . . . . 8
               |
38 | 11, 19, 20, 37 | syl21anc 1237 |
. . . . . . 7
 
     
                  |
39 | | vex 2740 |
. . . . . . . . . 10
 |
40 | | opexg 4225 |
. . . . . . . . . 10
                |
41 | 39, 38, 40 | sylancr 414 |
. . . . . . . . 9
 
     
                     |
42 | | snidg 3620 |
. . . . . . . . 9
       
                  |
43 | | elun2 3303 |
. . . . . . . . 9
                
                    |
44 | 41, 42, 43 | 3syl 17 |
. . . . . . . 8
 
     
                                |
45 | | simp3r 1026 |
. . . . . . . . . . . . 13
 
     
                         |
46 | | rspe 2526 |
. . . . . . . . . . . . 13
       
           

                   |
47 | 19, 20, 45, 46 | syl12anc 1236 |
. . . . . . . . . . . 12
 
     
                  
             |
48 | | feq2 5345 |
. . . . . . . . . . . . . 14
             |
49 | | raleq 2672 |
. . . . . . . . . . . . . 14
  
         

             |
50 | 48, 49 | anbi12d 473 |
. . . . . . . . . . . . 13
       
                
              |
51 | 50 | cbvrexv 2704 |
. . . . . . . . . . . 12
                   
     
             |
52 | 47, 51 | sylib 122 |
. . . . . . . . . . 11
 
     
                  
             |
53 | | vex 2740 |
. . . . . . . . . . . 12
 |
54 | | feq1 5344 |
. . . . . . . . . . . . . 14
     
       |
55 | | fveq1 5510 |
. . . . . . . . . . . . . . . 16
           |
56 | | reseq1 4897 |
. . . . . . . . . . . . . . . . 17
       |
57 | 56 | fveq2d 5515 |
. . . . . . . . . . . . . . . 16
               |
58 | 55, 57 | eqeq12d 2192 |
. . . . . . . . . . . . . . 15
           
             |
59 | 58 | ralbidv 2477 |
. . . . . . . . . . . . . 14
  
         

             |
60 | 54, 59 | anbi12d 473 |
. . . . . . . . . . . . 13
       
                
              |
61 | 60 | rexbidv 2478 |
. . . . . . . . . . . 12
  
     
           
     
              |
62 | | tfrcllemsucfn.1 |
. . . . . . . . . . . 12
 
                   |
63 | 53, 61, 62 | elab2 2885 |
. . . . . . . . . . 11


                   |
64 | 52, 63 | sylibr 134 |
. . . . . . . . . 10
 
     
              |
65 | 12, 20, 64 | 3jca 1177 |
. . . . . . . . 9
 
     
                    |
66 | | snexg 4181 |
. . . . . . . . . . 11
       
           |
67 | | unexg 4440 |
. . . . . . . . . . . 12
          
              |
68 | 53, 67 | mpan 424 |
. . . . . . . . . . 11
         
             |
69 | 41, 66, 68 | 3syl 17 |
. . . . . . . . . 10
 
     
                         |
70 | | isset 2743 |
. . . . . . . . . 10
           

             |
71 | 69, 70 | sylib 122 |
. . . . . . . . 9
 
     
                          |
72 | | simpr3 1005 |
. . . . . . . . . . . . 13
                                 |
73 | | 19.8a 1590 |
. . . . . . . . . . . . . 14
     
           
                     |
74 | | rspe 2526 |
. . . . . . . . . . . . . . 15
        
                    
              |
75 | | tfrcllembacc.3 |
. . . . . . . . . . . . . . . 16
 
      
              |
76 | 75 | abeq2i 2288 |
. . . . . . . . . . . . . . 15


                     |
77 | 74, 76 | sylibr 134 |
. . . . . . . . . . . . . 14
        
               |
78 | 73, 77 | sylan2 286 |
. . . . . . . . . . . . 13
                      |
79 | 72, 78 | eqeltrrd 2255 |
. . . . . . . . . . . 12
                                 |
80 | 79 | 3exp2 1225 |
. . . . . . . . . . 11
      
                            |
81 | 80 | 3imp 1193 |
. . . . . . . . . 10
     
                           |
82 | 81 | exlimdv 1819 |
. . . . . . . . 9
     
                            |
83 | 65, 71, 82 | sylc 62 |
. . . . . . . 8
 
     
                         |
84 | | elunii 3812 |
. . . . . . . 8
                                          |
85 | 44, 83, 84 | syl2anc 411 |
. . . . . . 7
 
     
                      |
86 | | opeq2 3777 |
. . . . . . . . . 10
       
         |
87 | 86 | eleq1d 2246 |
. . . . . . . . 9
         
           |
88 | 87 | spcegv 2825 |
. . . . . . . 8
                       |
89 | 39 | eldm2 4821 |
. . . . . . . 8
          |
90 | 88, 89 | syl6ibr 162 |
. . . . . . 7
                  |
91 | 38, 85, 90 | sylc 62 |
. . . . . 6
 
     
               |
92 | 91 | 3expia 1205 |
. . . . 5
 
       
               |
93 | 92 | exlimdv 1819 |
. . . 4
 
         
               |
94 | 93 | ralimdva 2544 |
. . 3
                      
    |
95 | 10, 94 | mpd 13 |
. 2
 
   |
96 | | dfss3 3145 |
. 2



   |
97 | 95, 96 | sylibr 134 |
1

   |