Step | Hyp | Ref
| Expression |
1 | | tfrcl.x |
. . . . . . . . . 10
   |
2 | 1 | adantr 272 |
. . . . . . . . 9
 
   |
3 | | simpr 109 |
. . . . . . . . . 10
 
   |
4 | | tfrcllemres.yx |
. . . . . . . . . . 11
   |
5 | 4 | adantr 272 |
. . . . . . . . . 10
 
   |
6 | 3, 5 | jca 302 |
. . . . . . . . 9
 
 
   |
7 | | ordtr1 4248 |
. . . . . . . . 9

 
    |
8 | 2, 6, 7 | sylc 62 |
. . . . . . . 8
 
   |
9 | | tfrcl.f |
. . . . . . . . 9
recs   |
10 | | tfrcl.g |
. . . . . . . . 9
   |
11 | | tfrcl.ex |
. . . . . . . . 9
 
           |
12 | | tfrcllemsucfn.1 |
. . . . . . . . 9
 
                   |
13 | | tfrcllemres.u |
. . . . . . . . 9
 
 
  |
14 | 9, 10, 1, 11, 12, 13 | tfrcllemaccex 6188 |
. . . . . . . 8
 
        
             |
15 | 8, 14 | syldan 278 |
. . . . . . 7
 
        
             |
16 | 10 | ad2antrr 475 |
. . . . . . . . 9
                     
  |
17 | 1 | ad2antrr 475 |
. . . . . . . . 9
                     
  |
18 | 11 | 3adant1r 1177 |
. . . . . . . . . 10
   
           |
19 | 18 | 3adant1r 1177 |
. . . . . . . . 9
   
      
                       |
20 | 4 | ad2antrr 475 |
. . . . . . . . 9
                     
  |
21 | 3 | adantr 272 |
. . . . . . . . 9
                     
  |
22 | 13 | adantlr 464 |
. . . . . . . . . 10
        |
23 | 22 | adantlr 464 |
. . . . . . . . 9
   
      
                |
24 | | simprl 501 |
. . . . . . . . 9
                     
      |
25 | | feq2 5192 |
. . . . . . . . . . . . . 14
     
       |
26 | | raleq 2584 |
. . . . . . . . . . . . . 14
  
         

             |
27 | 25, 26 | anbi12d 460 |
. . . . . . . . . . . . 13
       
                
              |
28 | | fveq2 5353 |
. . . . . . . . . . . . . . . 16
           |
29 | | reseq2 4750 |
. . . . . . . . . . . . . . . . 17
       |
30 | 29 | fveq2d 5357 |
. . . . . . . . . . . . . . . 16
               |
31 | 28, 30 | eqeq12d 2114 |
. . . . . . . . . . . . . . 15
           
             |
32 | 31 | cbvralv 2612 |
. . . . . . . . . . . . . 14
 
         

            |
33 | 32 | anbi2i 448 |
. . . . . . . . . . . . 13
                       
             |
34 | 27, 33 | syl6bb 195 |
. . . . . . . . . . . 12
       
                
              |
35 | 34 | rspcev 2744 |
. . . . . . . . . . 11
       
           

                   |
36 | 8, 35 | sylan 279 |
. . . . . . . . . 10
                     

                   |
37 | | vex 2644 |
. . . . . . . . . . 11
 |
38 | | feq1 5191 |
. . . . . . . . . . . . 13
     
       |
39 | | fveq1 5352 |
. . . . . . . . . . . . . . 15
           |
40 | | reseq1 4749 |
. . . . . . . . . . . . . . . 16
       |
41 | 40 | fveq2d 5357 |
. . . . . . . . . . . . . . 15
               |
42 | 39, 41 | eqeq12d 2114 |
. . . . . . . . . . . . . 14
           
             |
43 | 42 | ralbidv 2396 |
. . . . . . . . . . . . 13
  
         

             |
