Step | Hyp | Ref
| Expression |
1 | | brltc 6115 |
. . . . 5
Nc 1c c Nc 1c c Nc
1c    |
2 | 1 | simplbi 446 |
. . . 4
Nc 1c c Nc 1c
c   |
3 | | 1cex 4143 |
. . . . . . . 8
1c
 |
4 | 3 | ncelncsi 6122 |
. . . . . . 7
Nc 1c NC |
5 | | tlecg 6231 |
. . . . . . 7
 Nc
1c
NC NC Nc 1c c Tc Nc 1c c Tc    |
6 | 4, 5 | mpan 651 |
. . . . . 6
 NC Nc 1c c Tc Nc
1c c Tc    |
7 | 6 | adantl 452 |
. . . . 5
 c We NC NC Nc 1c c Tc Nc 1c c Tc    |
8 | | tcnc1c 6228 |
. . . . . . 7
Tc Nc
1c
Nc 1 1c |
9 | 8 | breq1i 4647 |
. . . . . 6
Tc Nc
1c c Tc Nc 1 1c c Tc   |
10 | | tccl 6161 |
. . . . . . . . 9
 NC Tc NC  |
11 | | te0c 6238 |
. . . . . . . . 9
 NC Tc ↑c
0c
NC  |
12 | 3 | pw1ex 4304 |
. . . . . . . . . . 11
1
1c
 |
13 | 12 | ncelncsi 6122 |
. . . . . . . . . 10
Nc 1 1c NC |
14 | | ce2le 6234 |
. . . . . . . . . . 11
  Nc 1 1c NC Tc NC Tc ↑c
0c
NC Nc 1 1c c Tc 
2c
↑c Nc 1 1c c 2c ↑c
Tc    |
15 | 14 | ex 423 |
. . . . . . . . . 10
 Nc 1
1c
NC Tc NC Tc ↑c 0c NC Nc 1 1c c Tc 2c ↑c Nc 1 1c c 2c ↑c Tc     |
16 | 13, 15 | mp3an1 1264 |
. . . . . . . . 9
 Tc NC Tc ↑c 0c NC Nc 1 1c c Tc 2c ↑c Nc 1 1c c 2c ↑c Tc     |
17 | 10, 11, 16 | syl2anc 642 |
. . . . . . . 8
 NC Nc 1 1c c Tc 2c ↑c Nc 1 1c c 2c ↑c Tc     |
18 | 17 | adantl 452 |
. . . . . . 7
 c We NC NC Nc 1 1c c Tc 2c ↑c Nc 1 1c c 2c ↑c Tc     |
19 | | ce2ncpw11c 6195 |
. . . . . . . . 9
2c
↑c Nc 1 1c Nc
1c |
20 | 19 | breq1i 4647 |
. . . . . . . 8
 2c ↑c
Nc 1 1c c 2c ↑c Tc 
Nc 1c c 2c ↑c
Tc    |
21 | | orc 374 |
. . . . . . . . . 10
Nc 1c c 2c ↑c
Tc  Nc 1c c 2c ↑c
Tc  Nc 1c 2c ↑c Tc     |
22 | | brltc 6115 |
. . . . . . . . . . . 12
Nc 1c c 2c ↑c Tc 
Nc 1c c 2c ↑c
Tc  Nc 1c 2c ↑c Tc     |
23 | 22 | orbi1i 506 |
. . . . . . . . . . 11
 Nc
1c c 2c ↑c Tc 
Nc 1c 2c ↑c Tc    Nc
1c c 2c ↑c Tc 
Nc 1c 2c ↑c Tc   Nc 1c 2c ↑c Tc     |
24 | | pm2.1 406 |
. . . . . . . . . . . . 13
 Nc
1c
2c
↑c Tc  Nc 1c 2c ↑c
Tc    |
25 | | df-ne 2519 |
. . . . . . . . . . . . . 14
Nc 1c 2c ↑c Tc 
Nc 1c 2c ↑c Tc    |
26 | 25 | orbi1i 506 |
. . . . . . . . . . . . 13
 Nc
1c 2c ↑c Tc 
Nc 1c 2c ↑c Tc    Nc
1c
2c
↑c Tc  Nc 1c 2c ↑c
Tc     |
27 | 24, 26 | mpbir 200 |
. . . . . . . . . . . 12
Nc 1c 2c ↑c Tc 
Nc 1c 2c ↑c Tc    |
28 | | ordir 835 |
. . . . . . . . . . . 12
  Nc 1c c 2c
