Big intersection operation ∅ ≠ A ⊆ B ⇒ ⋂ B ⊆ ⋂ A .In each case, the proof is straightforward. For example, in the last case, we assume that every member of A is also a member of B. Hence if x ∈ ⋂ B, i.e., if x belongs to every member of B, then a fortiori x belongs to every member of the smaller collection A. And consequently x ∈ ⋂ A.I wonder if the last part is really a proof. It is okay to assume x ∈ ⋂ B and arrive at x ∈ ⋂ A. But can I use this reasoning "then a fortiori x belongs to every member of the smaller collection" in a proof exercise? It looks like just using intuition (it does not seem rigorous).

Question

Big intersection operation  ∅  ≠  A  ⊆  B      ⇒      ⋂  B  ⊆  ⋂  A  .In each case, the proof is straightforward. For example, in the last case, we assume that every member of A is also a member of B. Hence if   x  ∈  ⋂  B, i.e., if x belongs to every member of B, then a fortiori x belongs to every member of the smaller collection A. And consequently   x  ∈  ⋂  A.I wonder if the last part is really a proof. It is okay to assume   x  ∈  ⋂  B and arrive at   x  ∈  ⋂  A. But can I use this reasoning &quot;then a fortiori x belongs to every member of the smaller collection&quot; in a proof exercise? It looks like just using intuition (it does not seem rigorous).

esperoanow · Accepted Answer

Step 1I do not agree. It is a very rigorous argument, and I cannot see how it could be made more formal. Indeed, the proof assumes that   A  ⊆  B, which means that (I quote from the proof)every member of A is also a member of B.Step 2From that and from the fact that &quot;x belongs to every member of B&quot;, it follows immediately that, in particular, &quot;x belongs to every member of A&quot;. It is just a syllogistic inference roughly of the form &quot;if X implies Y and Y implies Z, then X implies Z&quot;, which does not require any further justification.

Alissa Hancock · Accepted Answer

Step 1In case it helps, here is a different style of proof of the same.For all x, we have                                        x        ∈        ⋂        A                            ≡                                    “                  definition of                                   ⋂                                      ”                                                        ⟨        ∀        S        ::        S        ∈        A                ⇒                x        ∈        S        ⟩                            ⇐                                    “                                          A            ⊆            B                                , so by the definition of                                   ⊆                                ,                                                                                      “                                                            T            ∈            A            ⇒            T            ∈            B                                 for any                                   T                                ; logic                ”                                                        ⟨        ∀        S        ::        S        ∈        B                ⇒                x        ∈        S        ⟩                            ≡                                    “                  definition of                                   ⋂                                      ”                                                x        ∈        ⋂        B            Step 2Or equivalently, by the definition of     ⊆  ,     ⋂  B  ⊆  ⋂  A  .Note that weakening the antecedent of     ⇒   (from     S  ∈  A   to     S  ∈  B  ), causes the expression     S  ∈  A    ⇒    x  ∈  S   as a whole to be strengthened, and therefore the middle step uses     ⇐  , &#039;flipping&#039; the direction of the implication.