Step | Hyp | Ref
| Expression |
1 | | simpl 443 |
. . 3
  NC  ↑c
0c
NC NC  |
2 | | snex 4112 |
. . . . 5
 
 |
3 | | fvex 5340 |
. . . . 5
Spac  2c ↑c  
 |
4 | 2, 3 | unex 4107 |
. . . 4
   Spac  2c ↑c     |
5 | 4 | a1i 10 |
. . 3
  NC  ↑c
0c
NC    Spac  2c ↑c      |
6 | | snidg 3759 |
. . . . 5
 NC     |
7 | 6 | adantr 451 |
. . . 4
  NC  ↑c
0c
NC     |
8 | | elun1 3431 |
. . . 4
      Spac  2c ↑c      |
9 | 7, 8 | syl 15 |
. . 3
  NC  ↑c
0c
NC    Spac  2c
↑c      |
10 | | elun 3221 |
. . . . . . . . . 10
    Spac  2c ↑c      
Spac  2c ↑c      |
11 | | elsn 3749 |
. . . . . . . . . . 11
  
  |
12 | 11 | orbi1i 506 |
. . . . . . . . . 10
    Spac
 2c
↑c    
Spac  2c ↑c      |
13 | 10, 12 | bitri 240 |
. . . . . . . . 9
    Spac  2c ↑c    
Spac  2c ↑c      |
14 | | spacssnc 6285 |
. . . . . . . . . . . . . . 15
 NC Spac  
NC  |
15 | 14 | adantr 451 |
. . . . . . . . . . . . . 14
  NC  ↑c
0c
NC Spac   NC  |
16 | | spacid 6286 |
. . . . . . . . . . . . . . . 16
 NC Spac     |
17 | 16 | adantr 451 |
. . . . . . . . . . . . . . 15
  NC  ↑c
0c
NC Spac     |
18 | | simpr 447 |
. . . . . . . . . . . . . . 15
  NC  ↑c
0c
NC  ↑c
0c
NC  |
19 | | spaccl 6287 |
. . . . . . . . . . . . . . 15
  NC Spac
  
↑c 0c NC 2c ↑c 
Spac     |
20 | 1, 17, 18, 19 | syl3anc 1182 |
. . . . . . . . . . . . . 14
  NC  ↑c
0c
NC 2c
↑c  Spac
    |
21 | 15, 20 | sseldd 3275 |
. . . . . . . . . . . . 13
  NC  ↑c
0c
NC 2c
↑c  NC  |
22 | | spacid 6286 |
. . . . . . . . . . . . 13
 2c ↑c
 NC 2c ↑c  Spac  2c ↑c     |
23 | 21, 22 | syl 15 |
. . . . . . . . . . . 12
  NC  ↑c
0c
NC 2c
↑c  Spac
 2c
↑c     |
24 | | oveq2 5532 |
. . . . . . . . . . . . 13
 2c
↑c  2c ↑c
   |
25 | 24 | eleq1d 2419 |
. . . . . . . . . . . 12
  2c ↑c  Spac  2c ↑c  
2c
↑c  Spac
 2c
↑c      |
26 | 23, 25 | syl5ibrcom 213 |
. . . . . . . . . . 11
  NC  ↑c
0c
NC  2c
↑c  Spac
 2c
↑c      |
27 | 26 | adantr 451 |
. . . . . . . . . 10
   NC  ↑c
0c
NC  ↑c
0c
NC  2c
↑c  Spac
 2c
↑c      |
28 | | 2nnc 6168 |
. . . . . . . . . . . . . 14
2c
Nn |
29 | | ceclnn1 6190 |
. . . . . . . . . . . . . 14
 2c Nn NC 
↑c 0c NC 2c ↑c 
NC  |
30 | 28, 29 | mp3an1 1264 |
. . . . . . . . . . . . 13
  NC  ↑c
0c
NC 2c
↑c  NC  |
31 | 30 | adantr 451 |
. . . . . . . . . . . 12
   NC  ↑c
0c
NC   ↑c 0c NC
Spac  2c ↑c     2c ↑c  NC  |
32 | | simprr 733 |
. . . . . . . . . . . 12
   NC  ↑c
0c
NC   ↑c 0c NC
Spac  2c ↑c    
Spac  2c ↑c     |
33 | | simprl 732 |
. . . . . . . . . . . 12
   NC  ↑c