↑c Tc  Nc 1c 2c
↑c Tc   Nc 1c 2c ↑c Tc    Nc
1c c 2c ↑c Tc 
Nc 1c 2c ↑c Tc   Nc
1c 2c ↑c Tc 
Nc 1c 2c ↑c Tc      |
29 | 27, 28 | mpbiran2 885 |
. . . . . . . . . . 11
  Nc 1c c 2c
↑c Tc  Nc 1c 2c
↑c Tc   Nc 1c 2c ↑c Tc   Nc 1c c 2c ↑c
Tc  Nc 1c 2c ↑c Tc     |
30 | 23, 29 | bitri 240 |
. . . . . . . . . 10
 Nc
1c c 2c ↑c Tc 
Nc 1c 2c ↑c Tc   Nc 1c c 2c ↑c
Tc  Nc 1c 2c ↑c Tc     |
31 | 21, 30 | sylibr 203 |
. . . . . . . . 9
Nc 1c c 2c ↑c
Tc  Nc 1c c 2c ↑c Tc 
Nc 1c 2c ↑c Tc     |
32 | | ce2t 6236 |
. . . . . . . . . . . 12
 NC 2c ↑c Tc 
NC  |
33 | | nchoicelem8 6297 |
. . . . . . . . . . . 12
 c We NC 2c ↑c Tc 
NC   2c ↑c Tc 
↑c 0c NC Nc
1c c 2c ↑c Tc     |
34 | 32, 33 | sylan2 460 |
. . . . . . . . . . 11
 c We NC NC   2c ↑c Tc 
↑c 0c NC Nc
1c c 2c ↑c Tc     |
35 | | nchoicelem3 6292 |
. . . . . . . . . . . . . . . 16
  2c ↑c Tc 
NC  2c ↑c
Tc  ↑c 0c NC Spac  2c ↑c Tc    2c ↑c Tc     |
36 | 35 | nceqd 6111 |
. . . . . . . . . . . . . . 15
  2c ↑c Tc 
NC  2c ↑c
Tc  ↑c 0c NC Nc Spac  2c ↑c Tc   Nc  2c ↑c Tc     |
37 | | ovex 5552 |
. . . . . . . . . . . . . . . 16
2c
↑c Tc   |
38 | 37 | df1c3 6141 |
. . . . . . . . . . . . . . 15
1c
Nc  2c ↑c Tc    |
39 | 36, 38 | syl6eqr 2403 |
. . . . . . . . . . . . . 14
  2c ↑c Tc 
NC  2c ↑c
Tc  ↑c 0c NC Nc Spac  2c ↑c Tc   1c |
40 | 39 | ex 423 |
. . . . . . . . . . . . 13
 2c ↑c
Tc  NC   2c ↑c Tc 
↑c 0c NC Nc Spac  2c ↑c Tc   1c  |
41 | 32, 40 | syl 15 |
. . . . . . . . . . . 12
 NC   2c ↑c
Tc  ↑c 0c NC Nc
Spac  2c ↑c Tc   1c  |
42 | 41 | adantl 452 |
. . . . . . . . . . 11
 c We NC NC   2c ↑c Tc 
↑c 0c NC Nc Spac  2c ↑c Tc   1c  |
43 | 34, 42 | sylbird 226 |
. . . . . . . . . 10
 c We NC NC Nc 1c c 2c ↑c Tc 
Nc Spac  2c ↑c Tc   1c  |
44 | | nclecid 6198 |
. . . . . . . . . . . . . . . . . . 19
Nc 1c NC Nc 1c c Nc
1c |
45 | 4, 44 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
Nc 1c c Nc
1c |
46 | | ce0lenc1 6240 |
. . . . . . . . . . . . . . . . . . 19
Nc 1c NC  Nc 1c
↑c 0c NC Nc
1c c Nc 1c  |
47 | 4, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
 Nc
1c ↑c 0c NC Nc 1c c Nc
1c |
48 | 45, 47 | mpbir 200 |
. . . . . . . . . . . . . . . . 17
Nc 1c ↑c
0c
NC |
49 | | ce2lt 6221 |
. . . . . . . . . . . . . . . . 17
 Nc
1c
NC
Nc 1c ↑c
0c
NC Nc 1c c 2c ↑c Nc 1c  |
50 | 4, 48, 49 | mp2an 653 |
. . . . . . . . . . . . . . . 16
Nc 1c c 2c ↑c Nc 1c |
51 | | 2nnc 6168 |
. . . . . . . . . . . . . . . . . 18
2c
Nn |
52 | | ceclnn1 6190 |
. . . . . . . . . . . . . . . . . 18
 2c Nn Nc 1c NC Nc
