Proof of Theorem tfr1onlembfn
Step | Hyp | Ref
| Expression |
1 | | tfr1on.f |
. . . . . 6
recs   |
2 | | tfr1on.g |
. . . . . 6
   |
3 | | tfr1on.x |
. . . . . 6
   |
4 | | tfr1on.ex |
. . . . . 6
 

      |
5 | | tfr1onlemsucfn.1 |
. . . . . 6
 
               |
6 | | tfr1onlembacc.3 |
. . . . . 6
 
                 |
7 | | tfr1onlembacc.u |
. . . . . 6
 
 
  |
8 | | tfr1onlembacc.4 |
. . . . . 6
   |
9 | | tfr1onlembacc.5 |
. . . . . 6
     
             |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | tfr1onlembacc 6336 |
. . . . 5

  |
11 | 10 | unissd 3831 |
. . . 4
     |
12 | 5, 3 | tfr1onlemssrecs 6333 |
. . . 4
  recs    |
13 | 11, 12 | sstrd 3165 |
. . 3
  recs    |
14 | | tfrfun 6314 |
. . 3
recs   |
15 | | funss 5230 |
. . 3
  recs   recs      |
16 | 13, 14, 15 | mpisyl 1446 |
. 2
    |
17 | | simpr3 1005 |
. . . . . . . . . . . 12
    
                          |
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 4384 |
. . . . . . . . . . . . . . . . . . 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 | tfr1onlemsucfn 6334 |
. . . . . . . . . . . . . . . . 17
    
                          |
34 | 25, 33 | sylan 283 |
. . . . . . . . . . . . . . . 16
    
                          |
35 | | dffn2 5362 |
. . . . . . . . . . . . . . . 16
           
                 |
36 | 34, 35 | sylib 122 |
. . . . . . . . . . . . . . 15
    
                              |
37 | | fssxp 5378 |
. . . . . . . . . . . . . . 15
                           
   |
38 | 36, 37 | syl 14 |
. . . . . . . . . . . . . 14
    
                        
   |
39 | | ordelon 4379 |
. . . . . . . . . . . . . . . . . . 19
     |
40 | 3, 8, 39 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
   |
41 | | eloni 4371 |
. . . . . . . . . . . . . . . . . 18
   |
42 | 40, 41 | syl 14 |
. . . . . . . . . . . . . . . . 17
   |
43 | 42 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
    
            
  |
44 | | simplr 528 |
. . . . . . . . . . . . . . . 16
    
               |
45 | | ordsucss 4499 |
. . . . . . . . . . . . . . . 16


   |
46 | 43, 44, 45 | sylc 62 |
. . . . . . . . . . . . . . 15
    
            
  |
47 | | xpss1 4732 |
. . . . . . . . . . . . . . 15

      |
48 | 46, 47 | syl 14 |
. . . . . . . . . . . . . 14
    
                   |
49 | 38, 48 | sstrd 3165 |
. . . . . . . . . . . . 13
    
                            |
50 | | vex 2740 |
. . . . . . . . . . . . . . 15
 |
51 | | vex 2740 |
. . . . . . . . . . . . . . . . 17
 |
52 | 18 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
    
               |
53 | 24 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
    
               |
54 | | simpr1 1003 |
. . . . . . . . . . . . . . . . . 18
    
               |
55 | | fneq2 5300 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
56 | 55 | imbi1d 231 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
57 | 56 | albidv 1824 |
. . . . . . . . . . . . . . . . . . . 20
    
                |
58 | 4 | 3expia 1205 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
         |
59 | 58 | alrimiv 1874 |
. . . . . . . . . . . . . . . . . . . . . 22
 
           |
60 | 59 | ralrimiva 2550 |
. . . . . . . . . . . . . . . . . . . . 21
    
       |
61 | 60 | 3ad2ant1 1018 |
. . . . . . . . . . . . . . . . . . . 20
 


          |
62 | | simp2 998 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
63 | 57, 61, 62 | rspcdva 2846 |
. . . . . . . . . . . . . . . . . . 19
 

          |
64 | | simp3 999 |
. . . . . . . . . . . . . . . . . . 19
 

  |
65 | | fneq1 5299 |
. . . . . . . . . . . . . . . . . . . . 21
 
   |
66 | | fveq2 5510 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
67 | 66 | eleq1d 2246 |
. . . . . . . . . . . . . . . . . . . . 21
     
       |
68 | 65, 67 | imbi12d 234 |
. . . . . . . . . . . . . . . . . . . 20
                 |
69 | 68 | spv 1860 |
. . . . . . . . . . . . . . . . . . 19
   
     
       |
70 | 63, 64, 69 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
 

      |
71 | 52, 53, 54, 70 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
    
                   |
72 | | opexg 4224 |
. . . . . . . . . . . . . . . . 17
                |
73 | 51, 71, 72 | sylancr 414 |
. . . . . . . . . . . . . . . 16
    
                      |
74 | | snexg 4181 |
. . . . . . . . . . . . . . . 16
       
           |
75 | 73, 74 | syl 14 |
. . . . . . . . . . . . . . 15
    
                        |
76 | | unexg 4439 |
. . . . . . . . . . . . . . 15
          
              |
77 | 50, 75, 76 | sylancr 414 |
. . . . . . . . . . . . . 14
    
                          |
78 | | elpwg 3582 |
. . . . . . . . . . . . . 14
                         
                 |
79 | 77, 78 | syl 14 |
. . . . . . . . . . . . 13
    
                           
                |
80 | 49, 79 | mpbird 167 |
. . . . . . . . . . . 12
    
                         
   |
81 | 17, 80 | eqeltrd 2254 |
. . . . . . . . . . 11
    
              
   |
82 | 81 | ex 115 |
. . . . . . . . . 10
 
  
           
      |
83 | 82 | exlimdv 1819 |
. . . . . . . . 9
 
                
      |
84 | 83 | rexlimdva 2594 |
. . . . . . . 8
     
           
      |
85 | 84 | abssdv 3229 |
. . . . . . 7
  
                     |
86 | 6, 85 | eqsstrid 3201 |
. . . . . 6

     |
87 | | sspwuni 3968 |
. . . . . 6
   
     |
88 | 86, 87 | sylib 122 |
. . . . 5
      |
89 | | dmss 4821 |
. . . . 5
   
     |
90 | 88, 89 | syl 14 |
. . . 4
      |
91 | | dmxpss 5054 |
. . . 4
   |
92 | 90, 91 | sstrdi 3167 |
. . 3
    |
93 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | tfr1onlembxssdm 6337 |
. . 3

   |
94 | 92, 93 | eqssd 3172 |
. 2
    |
95 | | df-fn 5214 |
. 2
 
  
   |
96 | 16, 94, 95 | sylanbrc 417 |
1
    |