Proof of Theorem tfrcllembfn
Step | Hyp | Ref
| Expression |
1 | | tfrcl.f |
. . . . . . 7
recs   |
2 | | tfrcl.g |
. . . . . . 7
   |
3 | | tfrcl.x |
. . . . . . 7
   |
4 | | tfrcl.ex |
. . . . . . 7
 
           |
5 | | tfrcllemsucfn.1 |
. . . . . . 7
 
                   |
6 | | tfrcllembacc.3 |
. . . . . . 7
 
      
              |
7 | | tfrcllembacc.u |
. . . . . . 7
 
 
  |
8 | | tfrcllembacc.4 |
. . . . . . 7
   |
9 | | tfrcllembacc.5 |
. . . . . . 7
         
             |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | tfrcllembacc 6352 |
. . . . . 6

  |
11 | 10 | unissd 3833 |
. . . . 5
     |
12 | 5, 3 | tfrcllemssrecs 6349 |
. . . . 5
  recs    |
13 | 11, 12 | sstrd 3165 |
. . . 4
  recs    |
14 | | tfrfun 6317 |
. . . 4
recs   |
15 | | funss 5233 |
. . . 4
  recs   recs      |
16 | 13, 14, 15 | mpisyl 1446 |
. . 3
    |
17 | | simpr3 1005 |
. . . . . . . . . . . . 13
        
                          |
18 | | simpl 109 |
. . . . . . . . . . . . . . . . . 18
 
   |
19 | 3 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
 
   |
20 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
21 | 8 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
22 | 20, 21 | jca 306 |
. . . . . . . . . . . . . . . . . . 19
 
 
   |
23 | | ordtr1 4387 |
. . . . . . . . . . . . . . . . . . 19

 
    |
24 | 19, 22, 23 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
 
   |
25 | 18, 24 | jca 306 |
. . . . . . . . . . . . . . . . 17
 
     |
26 | 2 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
        
               |
27 | 3 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
        
               |
28 | 4 | 3adant1r 1231 |
. . . . . . . . . . . . . . . . . . 19
   
           |
29 | 28 | 3adant1r 1231 |
. . . . . . . . . . . . . . . . . 18
   
                              |
30 | | simplr 528 |
. . . . . . . . . . . . . . . . . 18
        
               |
31 | | simpr1 1003 |
. . . . . . . . . . . . . . . . . 18
        
                   |
32 | | simpr2 1004 |
. . . . . . . . . . . . . . . . . 18
        
               |
33 | 1, 26, 27, 29, 5, 30, 31, 32 | tfrcllemsucfn 6350 |
. . . . . . . . . . . . . . . . 17
        
                              |
34 | 25, 33 | sylan 283 |
. . . . . . . . . . . . . . . 16
        
                              |
35 | | fssxp 5381 |
. . . . . . . . . . . . . . . 16
                           
   |
36 | 34, 35 | syl 14 |
. . . . . . . . . . . . . . 15
        
                            |
37 | | ordelon 4382 |
. . . . . . . . . . . . . . . . . . . 20
     |
38 | 3, 8, 37 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
   |
39 | | eloni 4374 |
. . . . . . . . . . . . . . . . . . 19
   |
40 | 38, 39 | syl 14 |
. . . . . . . . . . . . . . . . . 18
   |
41 | 40 | ad2antrr 488 |
. . . . . . . . . . . . . . . . 17
        
               |
42 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
        
               |
43 | | ordsucss 4502 |
. . . . . . . . . . . . . . . . 17


   |
44 | 41, 42, 43 | sylc 62 |
. . . . . . . . . . . . . . . 16
        
               |
45 | | xpss1 4735 |
. . . . . . . . . . . . . . . 16

 
    |
46 | 44, 45 | syl 14 |
. . . . . . . . . . . . . . 15
        
             

    |
47 | 36, 46 | sstrd 3165 |
. . . . . . . . . . . . . 14
        
                            |
48 | | vex 2740 |
. . . . . . . . . . . . . . . 16
 |