1c ↑c 0c NC 2c ↑c Nc 1c NC  |
53 | 51, 4, 48, 52 | mp3an 1277 |
. . . . . . . . . . . . . . . . 17
2c
↑c Nc
1c
NC |
54 | | nchoicelem8 6297 |
. . . . . . . . . . . . . . . . 17
 c We NC 2c ↑c Nc 1c NC   2c ↑c Nc 1c ↑c
0c
NC Nc
1c c 2c ↑c Nc 1c   |
55 | 53, 54 | mpan2 652 |
. . . . . . . . . . . . . . . 16
c We
NC   2c ↑c
Nc 1c ↑c
0c
NC Nc
1c c 2c ↑c Nc 1c   |
56 | 50, 55 | mpbiri 224 |
. . . . . . . . . . . . . . 15
c We
NC  2c
↑c Nc
1c
↑c 0c NC  |
57 | | nchoicelem3 6292 |
. . . . . . . . . . . . . . . . . 18
  2c ↑c Nc 1c NC  2c ↑c Nc 1c ↑c
0c
NC Spac  2c ↑c Nc 1c  2c
↑c Nc
1c   |
58 | 57 | nceqd 6111 |
. . . . . . . . . . . . . . . . 17
  2c ↑c Nc 1c NC  2c ↑c Nc 1c ↑c
0c
NC Nc Spac  2c ↑c Nc 1c Nc  2c ↑c Nc 1c   |
59 | | ovex 5552 |
. . . . . . . . . . . . . . . . . 18
2c
↑c Nc
1c
 |
60 | 59 | df1c3 6141 |
. . . . . . . . . . . . . . . . 17
1c
Nc  2c ↑c Nc 1c  |
61 | 58, 60 | syl6eqr 2403 |
. . . . . . . . . . . . . . . 16
  2c ↑c Nc 1c NC  2c ↑c Nc 1c ↑c
0c
NC Nc Spac  2c ↑c Nc 1c
1c |
62 | 53, 61 | mpan 651 |
. . . . . . . . . . . . . . 15
  2c ↑c Nc 1c ↑c
0c
NC Nc Spac  2c
↑c Nc
1c 1c |
63 | 56, 62 | syl 15 |
. . . . . . . . . . . . . 14
c We
NC Nc Spac  2c ↑c Nc 1c
1c |
64 | 63 | addceq1d 4390 |
. . . . . . . . . . . . 13
c We
NC Nc Spac  2c
↑c Nc
1c
1c
1c 1c  |
65 | | nchoicelem7 6296 |
. . . . . . . . . . . . . 14
 Nc
1c
NC
Nc 1c ↑c
0c
NC Nc Spac Nc
1c
Nc Spac  2c ↑c Nc 1c
1c  |
66 | 4, 48, 65 | mp2an 653 |
. . . . . . . . . . . . 13
Nc Spac Nc
1c
Nc Spac  2c ↑c Nc 1c
1c |
67 | | 1p1e2c 6156 |
. . . . . . . . . . . . . 14
1c
1c
2c |
68 | 67 | eqcomi 2357 |
. . . . . . . . . . . . 13
2c
1c
1c |
69 | 64, 66, 68 | 3eqtr4g 2410 |
. . . . . . . . . . . 12
c We
NC Nc Spac Nc
1c
2c |
70 | | fveq2 5329 |
. . . . . . . . . . . . . 14
Nc 1c 2c ↑c Tc 
Spac Nc
1c
Spac  2c ↑c Tc     |
71 | 70 | nceqd 6111 |
. . . . . . . . . . . . 13
Nc 1c 2c ↑c Tc 
Nc Spac Nc
1c
Nc Spac  2c ↑c Tc     |
72 | 71 | eqeq1d 2361 |
. . . . . . . . . . . 12
Nc 1c 2c ↑c Tc 
Nc Spac Nc
1c
2c
Nc Spac  2c ↑c Tc   2c  |
73 | 69, 72 | syl5ibcom 211 |
. . . . . . . . . . 11
c We
NC Nc 1c 2c ↑c
Tc  Nc Spac  2c ↑c Tc   2c  |
74 | 73 | adantr 451 |
. . . . . . . . . 10
 c We NC NC Nc 1c 2c ↑c Tc 
