Step | Hyp | Ref
| Expression |
1 | | cvmlift2.f |
. . 3
  CovMap    |
2 | | cvmlift2.g |
. . . . 5
  
    |
3 | | iitop 21990 |
. . . . . . 7
 |
4 | | iiuni 21991 |
. . . . . . 7
  ![[,] [,]](_icc.gif)    |
5 | 3, 3, 4, 4 | txunii 20685 |
. . . . . 6
   ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)       |
6 | | eqid 2471 |
. . . . . 6
   |
7 | 5, 6 | cnf 20339 |
. . . . 5
          ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        |
8 | 2, 7 | syl 17 |
. . . 4
      ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        |
9 | | cvmlift2lem10.1 |
. . . . 5
   ![[,] [,]](_icc.gif)    |
10 | | cvmlift2lem10.2 |
. . . . 5
   ![[,] [,]](_icc.gif)    |
11 | | opelxpi 4871 |
. . . . 5
    ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
12 | 9, 10, 11 | syl2anc 673 |
. . . 4
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
13 | 8, 12 | ffvelrnd 6038 |
. . 3
           |
14 | | cvmlift2lem10.s |
. . . 4
                       
    ↾t    
↾t        |
15 | 14, 6 | cvmcov 30058 |
. . 3
   CovMap           
               |
16 | 1, 13, 15 | syl2anc 673 |
. 2
                 |
17 | | n0 3732 |
. . . . 5
            |
18 | 12 | adantr 472 |
. . . . . . . . . . 11
 
       
            ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
19 | | simprl 772 |
. . . . . . . . . . 11
 
       
               |
20 | 8 | adantr 472 |
. . . . . . . . . . . 12
 
       
           ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)        |
21 | | ffn 5739 |
. . . . . . . . . . . 12
      ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     |
22 | | elpreima 6017 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)           
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)              |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . . . . 11
 
       
              
       ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)              |
24 | 18, 19, 23 | mpbir2and 936 |
. . . . . . . . . 10
 
       
                |
25 | 2 | adantr 472 |
. . . . . . . . . . . 12
 
       
        
   |
26 | 14 | cvmsrcl 30059 |
. . . . . . . . . . . . 13
       |
27 | 26 | ad2antll 743 |
. . . . . . . . . . . 12
 
       
        |
28 | | cnima 20358 |
. . . . . . . . . . . 12
   
            |
29 | 25, 27, 28 | syl2anc 673 |
. . . . . . . . . . 11
 
       
               |
30 | | eltx 20660 |
. . . . . . . . . . . 12
         
         
              |
31 | 3, 3, 30 | mp2an 686 |
. . . . . . . . . . 11
       
        
             |
32 | 29, 31 | sylib 201 |
. . . . . . . . . 10
 
       
                 
          |
33 | | eleq1 2537 |
. . . . . . . . . . . . . 14
               |
34 | | opelxp 4869 |
. . . . . . . . . . . . . 14
  
       |
35 | 33, 34 | syl6bb 269 |
. . . . . . . . . . . . 13
            |
36 | 35 | anbi1d 719 |
. . . . . . . . . . . 12
               
 
  
         |
37 | 36 | 2rexbidv 2897 |
. . . . . . . . . . 11
         
         
              |
38 | 37 | rspcv 3132 |
. . . . . . . . . 10
  
       
       
          
                |
39 | 24, 32, 38 | sylc 61 |
. . . . . . . . 9
 
       
                     |
40 | | iillyscon 30048 |
. . . . . . . . . . . . . 14
Locally SCon |
41 | 40 | a1i 11 |
. . . . . . . . . . . . 13
                  
              Locally SCon |
42 | | simplrl 778 |
. . . . . . . . . . . . 13
                  
                |
43 | | simprll 780 |
. . . . . . . . . . . . 13
                  
                |
44 | | llyi 20566 |
. . . . . . . . . . . . 13
  Locally
SCon    
↾t  SCon  |
45 | 41, 42, 43, 44 | syl3anc 1292 |
. . . . . . . . . . . 12
                  
                
↾t  SCon  |
46 | | simplrr 779 |
. . . . . . . . . . . . 13
                  
                |
47 | | simprlr 781 |
. . . . . . . . . . . . 13
                  
                |
48 | | llyi 20566 |
. . . . . . . . . . . . 13
  Locally
SCon     ↾t  SCon  |
49 | 41, 46, 47, 48 | syl3anc 1292 |
. . . . . . . . . . . 12
                  
                 ↾t  SCon  |
50 | | reeanv 2944 |
. . . . . . . . . . . . 13
  
 

