Do you know where I can find proof of equivalence Baire Category Theorem and DC (Axiom of Dependent Choice)? It is well known fact but I can't find appropriate literature with the proof.
You can find it, amongst other places in my write up:
Zornian Functional Analysis or: How I Learned to Stop Worrying and Love the Axiom of Choice.
If you need a source to cite, my money is on Handbook of Analysis and its Foundations by Eric S. Schechter.

$\begingroup$ Thank you very much, that's what I was looking for. $\endgroup$ – Michael Oct 3 at 12:55

3$\begingroup$ Now that's a title that makes me want to read the paper. $\endgroup$ – Andrej Bauer Oct 4 at 11:37


$\begingroup$ The section on automatic continuity suggests that one should try to quantify how much a map is continuous also in other settings, e.g., constructively: given $f : X \to Y$, consider the set $c(f) \subseteq X$ of points at which $f$ is continuous. Constructively we cannot refute $c(f) = X$, but we should be able to say more than that, at least under certain circumstances. $\endgroup$ – Andrej Bauer Oct 4 at 11:48

$\begingroup$ @Andrej: I'm sure that one can write "Excluded Functional Analysis or: How I Learned to Stop Worrying and Love the Law of Excluded Middle" paper along similar lines. $\endgroup$ – Asaf Karagila Oct 4 at 11:50
Wikipedia article on Baire category theorem and several other sources mention this paper: Blair, Charles E. The Baire category theorem implies the principle of dependent choices. Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 25 (1977), no. 10, 933–934. MR0469765, Zbl 0377.04011. However, I did not succeed in finding this paper online.
Still you can find this result for example in:
 Horst Herrlich: Axiom of Choice as Theorem 4.106
 Theo Bühler, Dietmar A. Salamon: Functional Analysis as Exercise 1.7.14
 John C. Oxtoby: Measure and Category, notes to Chapter 9, page 95
 Following the suggestion in Asaf Karagila's answer, I have looked also in the book Eric Schechter: Handbook of Analysis and Its Foundations. It contains this result in paragraph 20.16. (The result is stated for pseudometric spaces, but in the direction BCT $\Rightarrow$ DC, a metric spaces is used.)
 Some versions of Baire Category theorem are listed (together with references) Paul Howard, Jean E. Rubin: Consequences of the Axiom of Choice under Form 43.
EDIT: Some sources mention that the result was proved again later in this paper: Goldblatt, Robert, On the role of the Baire category theorem and dependent choice in the foundations of logic, J. Symb. Log. 50, 412422 (1985). ZBL0567.03023, MR793122.
(G. H. Moore uses this in the introduction of his book Zermelo's Axiom of Choice: Its Origins, Development, and Influence as an illustration that some kind of database with consequences of AC might be useful to decrease likelihood of reproving already known results.)
I will freely admit that I found some of the above results simply by trying to search for some suitable phrases in Google Books and Google Scholar. Maybe you might find some further references in this way. It might be also worth checking the work which cite Blair's paper; you can try them, e.g., in Google Scholar, Zentralblatt or MathSciNet. (I do not have access to the latter.) Or simply check the books which mention this paper.
Yet another formulation of Blair's proof is in M. Väth, Topological Analysis, DeGruyter 2012.

2$\begingroup$ To make this reference a bit easier to locate, I will add that it appears (in the first edition) as Theorem 2.3 on page 12 $\endgroup$ – Martin Sleziak Oct 3 at 16:30