Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > axcc  Unicode version 
Description: The axiom of countable choice (CC), also known as the axiom of denumerable choice. It is clearly a special case of ac5 8313, but is weak enough that it can be proven using DC (see axcc 8294). It is, however, strictly stronger than ZF and cannot be proven in ZF. It states that any countable collection of nonempty sets must have a choice function. (Contributed by Mario Carneiro, 9Feb2013.) 
Ref  Expression 

axcc 
Step  Hyp  Ref  Expression 

1  vx  . . . 4  
2  1  cv 1648  . . 3 
3  com 4804  . . 3  
4  cen 7065  . . 3  
5  2, 3, 4  wbr 4172  . 2 
6  vz  . . . . . . 7  
7  6  cv 1648  . . . . . 6 
8  c0 3588  . . . . . 6  
9  7, 8  wne 2567  . . . . 5 
10  vf  . . . . . . . 8  
11  10  cv 1648  . . . . . . 7 
12  7, 11  cfv 5413  . . . . . 6 
13  12, 7  wcel 1721  . . . . 5 
14  9, 13  wi 4  . . . 4 
15  14, 6, 2  wral 2666  . . 3 
16  15, 10  wex 1547  . 2 
17  5, 16  wi 4  1 
Colors of variables: wff set class 
This axiom is referenced by: axcc2lem 8272 
Copyright terms: Public domain  W3C validator 