↾t  SCon 

↾t  SCon
 


↾t  SCon  

↾t  SCon   |
51 | | simpl2 1034 |
. . . . . . . . . . . . . . . . . 18
  

↾t  SCon 

↾t  SCon   |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . 17
                  
                 
↾t  SCon 

↾t  SCon    |
53 | | simpr2 1037 |
. . . . . . . . . . . . . . . . . 18
  

↾t  SCon 

↾t  SCon   |
54 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . 17
                  
                 
↾t  SCon 

↾t  SCon    |
55 | | simprl1 1075 |
. . . . . . . . . . . . . . . . . . . 20
                   
               

↾t  SCon 

↾t  SCon    |
56 | | simprr1 1078 |
. . . . . . . . . . . . . . . . . . . 20
                   
               

↾t  SCon 

↾t  SCon 
  |
57 | | xpss12 4945 |
. . . . . . . . . . . . . . . . . . . 20
 
  
    |
58 | 55, 56, 57 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
                   
               

↾t  SCon 

↾t  SCon   
    |
59 | | simplrr 779 |
. . . . . . . . . . . . . . . . . . 19
                   
               

↾t  SCon 

↾t  SCon   
       |
60 | 58, 59 | sstrd 3428 |
. . . . . . . . . . . . . . . . . 18
                   
               

↾t  SCon 

↾t  SCon   
       |
61 | 60 | ex 441 |
. . . . . . . . . . . . . . . . 17
                  
                 
↾t  SCon 

↾t  SCon           |
62 | 52, 54, 61 | 3jcad 1211 |
. . . . . . . . . . . . . . . 16
                  
                 
↾t  SCon 

↾t  SCon 


         |
63 | | simp3 1032 |
. . . . . . . . . . . . . . . . . 18
 

↾t  SCon 
↾t  SCon |
64 | | simp3 1032 |
. . . . . . . . . . . . . . . . . 18
 

↾t  SCon
 ↾t 
SCon |
65 | 63, 64 | anim12i 576 |
. . . . . . . . . . . . . . . . 17
  

↾t  SCon 

↾t  SCon  
↾t  SCon 
↾t  SCon  |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
                  
                 
↾t  SCon 

↾t  SCon  
↾t  SCon 
↾t  SCon   |
67 | 62, 66 | jcad 542 |
. . . . . . . . . . . . . . 15
                  
                 
↾t  SCon 

↾t  SCon  
 
        ↾t  SCon  ↾t  SCon    |
68 | 67 | reximdv 2857 |
. . . . . . . . . . . . . 14
                  
               
  
↾t  SCon 

↾t  SCon   
          ↾t  SCon
 ↾t 
SCon    |
69 | 68 | reximdv 2857 |
. . . . . . . . . . . . 13
                  
               

  
↾t  SCon 

↾t  SCon    
          ↾t  SCon
 ↾t 
SCon    |
70 | 50, 69 | syl5bir 226 |
. . . . . . . . . . . 12
                  
                  
↾t  SCon  

↾t  SCon    
          ↾t  SCon
 ↾t 
SCon    |
71 | 45, 49, 70 | mp2and 693 |
. . . . . . . . . . 11
                  
                 
          ↾t  SCon
 ↾t 
SCon   |
72 | 71 | ex 441 |
. . . . . . . . . 10
          
      
              

            ↾t  SCon 
↾t  SCon    |
73 | 72 | rexlimdvva 2878 |
. . . . . . . . 9
 
       
       

           

            ↾t  SCon 
↾t  SCon    |
74 | 39, 73 | mpd 15 |
. . . . . . . 8
 
       
         
          ↾t  SCon
 ↾t 
SCon   |
75 | | simp3l1 1135 |
. . . . . . . . . . . . 13
          
      
  
          ↾t  SCon
 ↾t 
SCon 
  |
76 | | simp3l2 1136 |
. . . . . . . . . . . . 13
          
      
  
          ↾t  SCon
 ↾t 
SCon 
  |
77 | | cvmlift2.b |
. . . . . . . . . . . . . . 15
  |
78 | | simpl1l 1081 |
. . . . . . . . . . . . . . . 16
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
         |
79 | 78, 1 | syl 17 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
        CovMap    |
80 | 78, 2 | syl 17 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
             |
81 | | cvmlift2.p |
. . . . . . . . . . . . . . . 16
   |
82 | 78, 81 | syl 17 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
         |
83 | | cvmlift2.i |
. . . . . . . . . . . . . . . 16
           |
84 | 78, 83 | syl 17 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
                 |