49 | | vex 2740 |
. . . . . . . . . . . . . . . . . 18
 |
50 | 18 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
        
               |
51 | 24 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
        
               |
52 | | simpr1 1003 |
. . . . . . . . . . . . . . . . . . 19
        
                   |
53 | | feq2 5347 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
       |
54 | 53 | imbi1d 231 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                  |
55 | 54 | albidv 1824 |
. . . . . . . . . . . . . . . . . . . . 21
             
      
        |
56 | 4 | 3expia 1205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
             |
57 | 56 | alrimiv 1874 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
       
       |
58 | 57 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . . . . . . 22
                |
59 | 58 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . . 21
 
     
      
       |
60 | | simp2 998 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
61 | 55, 59, 60 | rspcdva 2846 |
. . . . . . . . . . . . . . . . . . . 20
 
           
       |
62 | | simp3 999 |
. . . . . . . . . . . . . . . . . . . 20
 
           |
63 | | feq1 5346 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
64 | | fveq2 5513 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
65 | 64 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
66 | 63, 65 | imbi12d 234 |
. . . . . . . . . . . . . . . . . . . . 21
      
                  |
67 | 66 | spv 1860 |
. . . . . . . . . . . . . . . . . . . 20
                         |
68 | 61, 62, 67 | sylc 62 |
. . . . . . . . . . . . . . . . . . 19
 
           |
69 | 50, 51, 52, 68 | syl3anc 1238 |
. . . . . . . . . . . . . . . . . 18
        
                   |
70 | | opexg 4227 |
. . . . . . . . . . . . . . . . . 18
                |
71 | 49, 69, 70 | sylancr 414 |
. . . . . . . . . . . . . . . . 17
        
                      |
72 | | snexg 4183 |
. . . . . . . . . . . . . . . . 17
       
           |
73 | 71, 72 | syl 14 |
. . . . . . . . . . . . . . . 16
        
                        |
74 | | unexg 4442 |
. . . . . . . . . . . . . . . 16
          
              |
75 | 48, 73, 74 | sylancr 414 |
. . . . . . . . . . . . . . 15
        
                          |
76 | | elpwg 3583 |
. . . . . . . . . . . . . . 15
                         
                 |
77 | 75, 76 | syl 14 |
. . . . . . . . . . . . . 14
        
                          
                 |
78 | 47, 77 | mpbird 167 |
. . . . . . . . . . . . 13
        
                             |
79 | 17, 78 | eqeltrd 2254 |
. . . . . . . . . . . 12
        
                  |
80 | 79 | ex 115 |
. . . . . . . . . . 11
 
                  
      |
81 | 80 | exlimdv 1819 |
. . . . . . . . . 10
 
        
           
      |
82 | 81 | rexlimdva 2594 |
. . . . . . . . 9
         
           
      |
83 | 82 | abssdv 3229 |
. . . . . . . 8
  
      
                  |
84 | 6, 83 | eqsstrid 3201 |
. . . . . . 7

     |
85 | | sspwuni 3970 |
. . . . . . 7
   
 
   |
86 | 84, 85 | sylib 122 |
. . . . . 6
      |
87 | | dmss 4824 |
. . . . . 6
    
    |
88 | 86, 87 | syl 14 |
. . . . 5
      |
89 | | dmxpss 5057 |
. . . . 5
   |
90 | 88, 89 | sstrdi 3167 |
. . . 4
    |
91 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | tfrcllembxssdm 6353 |
. . . 4

   |
92 | 90, 91 | eqssd 3172 |
. . 3
    |
93 | | df-fn 5217 |
. . 3
 
  
   |
94 | 16, 92, 93 | sylanbrc 417 |
. 2
    |
95 | | rnss 4855 |
. . . 4
    
    |
96 | 86, 95 | syl 14 |
. . 3
      |
97 | | rnxpss 5058 |
. . 3
   |
98 | 96, 97 | sstrdi 3167 |
. 2
    |
99 | | df-f 5218 |
. 2
     
 
    |
100 | 94, 98, 99 | sylanbrc 417 |
1
        |