Theorem 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 \left(\left(X\in B\wedge \forall x\in \left(𝒫A\setminus \left\{\varnothing \right\}\right)\bigcap x\in B\right)\leftrightarrow \forall x\in 𝒫AX\cap \bigcap x\in B\right)$$

Proof

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