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	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∩ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ssv	⊢ 𝑋 ⊆ V
2		int0	⊢ ∩ ∅ = V
3	1 2	sseqtrri	⊢ 𝑋 ⊆ ∩ ∅
4		df-ss	⊢ ( 𝑋 ⊆ ∩ ∅ ↔ ( 𝑋 ∩ ∩ ∅ ) = 𝑋 )
5	3 4	mpbi	⊢ ( 𝑋 ∩ ∩ ∅ ) = 𝑋
6	5	eqcomi	⊢ 𝑋 = ( 𝑋 ∩ ∩ ∅ )
7	6	eleq1i	⊢ ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ ∅ ) ∈ 𝐵 )
8	7	a1i	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( 𝑋 ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ ∅ ) ∈ 𝐵 ) )
9		eldifsn	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ≠ ∅ ) )
10		sstr2	⊢ ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊆ 𝒫 𝑋 → 𝑥 ⊆ 𝒫 𝑋 ) )
11		intss2	⊢ ( 𝑥 ⊆ 𝒫 𝑋 → ( 𝑥 ≠ ∅ → ∩ 𝑥 ⊆ 𝑋 ) )
12	10 11	syl6	⊢ ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊆ 𝒫 𝑋 → ( 𝑥 ≠ ∅ → ∩ 𝑥 ⊆ 𝑋 ) ) )
13		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
14	12 13	syl11	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( 𝑥 ∈ 𝒫 𝐴 → ( 𝑥 ≠ ∅ → ∩ 𝑥 ⊆ 𝑋 ) ) )
15	14	impd	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ⊆ 𝑋 ) )
16	9 15	syl5bi	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ∩ 𝑥 ⊆ 𝑋 ) )
17		df-ss	⊢ ( ∩ 𝑥 ⊆ 𝑋 ↔ ( ∩ 𝑥 ∩ 𝑋 ) = ∩ 𝑥 )
18		incom	⊢ ( ∩ 𝑥 ∩ 𝑋 ) = ( 𝑋 ∩ ∩ 𝑥 )
19	18	eqeq1i	⊢ ( ( ∩ 𝑥 ∩ 𝑋 ) = ∩ 𝑥 ↔ ( 𝑋 ∩ ∩ 𝑥 ) = ∩ 𝑥 )
20		eqcom	⊢ ( ( 𝑋 ∩ ∩ 𝑥 ) = ∩ 𝑥 ↔ ∩ 𝑥 = ( 𝑋 ∩ ∩ 𝑥 ) )
21	19 20	sylbb	⊢ ( ( ∩ 𝑥 ∩ 𝑋 ) = ∩ 𝑥 → ∩ 𝑥 = ( 𝑋 ∩ ∩ 𝑥 ) )
22	17 21	sylbi	⊢ ( ∩ 𝑥 ⊆ 𝑋 → ∩ 𝑥 = ( 𝑋 ∩ ∩ 𝑥 ) )
23		eleq1	⊢ ( ∩ 𝑥 = ( 𝑋 ∩ ∩ 𝑥 ) → ( ∩ 𝑥 ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) )
24	23	a1i	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( ∩ 𝑥 = ( 𝑋 ∩ ∩ 𝑥 ) → ( ∩ 𝑥 ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) ) )
25	22 24	syl5	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( ∩ 𝑥 ⊆ 𝑋 → ( ∩ 𝑥 ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) ) )
26	16 25	syld	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) → ( ∩ 𝑥 ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) ) )
27	26	ralrimiv	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ∩ 𝑥 ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) )
28		ralbi	⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( ∩ 𝑥 ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∩ 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) )
29	27 28	syl	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∩ 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) )
30	8 29	anbi12d	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∩ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑋 ∩ ∩ ∅ ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) ) )
31	30	biancomd	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∩ 𝑥 ∈ 𝐵 ) ↔ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ∧ ( 𝑋 ∩ ∩ ∅ ) ∈ 𝐵 ) ) )
32		0elpw	⊢ ∅ ∈ 𝒫 𝐴
33		inteq	⊢ ( 𝑥 = ∅ → ∩ 𝑥 = ∩ ∅ )
34		ineq2	⊢ ( ∩ 𝑥 = ∩ ∅ → ( 𝑋 ∩ ∩ 𝑥 ) = ( 𝑋 ∩ ∩ ∅ ) )
35		eleq1	⊢ ( ( 𝑋 ∩ ∩ 𝑥 ) = ( 𝑋 ∩ ∩ ∅ ) → ( ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ ∅ ) ∈ 𝐵 ) )
36	33 34 35	3syl	⊢ ( 𝑥 = ∅ → ( ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ↔ ( 𝑋 ∩ ∩ ∅ ) ∈ 𝐵 ) )
37	36	bj-raldifsn	⊢ ( ∅ ∈ 𝒫 𝐴 → ( ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ↔ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ∧ ( 𝑋 ∩ ∩ ∅ ) ∈ 𝐵 ) ) )
38	32 37	ax-mp	⊢ ( ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ↔ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ∧ ( 𝑋 ∩ ∩ ∅ ) ∈ 𝐵 ) )
39	31 38	bitr4di	⊢ ( 𝐴 ⊆ 𝒫 𝑋 → ( ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ∩ 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝒫 𝐴 ( 𝑋 ∩ ∩ 𝑥 ) ∈ 𝐵 ) )