Proof of Theorem tfr1onlembxssdm
Step | Hyp | Ref
| Expression |
1 | | tfr1onlembacc.5 |
. . 3
     
             |
2 | | simp1 997 |
. . . . . . . 8
 
 
           
  |
3 | | simp2 998 |
. . . . . . . . 9
 
 
           
  |
4 | | tfr1onlembacc.4 |
. . . . . . . . . 10
   |
5 | 2, 4 | syl 14 |
. . . . . . . . 9
 
 
           
  |
6 | | tfr1on.x |
. . . . . . . . . . 11
   |
7 | | ordtr1 4385 |
. . . . . . . . . . 11

 
    |
8 | 6, 7 | syl 14 |
. . . . . . . . . 10
       |
9 | 8 | imp 124 |
. . . . . . . . 9
 

    |
10 | 2, 3, 5, 9 | syl12anc 1236 |
. . . . . . . 8
 
 
           
  |
11 | | simp3l 1025 |
. . . . . . . 8
 
 
           
  |
12 | | fneq2 5301 |
. . . . . . . . . . . . 13
 
   |
13 | 12 | imbi1d 231 |
. . . . . . . . . . . 12
                 |
14 | 13 | albidv 1824 |
. . . . . . . . . . 11
    
                |
15 | | tfr1on.ex |
. . . . . . . . . . . . . . 15
 

      |
16 | 15 | 3expia 1205 |
. . . . . . . . . . . . . 14
 
         |
17 | 16 | alrimiv 1874 |
. . . . . . . . . . . . 13
 
           |
18 | 17 | ralrimiva 2550 |
. . . . . . . . . . . 12
    
       |
19 | 18 | adantr 276 |
. . . . . . . . . . 11
 
 
          |
20 | | simpr 110 |
. . . . . . . . . . 11
 
   |
21 | 14, 19, 20 | rspcdva 2846 |
. . . . . . . . . 10
 
           |
22 | | fneq1 5300 |
. . . . . . . . . . . 12
 
   |
23 | | fveq2 5511 |
. . . . . . . . . . . . 13
           |
24 | 23 | eleq1d 2246 |
. . . . . . . . . . . 12
     
       |
25 | 22, 24 | imbi12d 234 |
. . . . . . . . . . 11
                 |
26 | 25 | spv 1860 |
. . . . . . . . . 10
   
     
       |
27 | 21, 26 | syl 14 |
. . . . . . . . 9
 
         |
28 | 27 | imp 124 |
. . . . . . . 8
           |
29 | 2, 10, 11, 28 | syl21anc 1237 |
. . . . . . 7
 
 
           
      |
30 | | vex 2740 |
. . . . . . . . . 10
 |
31 | | opexg 4225 |
. . . . . . . . . 10
                |
32 | 30, 29, 31 | sylancr 414 |
. . . . . . . . 9
 
 
           
         |
33 | | snidg 3620 |
. . . . . . . . 9
       
                  |
34 | | elun2 3303 |
. . . . . . . . 9
                
                    |
35 | 32, 33, 34 | 3syl 17 |
. . . . . . . 8
 
 
           
                    |
36 | | simp3r 1026 |
. . . . . . . . . . . 12
 
 
           

            |
37 | | rspe 2526 |
. . . . . . . . . . . 12
               



             |
38 | 10, 11, 36, 37 | syl12anc 1236 |
. . . . . . . . . . 11
 
 
           



             |
39 | | vex 2740 |
. . . . . . . . . . . 12
 |
40 | | tfr1onlemsucfn.1 |
. . . . . . . . . . . . 13
 
               |
41 | 40 | tfr1onlem3ag 6332 |
. . . . . . . . . . . 12
 



              |
42 | 39, 41 | ax-mp 5 |
. . . . . . . . . . 11




             |
43 | 38, 42 | sylibr 134 |
. . . . . . . . . 10
 
 
           
  |
44 | 3, 11, 43 | 3jca 1177 |
. . . . . . . . 9
 
 
           

   |
45 | | snexg 4181 |
. . . . . . . . . . 11
       
           |
46 | | unexg 4440 |
. . . . . . . . . . . 12
          
              |
47 | 39, 46 | mpan 424 |
. . . . . . . . . . 11
         
             |
48 | 32, 45, 47 | 3syl 17 |
. . . . . . . . . 10
 
 
           
             |
49 | | isset 2743 |
. . . . . . . . . 10
           

             |
50 | 48, 49 | sylib 122 |
. . . . . . . . 9
 
 
           

             |
51 | | simpr3 1005 |
. . . . . . . . . . . . 13
  
                          |
52 | | 19.8a 1590 |
. . . . . . . . . . . . . 14
 
                             |
53 | | rspe 2526 |
. . . . . . . . . . . . . . 15
                                    |
54 | | tfr1onlembacc.3 |
. . . . . . . . . . . . . . . 16
 
                 |
55 | 54 | abeq2i 2288 |
. . . . . . . . . . . . . . 15


  
              |
56 | 53, 55 | sylibr 134 |
. . . . . . . . . . . . . 14
                    |
57 | 52, 56 | sylan2 286 |
. . . . . . . . . . . . 13
  
               |
58 | 51, 57 | eqeltrrd 2255 |
. . . . . . . . . . . 12
  
                          |
59 | 58 | 3exp2 1225 |
. . . . . . . . . . 11
                               |
60 | 59 | 3imp 1193 |
. . . . . . . . . 10
 
                           |
61 | 60 | exlimdv 1819 |
. . . . . . . . 9
 
                            |
62 | 44, 50, 61 | sylc 62 |
. . . . . . . 8
 
 
           
             |
63 | | elunii 3812 |
. . . . . . . 8
                                          |
64 | 35, 62, 63 | syl2anc 411 |
. . . . . . 7
 
 
           
          |
65 | | opeq2 3777 |
. . . . . . . . . 10
       
         |
66 | 65 | eleq1d 2246 |
. . . . . . . . 9
         
           |
67 | 66 | spcegv 2825 |
. . . . . . . 8
                       |
68 | 30 | eldm2 4821 |
. . . . . . . 8
          |
69 | 67, 68 | syl6ibr 162 |
. . . . . . 7
                  |
70 | 29, 64, 69 | sylc 62 |
. . . . . 6
 
 
           
   |
71 | 70 | 3expia 1205 |
. . . . 5
 
                   |
72 | 71 | exlimdv 1819 |
. . . 4
 
     
               |
73 | 72 | ralimdva 2544 |
. . 3
                  
    |
74 | 1, 73 | mpd 13 |
. 2
 
   |
75 | | dfss3 3145 |
. 2



   |
76 | 74, 75 | sylibr 134 |
1

   |