bj-0int

Description: If A is a collection of subsets of X , like a Moore collection or a topology, two equivalent ways to say that arbitrary intersections of elements of A relative to X belong to some class B : the LHS singles out the empty intersection (the empty intersection relative to X is X and the intersection of a nonempty family of subsets of X is included in X , so there is no need to intersect it with X ). In typical applications, B is A itself. (Contributed by BJ, 7-Dec-2021)

		Ref	Expression
	Assertion	bj-0int	$⊢ A \subseteq 𝒫 X \to ((X \in B \land \forall x \in (𝒫 A ∖ \{\emptyset\}) ⋂ x \in B) \leftrightarrow \forall x \in 𝒫 A X \cap ⋂ x \in B)$

Proof

Step	Hyp	Ref	Expression
1		ssv	$⊢ X \subseteq V$
2		int0	$⊢ ⋂ \emptyset = V$
3	1 2	sseqtrri	$⊢ X \subseteq ⋂ \emptyset$
4		df-ss	$⊢ X \subseteq ⋂ \emptyset \leftrightarrow X \cap ⋂ \emptyset = X$
5	3 4	mpbi	$⊢ X \cap ⋂ \emptyset = X$
6	5	eqcomi	$⊢ X = X \cap ⋂ \emptyset$
7	6	eleq1i	$⊢ X \in B \leftrightarrow X \cap ⋂ \emptyset \in B$
8	7	a1i	$⊢ A \subseteq 𝒫 X \to (X \in B \leftrightarrow X \cap ⋂ \emptyset \in B)$
9		eldifsn	$⊢ x \in (𝒫 A ∖ \{\emptyset\}) \leftrightarrow (x \in 𝒫 A \land x \neq \emptyset)$
10		sstr2	$⊢ x \subseteq A \to (A \subseteq 𝒫 X \to x \subseteq 𝒫 X)$
11		intss2	$⊢ x \subseteq 𝒫 X \to (x \neq \emptyset \to ⋂ x \subseteq X)$
12	10 11	syl6	$⊢ x \subseteq A \to (A \subseteq 𝒫 X \to (x \neq \emptyset \to ⋂ x \subseteq X))$
13		elpwi	$⊢ x \in 𝒫 A \to x \subseteq A$
14	12 13	syl11	$⊢ A \subseteq 𝒫 X \to (x \in 𝒫 A \to (x \neq \emptyset \to ⋂ x \subseteq X))$
15	14	impd	$⊢ A \subseteq 𝒫 X \to ((x \in 𝒫 A \land x \neq \emptyset) \to ⋂ x \subseteq X)$
16	9 15	syl5bi	$⊢ A \subseteq 𝒫 X \to (x \in (𝒫 A ∖ \{\emptyset\}) \to ⋂ x \subseteq X)$
17		df-ss	$⊢ ⋂ x \subseteq X \leftrightarrow ⋂ x \cap X = ⋂ x$
18		incom	$⊢ ⋂ x \cap X = X \cap ⋂ x$
19	18	eqeq1i	$⊢ ⋂ x \cap X = ⋂ x \leftrightarrow X \cap ⋂ x = ⋂ x$
20		eqcom	$⊢ X \cap ⋂ x = ⋂ x \leftrightarrow ⋂ x = X \cap ⋂ x$
21	19 20	sylbb	$⊢ ⋂ x \cap X = ⋂ x \to ⋂ x = X \cap ⋂ x$
22	17 21	sylbi	$⊢ ⋂ x \subseteq X \to ⋂ x = X \cap ⋂ x$
23		eleq1	$⊢ ⋂ x = X \cap ⋂ x \to (⋂ x \in B \leftrightarrow X \cap ⋂ x \in B)$
24	23	a1i	$⊢ A \subseteq 𝒫 X \to (⋂ x = X \cap ⋂ x \to (⋂ x \in B \leftrightarrow X \cap ⋂ x \in B))$
25	22 24	syl5	$⊢ A \subseteq 𝒫 X \to (⋂ x \subseteq X \to (⋂ x \in B \leftrightarrow X \cap ⋂ x \in B))$
26	16 25	syld	$⊢ A \subseteq 𝒫 X \to (x \in (𝒫 A ∖ \{\emptyset\}) \to (⋂ x \in B \leftrightarrow X \cap ⋂ x \in B))$
27	26	ralrimiv	$⊢ A \subseteq 𝒫 X \to \forall x \in (𝒫 A ∖ \{\emptyset\}) (⋂ x \in B \leftrightarrow X \cap ⋂ x \in B)$
28		ralbi	$⊢ \forall x \in (𝒫 A ∖ \{\emptyset\}) (⋂ x \in B \leftrightarrow X \cap ⋂ x \in B) \to (\forall x \in (𝒫 A ∖ \{\emptyset\}) ⋂ x \in B \leftrightarrow \forall x \in (𝒫 A ∖ \{\emptyset\}) X \cap ⋂ x \in B)$
29	27 28	syl	$⊢ A \subseteq 𝒫 X \to (\forall x \in (𝒫 A ∖ \{\emptyset\}) ⋂ x \in B \leftrightarrow \forall x \in (𝒫 A ∖ \{\emptyset\}) X \cap ⋂ x \in B)$
30	8 29	anbi12d	$⊢ A \subseteq 𝒫 X \to ((X \in B \land \forall x \in (𝒫 A ∖ \{\emptyset\}) ⋂ x \in B) \leftrightarrow (X \cap ⋂ \emptyset \in B \land \forall x \in (𝒫 A ∖ \{\emptyset\}) X \cap ⋂ x \in B))$
31	30	biancomd	$⊢ A \subseteq 𝒫 X \to ((X \in B \land \forall x \in (𝒫 A ∖ \{\emptyset\}) ⋂ x \in B) \leftrightarrow (\forall x \in (𝒫 A ∖ \{\emptyset\}) X \cap ⋂ x \in B \land X \cap ⋂ \emptyset \in B))$
32		0elpw	$⊢ \emptyset \in 𝒫 A$
33		inteq	$⊢ x = \emptyset \to ⋂ x = ⋂ \emptyset$
34		ineq2	$⊢ ⋂ x = ⋂ \emptyset \to X \cap ⋂ x = X \cap ⋂ \emptyset$
35		eleq1	$⊢ X \cap ⋂ x = X \cap ⋂ \emptyset \to (X \cap ⋂ x \in B \leftrightarrow X \cap ⋂ \emptyset \in B)$
36	33 34 35	3syl	$⊢ x = \emptyset \to (X \cap ⋂ x \in B \leftrightarrow X \cap ⋂ \emptyset \in B)$
37	36	bj-raldifsn	$⊢ \emptyset \in 𝒫 A \to (\forall x \in 𝒫 A X \cap ⋂ x \in B \leftrightarrow (\forall x \in (𝒫 A ∖ \{\emptyset\}) X \cap ⋂ x \in B \land X \cap ⋂ \emptyset \in B))$
38	32 37	ax-mp	$⊢ \forall x \in 𝒫 A X \cap ⋂ x \in B \leftrightarrow (\forall x \in (𝒫 A ∖ \{\emptyset\}) X \cap ⋂ x \in B \land X \cap ⋂ \emptyset \in B)$
39	31 38	bitr4di	$⊢ A \subseteq 𝒫 X \to ((X \in B \land \forall x \in (𝒫 A ∖ \{\emptyset\}) ⋂ x \in B) \leftrightarrow \forall x \in 𝒫 A X \cap ⋂ x \in B)$

Metamath Proof Explorer

Theorem bj-0int

Proof