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 C_ ~P X -> ( ( X e. B /\ A. x e. ( ~P A \ { (/) } ) |^| x e. B ) <-> A. x e. ~P A ( X i^i |^| x ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		ssv	|- X C_ _V
2		int0	|- |^| (/) = _V
3	1 2	sseqtrri	|- X C_ |^| (/)
4		dfss2	|- ( X C_ |^| (/) <-> ( X i^i |^| (/) ) = X )
5	3 4	mpbi	|- ( X i^i |^| (/) ) = X
6	5	eqcomi	|- X = ( X i^i |^| (/) )
7	6	eleq1i	|- ( X e. B <-> ( X i^i |^| (/) ) e. B )
8	7	a1i	|- ( A C_ ~P X -> ( X e. B <-> ( X i^i |^| (/) ) e. B ) )
9		eldifsn	|- ( x e. ( ~P A \ { (/) } ) <-> ( x e. ~P A /\ x =/= (/) ) )
10		sstr2	|- ( x C_ A -> ( A C_ ~P X -> x C_ ~P X ) )
11		intss2	|- ( x C_ ~P X -> ( x =/= (/) -> |^| x C_ X ) )
12	10 11	syl6	|- ( x C_ A -> ( A C_ ~P X -> ( x =/= (/) -> |^| x C_ X ) ) )
13		elpwi	|- ( x e. ~P A -> x C_ A )
14	12 13	syl11	|- ( A C_ ~P X -> ( x e. ~P A -> ( x =/= (/) -> |^| x C_ X ) ) )
15	14	impd	|- ( A C_ ~P X -> ( ( x e. ~P A /\ x =/= (/) ) -> |^| x C_ X ) )
16	9 15	biimtrid	|- ( A C_ ~P X -> ( x e. ( ~P A \ { (/) } ) -> |^| x C_ X ) )
17		dfss2	|- ( |^| x C_ X <-> ( |^| x i^i X ) = |^| x )
18		incom	|- ( |^| x i^i X ) = ( X i^i |^| x )
19	18	eqeq1i	|- ( ( |^| x i^i X ) = |^| x <-> ( X i^i |^| x ) = |^| x )
20		eqcom	|- ( ( X i^i |^| x ) = |^| x <-> |^| x = ( X i^i |^| x ) )
21	19 20	sylbb	|- ( ( |^| x i^i X ) = |^| x -> |^| x = ( X i^i |^| x ) )
22	17 21	sylbi	|- ( |^| x C_ X -> |^| x = ( X i^i |^| x ) )
23		eleq1	|- ( |^| x = ( X i^i |^| x ) -> ( |^| x e. B <-> ( X i^i |^| x ) e. B ) )
24	23	a1i	|- ( A C_ ~P X -> ( |^| x = ( X i^i |^| x ) -> ( |^| x e. B <-> ( X i^i |^| x ) e. B ) ) )
25	22 24	syl5	|- ( A C_ ~P X -> ( |^| x C_ X -> ( |^| x e. B <-> ( X i^i |^| x ) e. B ) ) )
26	16 25	syld	|- ( A C_ ~P X -> ( x e. ( ~P A \ { (/) } ) -> ( |^| x e. B <-> ( X i^i |^| x ) e. B ) ) )
27	26	ralrimiv	|- ( A C_ ~P X -> A. x e. ( ~P A \ { (/) } ) ( |^| x e. B <-> ( X i^i |^| x ) e. B ) )
28		ralbi	|- ( A. x e. ( ~P A \ { (/) } ) ( |^| x e. B <-> ( X i^i |^| x ) e. B ) -> ( A. x e. ( ~P A \ { (/) } ) |^| x e. B <-> A. x e. ( ~P A \ { (/) } ) ( X i^i |^| x ) e. B ) )
29	27 28	syl	|- ( A C_ ~P X -> ( A. x e. ( ~P A \ { (/) } ) |^| x e. B <-> A. x e. ( ~P A \ { (/) } ) ( X i^i |^| x ) e. B ) )
30	8 29	anbi12d	|- ( A C_ ~P X -> ( ( X e. B /\ A. x e. ( ~P A \ { (/) } ) |^| x e. B ) <-> ( ( X i^i |^| (/) ) e. B /\ A. x e. ( ~P A \ { (/) } ) ( X i^i |^| x ) e. B ) ) )
31	30	biancomd	|- ( A C_ ~P X -> ( ( X e. B /\ A. x e. ( ~P A \ { (/) } ) |^| x e. B ) <-> ( A. x e. ( ~P A \ { (/) } ) ( X i^i |^| x ) e. B /\ ( X i^i |^| (/) ) e. B ) ) )
32		0elpw	|- (/) e. ~P A
33		inteq	|- ( x = (/) -> |^| x = |^| (/) )
34		ineq2	|- ( |^| x = |^| (/) -> ( X i^i |^| x ) = ( X i^i |^| (/) ) )
35		eleq1	|- ( ( X i^i |^| x ) = ( X i^i |^| (/) ) -> ( ( X i^i |^| x ) e. B <-> ( X i^i |^| (/) ) e. B ) )
36	33 34 35	3syl	|- ( x = (/) -> ( ( X i^i |^| x ) e. B <-> ( X i^i |^| (/) ) e. B ) )
37	36	bj-raldifsn	|- ( (/) e. ~P A -> ( A. x e. ~P A ( X i^i |^| x ) e. B <-> ( A. x e. ( ~P A \ { (/) } ) ( X i^i |^| x ) e. B /\ ( X i^i |^| (/) ) e. B ) ) )
38	32 37	ax-mp	|- ( A. x e. ~P A ( X i^i |^| x ) e. B <-> ( A. x e. ( ~P A \ { (/) } ) ( X i^i |^| x ) e. B /\ ( X i^i |^| (/) ) e. B ) )
39	31 38	bitr4di	|- ( A C_ ~P X -> ( ( X e. B /\ A. x e. ( ~P A \ { (/) } ) |^| x e. B ) <-> A. x e. ~P A ( X i^i |^| x ) e. B ) )