MHB Proving a Set Theory Statement Regarding Families of Sets

[logan3]

I was wondering if anyone could please check my work and reasoning for this problem. Thank-you! (Also, would this be considered a direct proof? How might a contradiction and IFF proof look like and compare?)

Problem: Suppose F, G₁ and G₂ are nonempty families of sets. Prove that if F ⊆ G₁ ∩ G₂, then ∩ G₁ ∪ ∩ G₂ ⊆ ∩ F.

Solution: Suppose F ⊆ G₁ ∩ G₂. Let A be an arbitrary element of F. Then since F ⊆ G₁ ∩ G₂ and A ∈ F, A ∈ G₁ ∩ G₂.

Let x be an arbitrary element of ∩ G₁ and y be an arbitrary element of ∩ G₂, which are defined since G₁ and G₂ are nonempty. Then by definition 2.3.5. (see below), ∀A (A ∈ G₁ → x ∈ A) and ∀A (A ∈ G₂ → y ∈ A). Thus, x, y ∈ A. Since A is an arbitrary element of F and x, y ∈ A, then x, y ∈ ∩ F, which is defined since F is nonempty. But x and y are arbitrary elements of ∩ G₁ and ∩ G₂, respectively, therefore ∩ G₁ ∪ ∩ G₂ ⊆ ∩ F.

Definition 2.3.5. Suppose F is a family of sets. Then the intersection is the set ∩ F and defined as: ∩ F = {x | ∀A ∈ F (x ∈ A)} = {x | ∀A (A ∈ F → x ∈ A)} (Velleman, 2006, p. 77).

 

[Evgeny.Makarov]

Your proof is correct, but I would change one subtle point. Proofs of statements of the form $\forall x\,P(x)$ often have the following shape: fix some $x$; prove $P(x)$; since $x$ was arbitrary conclude $\forall x\,P(x)$. If you have several such lines of reasoning within one proof, they should be properly nested. For example:

fix some x
  fix some y
    prove Q(y)
  conclude ∀y Q(y)
  use ∀y Q(y) to prove P(x)
conclude ∀x P(x)

In your case you are proving $\bigcap G_1\cup\bigcap G_2\subseteq\bigcap F$, so you should start by fixing an arbitrary $x\in\bigcap G_1\cup\bigcap G_2$ and considering two cases: $x\in\bigcap G_1$ and $x\in\bigcap G_2$. (You are considering these cases simultaneously, which is fine.) Your next task is to prove $\forall A\;(A\in F\to x\in A)$, so you fix an arbitrary $A$ and assume $A\in F$. This implies $A\in G_1$ and $A\in G_2$, so $x\in A$. This concludes a subproof of $\forall A\;(A\in F\to x\in A)$, i.e., $x\in \bigcap F$. At this point $A$ does not exist because the subproof that considered a specific $A$ is closed, but $x$ still does. Finally, you conclude $\forall x\;(x\in \bigcap G_1\cup\bigcap G_2\to x\in \bigcap F)$ and close the scope of $x$.