NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nchoicelem17 Unicode version

Theorem nchoicelem17 6305
Description: Lemma for nchoice 6308. If the special set of a cardinal is finite, then so is the special set of its T-raising, and there is a calculable relationship between their sizes. Theorem 7.2 of [Specker] p. 974. (Contributed by SF, 19-Mar-2015.)
Assertion
Ref Expression
nchoicelem17 <_c We NC NC Spac Fin Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c

Proof of Theorem nchoicelem17
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 finnc 6243 . . 3 Spac Fin Nc Spac Nn
2 risset 2661 . . . 4 Nc Spac Nn Nn Nc Spac
3 nchoicelem13 6301 . . . . . . 7 NC 1c <_c Nc Spac
43ad2antlr 707 . . . . . 6 <_c We NC NC Nn 1c <_c Nc Spac
5 1cnc 6139 . . . . . . . 8 1c NC
6 fvex 5339 . . . . . . . . 9 Spac
76ncelncsi 6121 . . . . . . . 8 Nc Spac NC
8 dflec2 6210 . . . . . . . 8 1c NC Nc Spac NC 1c <_c Nc Spac NC Nc Spac 1c
95, 7, 8mp2an 653 . . . . . . 7 1c <_c Nc Spac NC Nc Spac 1c
10 eqtr 2370 . . . . . . . . . . . 12 Nc Spac Nc Spac 1c 1c
1110ancoms 439 . . . . . . . . . . 11 Nc Spac 1c Nc Spac 1c
12 eqtr2 2371 . . . . . . . . . . . . 13 Nc Spac 1c Nc Spac 1c
1312ex 423 . . . . . . . . . . . 12 Nc Spac 1c Nc Spac 1c
1413adantl 452 . . . . . . . . . . 11 Nc Spac 1c Nc Spac 1c Nc Spac 1c
1511, 14jcai 522 . . . . . . . . . 10 Nc Spac 1c Nc Spac 1c Nc Spac 1c
16 addceq2 4384 . . . . . . . . . . . . . . . . . 18 1c 1c
17 addccom 4406 . . . . . . . . . . . . . . . . . 18 1c 1c
1816, 17syl6eq 2401 . . . . . . . . . . . . . . . . 17 1c 1c
1918eqeq2d 2364 . . . . . . . . . . . . . . . 16 1c 1c
2019rspcev 2955 . . . . . . . . . . . . . . 15 1c NC 1c NC
215, 20mpan 651 . . . . . . . . . . . . . 14 1c NC
22 nnnc 6146 . . . . . . . . . . . . . . . 16 Nn NC
23 dflec2 6210 . . . . . . . . . . . . . . . 16 NC NC <_c NC
2422, 23sylan2 460 . . . . . . . . . . . . . . 15 NC Nn <_c NC
2524ancoms 439 . . . . . . . . . . . . . 14 Nn NC <_c NC
2621, 25syl5ibr 212 . . . . . . . . . . . . 13 Nn NC 1c <_c
2726adantll 694 . . . . . . . . . . . 12 <_c We NC NC Nn NC 1c <_c
28 nclenn 6249 . . . . . . . . . . . . . . 15 NC Nn <_c Nn
29283expia 1153 . . . . . . . . . . . . . 14 NC Nn <_c Nn
3029ancoms 439 . . . . . . . . . . . . 13 Nn NC <_c Nn
3130adantll 694 . . . . . . . . . . . 12 <_c We NC NC Nn NC <_c Nn
32 nchoicelem16 6304 . . . . . . . . . . . . . . . . . 18 <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
33 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . . 23 0c 1c 1c 0c
34 addcid1 4405 . . . . . . . . . . . . . . . . . . . . . . 23 1c 0c 1c
3533, 34syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . 22 0c 1c 1c
3635eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 0c Nc Spac 1c Nc Spac 1c
3736imbi1d 308 . . . . . . . . . . . . . . . . . . . 20 0c Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
3837ralbidv 2634 . . . . . . . . . . . . . . . . . . 19 0c NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
3938imbi2d 307 . . . . . . . . . . . . . . . . . 18 0c <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
40 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . 22 1c 1c
4140eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 Nc Spac 1c Nc Spac 1c
4241imbi1d 308 . . . . . . . . . . . . . . . . . . . 20 Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
4342ralbidv 2634 . . . . . . . . . . . . . . . . . . 19 NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
4443imbi2d 307 . . . . . . . . . . . . . . . . . 18 <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
45 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . . 23 1c 1c 1c 1c
4645eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . 22 1c Nc Spac 1c Nc Spac 1c 1c
4746imbi1d 308 . . . . . . . . . . . . . . . . . . . . 21 1c Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
4847ralbidv 2634 . . . . . . . . . . . . . . . . . . . 20 1c NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
49 fveq2 5328 . . . . . . . . . . . . . . . . . . . . . . . 24 Spac Spac
5049nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . 23 Nc Spac Nc Spac
5150eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . 22 Nc Spac 1c 1c Nc Spac 1c 1c
52 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . 25 Tc Tc
5352fveq2d 5332 . . . . . . . . . . . . . . . . . . . . . . . 24 Spac Tc Spac Tc
5453eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . 23 Spac Tc Fin Spac Tc Fin
5553nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nc Spac Tc Nc Spac Tc
56 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nc Spac Nc Spac Tc Nc Spac Tc Nc Spac
5750, 56syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Tc Nc Spac Tc Nc Spac
5857addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . 25 Tc Nc Spac 1c Tc Nc Spac 1c
5955, 58eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . 24 Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 1c
6057addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . 25 Tc Nc Spac 2c Tc Nc Spac 2c
6155, 60eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . 24 Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc Tc Nc Spac 2c
6259, 61orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . 23 Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
6354, 62anbi12d 691 . . . . . . . . . . . . . . . . . . . . . 22 Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
6451, 63imbi12d 311 . . . . . . . . . . . . . . . . . . . . 21 Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
6564cbvralv 2835 . . . . . . . . . . . . . . . . . . . 20 NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
6648, 65syl6bb 252 . . . . . . . . . . . . . . . . . . 19 1c NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
6766imbi2d 307 . . . . . . . . . . . . . . . . . 18 1c <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c <_c We NC NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
68 addceq2 4384 . . . . . . . . . . . . . . . . . . . . . 22 1c 1c
6968eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . 21 Nc Spac 1c Nc Spac 1c
7069imbi1d 308 . . . . . . . . . . . . . . . . . . . 20 Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
7170ralbidv 2634 . . . . . . . . . . . . . . . . . . 19 NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
7271imbi2d 307 . . . . . . . . . . . . . . . . . 18 <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
73 nchoicelem14 6302 . . . . . . . . . . . . . . . . . . . . . 22 NC Nc Spac 1c c 0c NC
7473ex 423 . . . . . . . . . . . . . . . . . . . . 21 NC Nc Spac 1c c 0c NC
7574adantl 452 . . . . . . . . . . . . . . . . . . . 20 <_c We NC NC Nc Spac 1c c 0c NC
76 nchoicelem9 6297 . . . . . . . . . . . . . . . . . . . . . . 23 <_c We NC NC c 0c NC Nc Spac Tc 2c Nc Spac Tc 3c
77 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nc Spac Tc 2c Nc Spac Tc 2c
78 2nnc 6167 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2c Nn
7977, 78syl6eqel 2441 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nc Spac Tc 2c Nc Spac Tc Nn
80 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nc Spac Tc 3c Nc Spac Tc 3c
81 2p1e3c 6156 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2c 1c 3c
82 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2c Nn 2c 1c Nn
8378, 82ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2c 1c Nn
8481, 83eqeltrri 2424 . . . . . . . . . . . . . . . . . . . . . . . . . 26 3c Nn
8580, 84syl6eqel 2441 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nc Spac Tc 3c Nc Spac Tc Nn
8679, 85jaoi 368 . . . . . . . . . . . . . . . . . . . . . . . 24 Nc Spac Tc 2c Nc Spac Tc 3c Nc Spac Tc Nn
87 finnc 6243 . . . . . . . . . . . . . . . . . . . . . . . 24 Spac Tc Fin Nc Spac Tc Nn
8886, 87sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23 Nc Spac Tc 2c Nc Spac Tc 3c Spac Tc Fin
8976, 88syl 15 . . . . . . . . . . . . . . . . . . . . . 22 <_c We NC NC c 0c NC Spac Tc Fin
90 1p1e2c 6155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1c 1c 2c
9190eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nc Spac Tc 1c 1c Nc Spac Tc 2c
92 addccom 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1c 2c 2c 1c
9392, 81eqtri 2373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1c 2c 3c
9493eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nc Spac Tc 1c 2c Nc Spac Tc 3c
9591, 94orbi12i 507 . . . . . . . . . . . . . . . . . . . . . . . 24 Nc Spac Tc 1c 1c Nc Spac Tc 1c 2c Nc Spac Tc 2c Nc Spac Tc 3c
9676, 95sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23 <_c We NC NC c 0c NC Nc Spac Tc 1c 1c Nc Spac Tc 1c 2c
97 nchoicelem3 6291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 NC c 0c NC Spac
9897nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 NC c 0c NC Nc Spac Nc
99 df1c3g 6141 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 NC 1c Nc
10099adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 NC c 0c NC 1c Nc
10198, 100eqtr4d 2388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 NC c 0c NC Nc Spac 1c
102 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Nc Spac 1c Tc Nc Spac Tc 1c
103101, 102syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 NC c 0c NC Tc Nc Spac Tc 1c
104 tc1c 6165 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Tc 1c 1c
105103, 104syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 NC c 0c NC Tc Nc Spac 1c
106105addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 NC c 0c NC Tc Nc Spac 1c 1c 1c
107106eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . 25 NC c 0c NC Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc 1c 1c
108105addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . 26 NC c 0c NC Tc Nc Spac 2c 1c 2c
109108eqeq2d 2364 . . . . . . . . . . . . . . . . . . . . . . . . 25 NC c 0c NC Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc 1c 2c
110107, 109orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . 24 NC c 0c NC Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc 1c 1c Nc Spac Tc 1c 2c
1111103adant1 973 . . . . . . . . . . . . . . . . . . . . . . 23 <_c We NC NC c 0c NC Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc 1c 1c Nc Spac Tc 1c 2c
11296, 111mpbird 223 . . . . . . . . . . . . . . . . . . . . . 22 <_c We NC NC c 0c NC Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
11389, 112jca 518 . . . . . . . . . . . . . . . . . . . . 21 <_c We NC NC c 0c NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
1141133expia 1153 . . . . . . . . . . . . . . . . . . . 20 <_c We NC NC c 0c NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
11575, 114syld 40 . . . . . . . . . . . . . . . . . . 19 <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
116115ralrimiva 2697 . . . . . . . . . . . . . . . . . 18 <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
117 addccom 4406 . . . . . . . . . . . . . . . . . . . . . . . 24 1c 1c 1c 1c
118117eqeq2i 2363 . . . . . . . . . . . . . . . . . . . . . . 23 Nc Spac 1c 1c Nc Spac 1c 1c
119 nchoicelem13 6301 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 NC 1c <_c Nc Spac
120119ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c 1c <_c Nc Spac
121 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nn
122 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 NC Nc Spac 1c 1c Nc Spac 1c 1c
123 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Nn Nc Spac 1c 1c Nc Spac 1c 1c
124 0cnsuc 4401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 1c 0c
125 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Nn 1c Nn
126 peano1 4402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 0c Nn
127 1cnnc 4408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1c Nn
128 addccan1 4560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 1c Nn 0c Nn 1c Nn 1c 1c 0c 1c 1c 0c
129126, 127, 128mp3an23 1269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 1c Nn 1c 1c 0c 1c 1c 0c
130125, 129syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Nn 1c 1c 0c 1c 1c 0c
131130necon3bid 2551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Nn 1c 1c 0c 1c 1c 0c
132124, 131mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Nn 1c 1c 0c 1c
133 addcid2 4407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 0c 1c 1c
134133neeq2i 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1c 1c 0c 1c 1c 1c 1c
135132, 134sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Nn 1c 1c 1c
136135adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Nn Nc Spac 1c 1c 1c 1c 1c
137123, 136eqnetrd 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Nn Nc Spac 1c 1c Nc Spac 1c
138121, 122, 137syl2an 463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Nc Spac 1c
139138necomd 2599 . . . . . . . . . . . . . . . . . . . . . . . . . 26 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c 1c Nc Spac
140 brltc 6114 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1c <c Nc Spac 1c <_c Nc Spac 1c Nc Spac
141120, 139, 140sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . . . . 25 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c 1c <c Nc Spac
142 nchoicelem15 6303 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 NC 1c <c Nc Spac c 0c NC
143142ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 NC 1c <c Nc Spac c 0c NC
144143ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . . . 26 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c 1c <c Nc Spac c 0c NC
145 df-3an 936 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 NC Nc Spac 1c 1c c 0c NC NC Nc Spac 1c 1c c 0c NC
146 ceclnn1 6189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2c Nn NC c 0c NC 2cc NC
14778, 146mp3an1 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 NC c 0c NC 2cc NC
1481473adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 NC Nc Spac 1c 1c c 0c NC 2cc NC
149148adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c c 0c NC 2cc NC
150 fveq2 5328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2cc Spac Spac 2cc
151150nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2cc Nc Spac Nc Spac 2cc
152151eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2cc Nc Spac 1c Nc Spac 2cc 1c
153 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2cc Tc Tc 2cc
154153fveq2d 5332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2cc Spac Tc Spac Tc 2cc
155154eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2cc Spac Tc Fin Spac Tc 2cc Fin
156154nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2cc Nc Spac Tc Nc Spac Tc 2cc
157 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Nc Spac Nc Spac 2cc Tc Nc Spac Tc Nc Spac 2cc
158151, 157syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2cc Tc Nc Spac Tc Nc Spac 2cc
159158addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2cc Tc Nc Spac 1c Tc Nc Spac 2cc 1c
160156, 159eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2cc Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 1c
161158addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 2cc Tc Nc Spac 2c Tc Nc Spac 2cc 2c
162156, 161eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2cc Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c
163160, 162orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 2cc Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c
164155, 163anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2cc Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Spac Tc 2cc Fin Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c
165152, 164imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2cc Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac 2cc 1c Spac Tc 2cc Fin Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c
166165rspccva 2954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c 2cc NC Nc Spac 2cc 1c Spac Tc 2cc Fin Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c
167 tce2 6236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 NC c 0c NC Tc 2cc 2cc Tc
168167fveq2d 5332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 NC c 0c NC Spac Tc 2cc Spac 2cc Tc
169168eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 NC c 0c NC Spac Tc 2cc Fin Spac 2cc Tc Fin
170168nceqd 6110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 NC c 0c NC Nc Spac Tc 2cc Nc Spac 2cc Tc
171170eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 NC c 0c NC Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc Tc Nc Spac 2cc 1c
172170eqeq1d 2361 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 NC c 0c NC Nc Spac Tc 2cc Tc Nc Spac 2cc 2c Nc Spac 2cc Tc Tc Nc Spac 2cc 2c
173171, 172orbi12d 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 NC c 0c NC Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc Tc Nc Spac 2cc 2c
174169, 173anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 NC c 0c NC Spac Tc 2cc Fin Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c Spac 2cc Tc Fin Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc Tc Nc Spac 2cc 2c
175174imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 NC c 0c NC Nc Spac 2cc 1c Spac Tc 2cc Fin Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c Nc Spac 2cc 1c Spac 2cc Tc Fin Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc Tc Nc Spac 2cc 2c
1761753adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc 1c Spac Tc 2cc Fin Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c Nc Spac 2cc 1c Spac 2cc Tc Fin Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc Tc Nc Spac 2cc 2c
177176adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc 1c Spac Tc 2cc Fin Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c Nc Spac 2cc 1c Spac 2cc Tc Fin Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc Tc Nc Spac 2cc 2c
178 nchoicelem7 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 NC c 0c NC Nc Spac Nc Spac 2cc 1c
1791783adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 NC Nc Spac 1c 1c c 0c NC Nc Spac Nc Spac 2cc 1c
180 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 NC Nc Spac 1c 1c c 0c NC Nc Spac 1c 1c
181179, 180eqtr3d 2387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc 1c 1c 1c
182181adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc 1c 1c 1c
183 nnnc 6146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 1c Nn 1c NC
184 fvex 5339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Spac 2cc
185184ncelncsi 6121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Nc Spac 2cc NC
186 peano4nc 6150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Nc Spac 2cc NC 1c NC Nc Spac 2cc 1c 1c 1c Nc Spac 2cc 1c
187185, 186mpan 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 1c NC Nc Spac 2cc 1c 1c 1c Nc Spac 2cc 1c
188125, 183, 1873syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Nn Nc Spac 2cc 1c 1c 1c Nc Spac 2cc 1c
189188ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc 1c 1c 1c Nc Spac 2cc 1c
190182, 189mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc 1c
191 addccom 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 1c 1c
192190, 191syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc 1c
193 peano2 4403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Nc Spac 2cc Tc Nn Nc Spac 2cc Tc 1c Nn
194 tccl 6160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 NC Tc NC
195 te0c 6237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 NC Tc c 0c NC
196 nchoicelem7 6295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Tc NC Tc c 0c NC Nc Spac Tc Nc Spac 2cc Tc 1c
197194, 195, 196syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 NC Nc Spac Tc Nc Spac 2cc Tc 1c
1981973ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 NC Nc Spac 1c 1c c 0c NC Nc Spac Tc Nc Spac 2cc Tc 1c
199198adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac Tc Nc Spac 2cc Tc 1c
200199eleq1d 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac Tc Nn Nc Spac 2cc Tc 1c Nn
201193, 200syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc Tc Nn Nc Spac Tc Nn
202 finnc 6243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Spac 2cc Tc Fin Nc Spac 2cc Tc Nn
203 finnc 6243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Spac Tc Fin Nc Spac Tc Nn
204201, 202, 2033imtr4g 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Spac 2cc Tc Fin Spac Tc Fin
205 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc 1c Tc Nc Spac 2cc 1c 1c
206 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 Nc Spac Nc Spac 2cc 1c Tc Nc Spac Tc Nc Spac 2cc 1c
207178, 206syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 NC c 0c NC Tc Nc Spac Tc Nc Spac 2cc 1c
2082073adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 NC Nc Spac 1c 1c c 0c NC Tc Nc Spac Tc Nc Spac 2cc 1c
209208adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Tc Nc Spac Tc Nc Spac 2cc 1c
210 tcdi 6164 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 Nc Spac 2cc NC 1c NC Tc Nc Spac 2cc 1c Tc Nc Spac 2cc Tc 1c
211185, 5, 210mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Tc Nc Spac 2cc 1c Tc Nc Spac 2cc Tc 1c
212104addceq2i 4387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 Tc Nc Spac 2cc Tc 1c Tc Nc Spac 2cc 1c
213211, 212eqtri 2373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 Tc Nc Spac 2cc 1c Tc Nc Spac 2cc 1c
214209, 213syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Tc Nc Spac Tc Nc Spac 2cc 1c
215214addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Tc Nc Spac 1c Tc Nc Spac 2cc 1c 1c
216199, 215eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac Tc Tc Nc Spac 1c Nc Spac 2cc Tc 1c Tc Nc Spac 2cc 1c 1c
217205, 216syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac Tc Tc Nc Spac 1c
218 addceq1 4383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Nc Spac 2cc Tc Tc Nc Spac 2cc 2c Nc Spac 2cc Tc 1c Tc Nc Spac 2cc 2c 1c
219214addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Tc Nc Spac 2c Tc Nc Spac 2cc 1c 2c
220 addc32 4416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 Tc Nc Spac 2cc 1c 2c Tc Nc Spac 2cc 2c 1c
221219, 220syl6eq 2401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Tc Nc Spac 2c Tc Nc Spac 2cc 2c 1c
222199, 221eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac Tc Tc Nc Spac 2c Nc Spac 2cc Tc 1c Tc Nc Spac 2cc 2c 1c
223218, 222syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc Tc Tc Nc Spac 2cc 2c Nc Spac Tc Tc Nc Spac 2c
224217, 223orim12d 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc Tc Nc Spac 2cc 2c Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
225204, 224anim12d 546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Spac 2cc Tc Fin Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc Tc Nc Spac 2cc 2c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
226192, 225embantd 50 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc 1c Spac 2cc Tc Fin Nc Spac 2cc Tc Tc Nc Spac 2cc 1c Nc Spac 2cc Tc Tc Nc Spac 2cc 2c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
227177, 226sylbid 206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC Nc Spac 2cc 1c Spac Tc 2cc Fin Nc Spac Tc 2cc Tc Nc Spac 2cc 1c Nc Spac Tc 2cc Tc Nc Spac 2cc 2c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
228166, 227syl5 28 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c 2cc NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
229228exp4b 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 <_c We NC Nn NC Nc Spac 1c 1c c 0c NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c 2cc NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
230229com23 72 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c c 0c NC 2cc NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
2312303impia 1148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c c 0c NC 2cc NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
232231imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c c 0c NC 2cc NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
233149, 232mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c c 0c NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
234145, 233sylan2br 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c c 0c NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
235234expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c c 0c NC Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
236144, 235syld 40 . . . . . . . . . . . . . . . . . . . . . . . . 25 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c 1c <c Nc Spac Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
237141, 236mpd 14 . . . . . . . . . . . . . . . . . . . . . . . 24 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
238237expr 598 . . . . . . . . . . . . . . . . . . . . . . 23 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
239118, 238syl5bi 208 . . . . . . . . . . . . . . . . . . . . . 22 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
240239ralrimiva 2697 . . . . . . . . . . . . . . . . . . . . 21 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
2412403exp 1150 . . . . . . . . . . . . . . . . . . . 20 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
242241com12 27 . . . . . . . . . . . . . . . . . . 19 Nn <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
243242a2d 23 . . . . . . . . . . . . . . . . . 18 Nn <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c <_c We NC NC Nc Spac 1c 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
24432, 39, 44, 67, 72, 116, 243finds 4411 . . . . . . . . . . . . . . . . 17 Nn <_c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
245 fveq2 5328 . . . . . . . . . . . . . . . . . . . . 21 Spac Spac
246245nceqd 6110 . . . . . . . . . . . . . . . . . . . 20 Nc Spac Nc Spac
247246eqeq1d 2361 . . . . . . . . . . . . . . . . . . 19 Nc Spac 1c Nc Spac 1c
248 tceq 6158 . . . . . . . . . . . . . . . . . . . . . 22 Tc Tc
249248fveq2d 5332 . . . . . . . . . . . . . . . . . . . . 21 Spac Tc Spac Tc
250249eleq1d 2419 . . . . . . . . . . . . . . . . . . . 20 Spac Tc Fin Spac Tc Fin
251249nceqd 6110 . . . . . . . . . . . . . . . . . . . . . 22 Nc Spac Tc Nc Spac Tc
252 tceq 6158 . . . . . . . . . . . . . . . . . . . . . . . 24 Nc Spac Nc Spac Tc Nc Spac Tc Nc Spac
253246, 252syl 15 . . . . . . . . . . . . . . . . . . . . . . 23 Tc Nc Spac Tc Nc Spac
254253addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . 22 Tc Nc Spac 1c Tc Nc Spac 1c
255251, 254eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . 21 Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 1c
256253addceq1d 4389 . . . . . . . . . . . . . . . . . . . . . 22 Tc Nc Spac 2c Tc Nc Spac 2c
257251, 256eqeq12d 2367 . . . . . . . . . . . . . . . . . . . . 21 Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc Tc Nc Spac 2c
258255, 257orbi12d 690 . . . . . . . . . . . . . . . . . . . 20 Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
259250, 258anbi12d 691 . . . . . . . . . . . . . . . . . . 19 Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
260247, 259imbi12d 311 . . . . . . . . . . . . . . . . . 18 Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
261260rspccv 2952 . . . . . . . . . . . . . . . . 17 NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
262244, 261syl6com 31 . . . . . . . . . . . . . . . 16 <_c We NC Nn NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
263262com23 72 . . . . . . . . . . . . . . 15 <_c We NC NC Nn Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
264263imp 418 . . . . . . . . . . . . . 14 <_c We NC NC Nn Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
265264adantr 451 . . . . . . . . . . . . 13 <_c We NC NC Nn Nn Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
266265adantr 451 . . . . . . . . . . . 12 <_c We NC NC Nn NC Nn Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
26727, 31, 2663syld 51 . . . . . . . . . . 11 <_c We NC NC Nn NC 1c Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
268267imp3a 420 . . . . . . . . . 10 <_c We NC NC Nn NC 1c Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
26915, 268syl5 28 . . . . . . . . 9 <_c We NC NC Nn NC Nc Spac 1c Nc Spac Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
270269exp3a 425 . . . . . . . 8 <_c We NC NC Nn NC Nc Spac 1c Nc Spac Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
271270rexlimdva 2738 . . . . . . 7 <_c We NC NC Nn NC Nc Spac 1c Nc Spac Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
2729, 271syl5bi 208 . . . . . 6 <_c We NC NC Nn 1c <_c Nc Spac Nc Spac Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
2734, 272mpd 14 . . . . 5 <_c We NC NC Nn Nc Spac Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
274273rexlimdva 2738 . . . 4 <_c We NC NC Nn Nc Spac Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
2752, 274syl5bi 208 . . 3 <_c We NC NC Nc Spac Nn Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
2761, 275syl5bi 208 . 2 <_c We NC NC Spac Fin Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
2772763impia 1148 1 <_c We NC NC Spac Fin Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358   w3a 934   wceq 1642   wcel 1710   wne 2516  wral 2614  wrex 2615  csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   cplc 4375   Fin cfin 4376   class class class wbr 4639  cfv 4781  (class class class)co 5525   We cwe 5895   NC cncs 6088   <_c clec 6089   <c cltc 6090   Nc cnc 6091   Tc ctc 6093  2cc2c 6094  3cc3c 6095   ↑c cce 6096   Spac cspac 6273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-csb 3137  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-tp 3743  df-uni 3892  df-int 3927  df-iun 3971  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-fv 4795  df-2nd 4797  df-ov 5526  df-oprab 5528  df-mpt 5652  df-mpt2 5654  df-txp 5736  df-fix 5740  df-cup 5742  df-disj 5744  df-addcfn 5746  df-compose 5748  df-ins2 5750  df-ins3 5752  df-image 5754  df-ins4 5756  df-si3 5758  df-funs 5760  df-fns 5762  df-pw1fn 5766  df-fullfun 5768  df-clos1 5873  df-trans 5899  df-antisym 5901  df-partial 5902  df-connex 5903  df-strict 5904  df-we 5906  df-sym 5908  df-er 5909  df-ec 5947  df-qs 5951  df-map 6001  df-en 6029  df-ncs 6098  df-lec 6099  df-ltc 6100  df-nc 6101  df-tc 6103  df-2c 6104  df-3c 6105  df-ce 6106  df-tcfn 6107  df-spac 6274
This theorem is referenced by:  nchoicelem19  6307  nchoice  6308
  Copyright terms: Public domain W3C validator