Nc Spac  2c ↑c Tc   2c  |
75 | 43, 74 | orim12d 811 |
. . . . . . . . 9
 c We NC NC  Nc
1c c 2c ↑c Tc 
Nc 1c 2c ↑c Tc   Nc Spac  2c ↑c Tc   1c Nc Spac  2c ↑c Tc   2c   |
76 | 31, 75 | syl5 28 |
. . . . . . . 8
 c We NC NC Nc 1c c 2c ↑c
Tc  Nc Spac  2c ↑c Tc   1c Nc Spac  2c ↑c Tc   2c   |
77 | 20, 76 | syl5bi 208 |
. . . . . . 7
 c We NC NC  2c ↑c
Nc 1 1c c 2c ↑c Tc 
Nc Spac  2c ↑c Tc   1c Nc Spac  2c ↑c Tc   2c   |
78 | 18, 77 | syld 40 |
. . . . . 6
 c We NC NC Nc 1 1c c Tc Nc Spac  2c ↑c Tc   1c Nc Spac  2c ↑c Tc   2c   |
79 | 9, 78 | syl5bi 208 |
. . . . 5
 c We NC NC Tc Nc
1c c Tc Nc Spac
 2c
↑c Tc  
1c Nc Spac  2c
↑c Tc  
2c   |
80 | 7, 79 | sylbid 206 |
. . . 4
 c We NC NC Nc 1c c Nc Spac  2c
↑c Tc  
1c Nc Spac  2c
↑c Tc  
2c   |
81 | | addceq1 4384 |
. . . . 5
Nc Spac  2c ↑c Tc   1c Nc Spac  2c ↑c Tc  
1c
1c 1c  |
82 | | addceq1 4384 |
. . . . 5
Nc Spac  2c ↑c Tc   2c Nc Spac  2c ↑c Tc  
1c
2c 1c  |
83 | 81, 82 | orim12i 502 |
. . . 4
 Nc Spac  2c ↑c Tc   1c Nc Spac  2c ↑c Tc   2c 
Nc Spac  2c ↑c Tc  
1c
1c 1c
Nc Spac  2c ↑c Tc  
1c
2c 1c   |
84 | 2, 80, 83 | syl56 30 |
. . 3
 c We NC NC Nc 1c c  Nc Spac  2c ↑c Tc  
1c
1c 1c
Nc Spac  2c ↑c Tc  
1c
2c 1c    |
85 | | nchoicelem8 6297 |
. . 3
 c We NC NC  
↑c 0c NC Nc
1c c    |
86 | | nchoicelem7 6296 |
. . . . . . 7
 Tc NC Tc ↑c 0c NC Nc Spac Tc  Nc Spac  2c ↑c Tc  
1c  |
87 | 10, 11, 86 | syl2anc 642 |
. . . . . 6
 NC Nc Spac Tc  Nc Spac  2c ↑c Tc  
1c  |
88 | 68 | a1i 10 |
. . . . . 6
 NC 2c 1c 1c  |
89 | 87, 88 | eqeq12d 2367 |
. . . . 5
 NC Nc Spac Tc 
2c
Nc Spac  2c ↑c Tc  
1c
1c 1c   |
90 | | 2p1e3c 6157 |
. . . . . . . 8
2c
1c
3c |
91 | 90 | eqcomi 2357 |
. . . . . . 7
3c
2c
1c |
92 | 91 | a1i 10 |
. . . . . 6
 NC 3c 2c 1c  |
93 | 87, 92 | eqeq12d 2367 |
. . . . 5
 NC Nc Spac Tc 
3c
Nc Spac  2c ↑c Tc  
1c
2c 1c   |
94 | 89, 93 | orbi12d 690 |
. . . 4
 NC  Nc Spac Tc 
2c
Nc Spac Tc 
3c
 Nc Spac  2c ↑c Tc  
1c
1c 1c
Nc Spac  2c ↑c Tc  
1c
2c 1c    |
95 | 94 | adantl 452 |
. . 3
 c We NC NC  Nc Spac Tc  2c Nc Spac
Tc 
3c
 Nc Spac  2c ↑c Tc  
1c
1c 1c
Nc Spac  2c ↑c Tc  
1c
2c 1c    |
96 | 84, 85, 95 | 3imtr4d 259 |
. 2
 c We NC NC  
↑c 0c NC Nc Spac Tc 
2c
Nc Spac Tc 
3c   |
97 | 96 | 3impia 1148 |
1
 c We NC NC  ↑c
0c
NC Nc Spac Tc 
2c
Nc Spac Tc 
3c  |