Talk:Conjunction of Disjunctions Consequence

From ProofWiki
Jump to navigation Jump to search

Do we have this result yet? It's just a dinky little convenience lemma, but I seem to keep running into it in these set theory basics. --Dfeuer (talk) 18:38, 23 March 2013 (UTC)

Quantified form

There's a general form of this theorem that is equally intuitive:

$\forall x: p(x) \lor q(x) \vdash (\forall x: p(x)) \lor (\exists x: q(x))$

This shows up when proving that a bounded subset of a minimally $g$-inductive class has a greatest element.

This theorem in set-theoretic terms: If $P$ and $Q$ are classes, then either $P \cup Q \subseteq P$ or $Q$ has an element. --Dfeuer (talk) 22:09, 26 March 2013 (UTC)