Talk:Draft:Union of Set of Sets is Greatest Element under Subset Relation

I haven't looked in proper detail yet, but I don't see the point of the comment. By default all set-theoretical statements on $\mathsf{Pr} \infty \mathsf{fWiki}$ are dependent upon ZFC. It's the default model. This is should probably be explained more prominently in the pages discussing (pure) set theory, but I would rather we didn't go down the path of adding to every proof the default axiomatic basis upon which it depends.

In the case where it is specifically the Axiom of Choice under discussion, we have {{AoC}} which can be invoked, which can be used to define what it is, specifically, that relies upon AoC. --prime mover (talk) 00:08, 21 November 2024 (UTC)

I figured the axioms used by S&F (see main talk request) were an extension of/not exactly ZFC. Further demonstration I need to visit the book before further edits! Tule-hog (talk) 00:18, 21 November 2024 (UTC)

According to this review, S&F uses NBG. Tule-hog (talk) 00:40, 21 November 2024 (UTC)

I've been considering adding a proof that NBG conservatively extends ZF for a while now; maybe it's time I buckled down and did that. There should be a "generic" version of this proof that does the same for ACA0 and PA at the same time, but I need to go track down that source again. CircuitCraft (talk) 03:24, 21 November 2024 (UTC)

This proof is assuming without justification that there is a greatest element. I'm not sure why you're doing a proof by contradiction at all; if $x \in M$, then obviously $x \subseteq \bigcup M$. CircuitCraft (talk) 01:41, 21 November 2024 (UTC)

We still aren't proving "greatest" here (actually, we're proving it, then switching course and doing something else). That terms means $\forall x: x \preceq G$. You might instead mean "maximal," which is $\forall x: M \preceq x \implies M = x$. In this case, of course, $x \preceq y \iff x \subseteq y$. Otherwise, just cut the paragraph that mentions antisymmetry. Also, we already have Set is Subset of Union/General Result. CircuitCraft (talk) 03:21, 21 November 2024 (UTC)