44 | 38, 43 | anbi12d 460 |
. . . . . . . . . . . 12
       
                
              |
45 | 44 | rexbidv 2397 |
. . . . . . . . . . 11
  
     
           
     
              |
46 | 37, 45, 12 | elab2 2785 |
. . . . . . . . . 10


                   |
47 | 36, 46 | sylibr 133 |
. . . . . . . . 9
                     
  |
48 | 9, 16, 17, 19, 12, 20, 21, 23, 24, 47 | tfrcllemsucaccv 6181 |
. . . . . . . 8
                     
             |
49 | | vex 2644 |
. . . . . . . . . . 11
 |
50 | 25 | imbi1d 230 |
. . . . . . . . . . . . . 14
      
                  |
51 | 11 | 3expia 1151 |
. . . . . . . . . . . . . . . . . 18
 
             |
52 | 51 | alrimiv 1813 |
. . . . . . . . . . . . . . . . 17
 
       
       |
53 | | fveq2 5353 |
. . . . . . . . . . . . . . . . . . . 20
           |
54 | 53 | eleq1d 2168 |
. . . . . . . . . . . . . . . . . . 19
     
       |
55 | 38, 54 | imbi12d 233 |
. . . . . . . . . . . . . . . . . 18
      
                  |
56 | 55 | spv 1799 |
. . . . . . . . . . . . . . . . 17
                         |
57 | 52, 56 | syl 14 |
. . . . . . . . . . . . . . . 16
 
             |
58 | 57 | ralrimiva 2464 |
. . . . . . . . . . . . . . 15
      
       |
59 | 58 | adantr 272 |
. . . . . . . . . . . . . 14
 
 
            |
60 | 50, 59, 8 | rspcdva 2749 |
. . . . . . . . . . . . 13
 
             |
61 | 60 | imp 123 |
. . . . . . . . . . . 12
               |
62 | 24, 61 | syldan 278 |
. . . . . . . . . . 11
                     
      |
63 | | opexg 4088 |
. . . . . . . . . . 11
                |
64 | 49, 62, 63 | sylancr 408 |
. . . . . . . . . 10
                     
         |
65 | | snidg 3501 |
. . . . . . . . . 10
       
                  |
66 | | elun2 3191 |
. . . . . . . . . 10
                
                    |
67 | 64, 65, 66 | 3syl 17 |
. . . . . . . . 9
                     
                    |
68 | | opeldmg 4682 |
. . . . . . . . . 10
                                        |
69 | 49, 62, 68 | sylancr 408 |
. . . . . . . . 9
                     
                                 |
70 | 67, 69 | mpd 13 |
. . . . . . . 8
                     
             |
71 | | dmeq 4677 |
. . . . . . . . . 10
           
             |
72 | 71 | eleq2d 2169 |
. . . . . . . . 9
                           |
73 | 72 | rspcev 2744 |
. . . . . . . 8
            
            
  |
74 | 48, 70, 73 | syl2anc 406 |
. . . . . . 7
                     

  |
75 | 15, 74 | exlimddv 1837 |
. . . . . 6
 
 
  |
76 | | eliun 3764 |
. . . . . 6
 

  |
77 | 75, 76 | sylibr 133 |
. . . . 5
 
    |
78 | 77 | ex 114 |
. . . 4
  
   |
79 | 78 | ssrdv 3053 |
. . 3

   |
80 | | dmuni 4687 |
. . . 4

  |
81 | 12, 1 | tfrcllemssrecs 6179 |
. . . . 5
  recs    |
82 | | dmss 4676 |
. . . . 5
  recs 
 recs    |
83 | 81, 82 | syl 14 |
. . . 4
  recs    |
84 | 80, 83 | syl5eqssr 3094 |
. . 3
 
recs    |
85 | 79, 84 | sstrd 3057 |
. 2

recs    |
86 | 9 | dmeqi 4678 |
. 2
recs   |
87 | 85, 86 | syl6sseqr 3096 |
1

  |