intsal

Description: The arbitrary intersection of sigma-algebra (on the same set X ) is a sigma-algebra ( on the same set X , see intsaluni ). (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	intsal.ga	$⊢ φ \to G \subseteq SAlg$
	intsal.gn0	$⊢ φ \to G \neq \emptyset$
	intsal.x	$⊢ (φ \land s \in G) \to ⋃ s = X$
Assertion	intsal	$⊢ φ \to ⋂ G \in SAlg$

Proof

Step	Hyp	Ref	Expression
1		intsal.ga	$⊢ φ \to G \subseteq SAlg$
2		intsal.gn0	$⊢ φ \to G \neq \emptyset$
3		intsal.x	$⊢ (φ \land s \in G) \to ⋃ s = X$
4		simpl	$⊢ (φ \land s \in G) \to φ$
5	1	sselda	$⊢ (φ \land s \in G) \to s \in SAlg$
6		simpr	$⊢ (φ \land s \in SAlg) \to s \in SAlg$
7		0sal	$⊢ s \in SAlg \to \emptyset \in s$
8	6 7	syl	$⊢ (φ \land s \in SAlg) \to \emptyset \in s$
9	4 5 8	syl2anc	$⊢ (φ \land s \in G) \to \emptyset \in s$
10	9	ralrimiva	$⊢ φ \to \forall s \in G \emptyset \in s$
11		0ex	$⊢ \emptyset \in V$
12	11	elint2	$⊢ \emptyset \in ⋂ G \leftrightarrow \forall s \in G \emptyset \in s$
13	10 12	sylibr	$⊢ φ \to \emptyset \in ⋂ G$
14	1 2 3	intsaluni	$⊢ φ \to ⋃ ⋂ G = X$
15	14	eqcomd	$⊢ φ \to X = ⋃ ⋂ G$
16	15	adantr	$⊢ (φ \land s \in G) \to X = ⋃ ⋂ G$
17	3 16	eqtr2d	$⊢ (φ \land s \in G) \to ⋃ ⋂ G = ⋃ s$
18	17	difeq1d	$⊢ (φ \land s \in G) \to ⋃ ⋂ G ∖ y = ⋃ s ∖ y$
19	18	adantlr	$⊢ ((φ \land y \in ⋂ G) \land s \in G) \to ⋃ ⋂ G ∖ y = ⋃ s ∖ y$
20	5	adantlr	$⊢ ((φ \land y \in ⋂ G) \land s \in G) \to s \in SAlg$
21		elinti	$⊢ y \in ⋂ G \to (s \in G \to y \in s)$
22	21	imp	$⊢ (y \in ⋂ G \land s \in G) \to y \in s$
23	22	adantll	$⊢ ((φ \land y \in ⋂ G) \land s \in G) \to y \in s$
24		saldifcl	$⊢ (s \in SAlg \land y \in s) \to ⋃ s ∖ y \in s$
25	20 23 24	syl2anc	$⊢ ((φ \land y \in ⋂ G) \land s \in G) \to ⋃ s ∖ y \in s$
26	19 25	eqeltrd	$⊢ ((φ \land y \in ⋂ G) \land s \in G) \to ⋃ ⋂ G ∖ y \in s$
27	26	ralrimiva	$⊢ (φ \land y \in ⋂ G) \to \forall s \in G ⋃ ⋂ G ∖ y \in s$
28		intex	$⊢ G \neq \emptyset \leftrightarrow ⋂ G \in V$
29	28	biimpi	$⊢ G \neq \emptyset \to ⋂ G \in V$
30	2 29	syl	$⊢ φ \to ⋂ G \in V$
31	30	uniexd	$⊢ φ \to ⋃ ⋂ G \in V$
32	31	difexd	$⊢ φ \to ⋃ ⋂ G ∖ y \in V$
33	32	adantr	$⊢ (φ \land y \in ⋂ G) \to ⋃ ⋂ G ∖ y \in V$
34		elintg	$⊢ ⋃ ⋂ G ∖ y \in V \to (⋃ ⋂ G ∖ y \in ⋂ G \leftrightarrow \forall s \in G ⋃ ⋂ G ∖ y \in s)$
35	33 34	syl	$⊢ (φ \land y \in ⋂ G) \to (⋃ ⋂ G ∖ y \in ⋂ G \leftrightarrow \forall s \in G ⋃ ⋂ G ∖ y \in s)$
36	27 35	mpbird	$⊢ (φ \land y \in ⋂ G) \to ⋃ ⋂ G ∖ y \in ⋂ G$
37	36	ralrimiva	$⊢ φ \to \forall y \in ⋂ G ⋃ ⋂ G ∖ y \in ⋂ G$
38	5	ad4ant14	$⊢ (((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \land s \in G) \to s \in SAlg$
39		elpwi	$⊢ y \in 𝒫 ⋂ G \to y \subseteq ⋂ G$
40	39	adantr	$⊢ (y \in 𝒫 ⋂ G \land s \in G) \to y \subseteq ⋂ G$
41		intss1	$⊢ s \in G \to ⋂ G \subseteq s$
42	41	adantl	$⊢ (y \in 𝒫 ⋂ G \land s \in G) \to ⋂ G \subseteq s$
43	40 42	sstrd	$⊢ (y \in 𝒫 ⋂ G \land s \in G) \to y \subseteq s$
44		vex	$⊢ y \in V$
45	44	elpw	$⊢ y \in 𝒫 s \leftrightarrow y \subseteq s$
46	43 45	sylibr	$⊢ (y \in 𝒫 ⋂ G \land s \in G) \to y \in 𝒫 s$
47	46	adantll	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land s \in G) \to y \in 𝒫 s$
48	47	adantlr	$⊢ (((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \land s \in G) \to y \in 𝒫 s$
49		simplr	$⊢ (((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \land s \in G) \to y ≼ ω$
50	38 48 49	salunicl	$⊢ (((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \land s \in G) \to ⋃ y \in s$
51	50	ralrimiva	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \to \forall s \in G ⋃ y \in s$
52		vuniex	$⊢ ⋃ y \in V$
53	52	a1i	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \to ⋃ y \in V$
54		elintg	$⊢ ⋃ y \in V \to (⋃ y \in ⋂ G \leftrightarrow \forall s \in G ⋃ y \in s)$
55	53 54	syl	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \to (⋃ y \in ⋂ G \leftrightarrow \forall s \in G ⋃ y \in s)$
56	51 55	mpbird	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \to ⋃ y \in ⋂ G$
57	56	ex	$⊢ (φ \land y \in 𝒫 ⋂ G) \to (y ≼ ω \to ⋃ y \in ⋂ G)$
58	57	ralrimiva	$⊢ φ \to \forall y \in 𝒫 ⋂ G (y ≼ ω \to ⋃ y \in ⋂ G)$
59	13 37 58	3jca	$⊢ φ \to (\emptyset \in ⋂ G \land \forall y \in ⋂ G ⋃ ⋂ G ∖ y \in ⋂ G \land \forall y \in 𝒫 ⋂ G (y ≼ ω \to ⋃ y \in ⋂ G))$
60		issal	$⊢ ⋂ G \in V \to (⋂ G \in SAlg \leftrightarrow (\emptyset \in ⋂ G \land \forall y \in ⋂ G ⋃ ⋂ G ∖ y \in ⋂ G \land \forall y \in 𝒫 ⋂ G (y ≼ ω \to ⋃ y \in ⋂ G)))$
61	30 60	syl	$⊢ φ \to (⋂ G \in SAlg \leftrightarrow (\emptyset \in ⋂ G \land \forall y \in ⋂ G ⋃ ⋂ G ∖ y \in ⋂ G \land \forall y \in 𝒫 ⋂ G (y ≼ ω \to ⋃ y \in ⋂ G)))$
62	59 61	mpbird	$⊢ φ \to ⋂ G \in SAlg$

Metamath Proof Explorer

Theorem intsal

Proof