85 | | cvmlift2.h |
. . . . . . . . . . . . . . 15
           ![[,] [,]](_icc.gif)              |
86 | | cvmlift2.k |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)                      |
87 | | df-ov 6311 |
. . . . . . . . . . . . . . . 16
            |
88 | | simpl1r 1082 |
. . . . . . . . . . . . . . . . 17
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
              
       |
89 | 88 | simpld 466 |
. . . . . . . . . . . . . . . 16
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
                |
90 | 87, 89 | syl5eqel 2553 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
             |
91 | 88 | simprd 470 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
             |
92 | | simpl2l 1083 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
         |
93 | | simpl2r 1084 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
         |
94 | | simp3rl 1103 |
. . . . . . . . . . . . . . . . 17
          
      
  
          ↾t  SCon
 ↾t 
SCon 
 ↾t 
SCon |
95 | 94 | adantr 472 |
. . . . . . . . . . . . . . . 16
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
        ↾t  SCon |
96 | | sconpcon 30022 |
. . . . . . . . . . . . . . . 16
  ↾t  SCon  ↾t  PCon |
97 | | pconcon 30026 |
. . . . . . . . . . . . . . . 16
  ↾t  PCon  ↾t    |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
        ↾t    |
99 | | simp3rr 1104 |
. . . . . . . . . . . . . . . . 17
          
      
  
          ↾t  SCon
 ↾t 
SCon 
 ↾t 
SCon |
100 | 99 | adantr 472 |
. . . . . . . . . . . . . . . 16
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
        ↾t  SCon |
101 | | sconpcon 30022 |
. . . . . . . . . . . . . . . 16
  ↾t  SCon  ↾t  PCon |
102 | | pconcon 30026 |
. . . . . . . . . . . . . . . 16
  ↾t  PCon  ↾t    |
103 | 100, 101,
102 | 3syl 18 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
        ↾t    |
104 | 75 | adantr 472 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
         |
105 | 76 | adantr 472 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
         |
106 | | simp3l3 1137 |
. . . . . . . . . . . . . . . 16
          
      
  
          ↾t  SCon
 ↾t 
SCon 
         |
107 | 106 | adantr 472 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
                |
108 | | simprl 772 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
         |
109 | | simprr 774 |
. . . . . . . . . . . . . . 15
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
        
        ↾t         |
110 | | eqid 2471 |
. . . . . . . . . . . . . . 15
        
      |
111 | 77, 79, 80, 82, 84, 85, 86, 14, 90, 91, 92, 93, 98, 103, 104, 105, 107, 108, 109, 110 | cvmlift2lem9 30106 |
. . . . . . . . . . . . . 14
                  
  
          ↾t  SCon
 ↾t 
SCon 

          ↾t 
        
     
↾t       |
112 | 111 | rexlimdvaa 2872 |
. . . . . . . . . . . . 13
          
      
  
          ↾t  SCon
 ↾t 
SCon 
 
          ↾t 
             ↾t        |
113 | 75, 76, 112 | 3jca 1210 |
. . . . . . . . . . . 12
          
      
  
          ↾t  SCon
 ↾t 
SCon 

  
         ↾t 
             ↾t         |
114 | 113 | 3expia 1233 |
. . . . . . . . . . 11
          
      
               ↾t  SCon 
↾t  SCon 
            ↾t      
       
↾t          |
115 | 114 | anassrs 660 |
. . . . . . . . . 10
                 

   


        ↾t  SCon  ↾t  SCon

  
         ↾t 
             ↾t          |
116 | 115 | reximdva 2858 |
. . . . . . . . 9
          
     
    
          ↾t  SCon
 ↾t 
SCon  
   
        ↾t      
       
↾t          |
117 | 116 | reximdva 2858 |
. . . . . . . 8
 
       
       

            ↾t  SCon 
↾t  SCon      
         ↾t 
             ↾t          |
118 | 74, 117 | mpd 15 |
. . . . . . 7
 
       
           
         ↾t 
             ↾t         |
119 | 118 | expr 626 |
. . . . . 6
 
            
     
         ↾t 
             ↾t          |
120 | 119 | exlimdv 1787 |
. . . . 5
 
              


   
        ↾t      
       
↾t          |
121 | 17, 120 | syl5bi 225 |
. . . 4
 
              

   
        ↾t      
       
↾t          |
122 | 121 | expimpd 614 |
. . 3
                    
         ↾t 
             ↾t          |
123 | 122 | rexlimdvw 2874 |
. 2
                     
         ↾t 
             ↾t          |
124 | 16, 123 | mpd 15 |
1
  

   
        ↾t      
       
↾t         |