Metamath Proof Explorer

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 df-ss 
 |-  ( 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 syl5bi 
 |-  ( A C_ ~P X -> ( x e. ( ~P A \ { (/) } ) -> |^| x C_ X ) )
17 df-ss 
 |-  ( |^| 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 ) )