**Update:**made public now enough time has passed that it won't bug my non-math friends.

Hello, welcome to my new hard sums filter! Thanks for joining; if you're on and don't want to be, no problem, just let me know.

Chapter 2 of Category Theory, page 30, introduces Boolean algebras. Background: a preorder is any binary relation which is reflexive and transitive; a poset is any preorder which is antisymmetric. The text goes on to explain:

A Boolean algebra is a poset B equipped with distinguished elements 0, 1, binary operations a ∨ b of “join” and a ∧ b of “meet,” and a unary operation ¬b of “complementation.” These are required to satisfy the conditionsI think I have a proof of this last assertion, but it's a bit longer than I'd expect for something that says "it is not hard to see". From the way the text just presents the defining axioms and then makes this last assertion, I'd expect that I wouldn't have to prove a lot of stuff on top of them to get there, but it seems like I do.[...] A filter in a Boolean algebra B is a nonempty subset F ⊆ B that is closed upward and under meets:

- 0 ≤ a
- a ≤ 1
- a ≤ c and b ≤ c iff a ∨ b ≤ c
- c ≤ a and c ≤ b iff c ≤ a ∧ b
- a ≤ ¬b iff a ∧ b = 0
- ¬¬a = a
A filter F is maximal if the only strictly larger filter F ⊂ F' is the “improper” filter, namely all of B. An ultrafilter is a maximal filter. It is not hard to see that a filter F is an ultrafilter just if for every element b ∈ B, either b ∈ F or ¬b ∈ F, and not both (exercise!).

- a ∈ F and a ≤ b implies b ∈ F
- a ∈ F and b ∈ F implies a ∧ b ∈ F

The backwards part I can see. If F is not an ultrafilter, then there's some strictly larger F ⊂ F' ⊂ B. Let b be any element in F' but not in F. If ¬b were in F', then b ∧ ¬b = 0 would be in F', which would mean that F' = B, a contradiction. Therefore ¬b is not in F', so neither b nor ¬b are in F.

But it's the forward part I'm having trouble with. I asked about this on mathoverflow.net, and it feels as if the answer I got took me to exactly the point I'd got to when I asked the question; the proof invites me to "consider the filter generated by F ∪ b - which is to say the smallest filter F' containing F and b" but I got stuck exactly on proving that such an F' exists.

There's an argument to this effect in the comments, and it seems persuasive but a long way from being a proof. The final sentence reads "And if it's the meet of things included by upwards closure, I may as well pick the thing at the bottom to meet with - thus I can assume it to be a b ∧ f". To turn this into a proof, I think I have to prove that if I close first over meets and then upwards, the resulting set is still closed under meets. I can do that - this is the explicit construction of F' that I started off asking for. But the wording "it is not hard to see" suggests that there must be a simpler, more direct proof that I'm missing.

Anyone see a more straightforward way? Am I over-complicating things and failing to appreciate the elegance of the proof I've already been given? Thanks!