0c
NC   ↑c 0c NC
Spac  2c ↑c     
↑c 0c NC  |
34 | | spaccl 6287 |
. . . . . . . . . . . 12
  2c ↑c 
NC
Spac  2c ↑c  
 ↑c 0c NC 2c ↑c  Spac  2c ↑c     |
35 | 31, 32, 33, 34 | syl3anc 1182 |
. . . . . . . . . . 11
   NC  ↑c
0c
NC   ↑c 0c NC
Spac  2c ↑c     2c ↑c  Spac  2c ↑c     |
36 | 35 | expr 598 |
. . . . . . . . . 10
   NC  ↑c
0c
NC  ↑c
0c
NC  Spac  2c ↑c  
2c
↑c  Spac
 2c
↑c      |
37 | 27, 36 | jaod 369 |
. . . . . . . . 9
   NC  ↑c
0c
NC  ↑c
0c
NC  
Spac  2c ↑c    2c
↑c  Spac
 2c
↑c      |
38 | 13, 37 | syl5bi 208 |
. . . . . . . 8
   NC  ↑c
0c
NC  ↑c
0c
NC     Spac  2c ↑c    2c
↑c  Spac
 2c
↑c      |
39 | 38 | ex 423 |
. . . . . . 7
  NC  ↑c
0c
NC   ↑c 0c NC 
   Spac  2c ↑c    2c
↑c  Spac
 2c
↑c       |
40 | 39 | com23 72 |
. . . . . 6
  NC  ↑c
0c
NC     Spac  2c ↑c     
↑c 0c NC 2c ↑c 
Spac  2c ↑c       |
41 | 40 | imp3a 420 |
. . . . 5
  NC  ↑c
0c
NC      Spac  2c ↑c     ↑c 0c NC 2c ↑c  Spac  2c ↑c      |
42 | | elun2 3432 |
. . . . 5
 2c ↑c

Spac  2c ↑c  
2c
↑c     Spac  2c
↑c      |
43 | 41, 42 | syl6 29 |
. . . 4
  NC  ↑c
0c
NC      Spac  2c ↑c     ↑c 0c NC 2c ↑c     Spac  2c ↑c       |
44 | 43 | ralrimivw 2699 |
. . 3
  NC  ↑c
0c
NC 
Spac         Spac  2c ↑c     ↑c 0c NC 2c ↑c     Spac  2c ↑c       |
45 | | spacind 6288 |
. . 3
   NC    Spac  2c ↑c         Spac  2c
↑c     Spac
       
Spac  2c ↑c     ↑c 0c NC 2c ↑c     Spac  2c ↑c       Spac      Spac  2c ↑c      |
46 | 1, 5, 9, 44, 45 | syl22anc 1183 |
. 2
  NC  ↑c
0c
NC Spac      Spac  2c ↑c      |
47 | 16 | snssd 3854 |
. . . 4
 NC   Spac     |
48 | 47 | adantr 451 |
. . 3
  NC  ↑c
0c
NC   Spac     |
49 | | fvex 5340 |
. . . . 5
Spac    |
50 | 49 | a1i 10 |
. . . 4
  NC  ↑c
0c
NC Spac     |
51 | | spaccl 6287 |
. . . . . . 7
  NC Spac
  
↑c 0c NC 2c ↑c 
Spac     |
52 | 51 | 3expib 1154 |
. . . . . 6
 NC   Spac  
 ↑c 0c NC 2c ↑c  Spac      |
53 | 52 | adantr 451 |
. . . . 5
  NC  ↑c
0c
NC   Spac    ↑c 0c NC 2c ↑c  Spac      |
54 | 53 | ralrimivw 2699 |
. . . 4
  NC  ↑c
0c
NC 
Spac  2c ↑c      Spac    ↑c 0c NC 2c ↑c  Spac      |
55 | | spacind 6288 |
. . . 4
   2c ↑c 
NC
Spac     2c
↑c  Spac
   Spac
 2c
↑c      Spac
  
↑c 0c NC 2c ↑c 
Spac      Spac  2c ↑c  
Spac     |
56 | 21, 50, 20, 54, 55 | syl22anc 1183 |
. . 3
  NC  ↑c
0c
NC Spac  2c ↑c  
Spac     |
57 | 48, 56 | unssd 3440 |
. 2
  NC  ↑c
0c
NC    Spac  2c ↑c    Spac     |
58 | 46, 57 | eqssd 3290 |
1
  NC  ↑c
0c
NC Spac      Spac  2c
↑c      |