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		difexg	$⊢ ⋃ ⋂ G \in V \to ⋃ ⋂ G ∖ y \in V$
33	31 32	syl	$⊢ φ \to ⋃ ⋂ G ∖ y \in V$
34	33	adantr	$⊢ (φ \land y \in ⋂ G) \to ⋃ ⋂ G ∖ y \in V$
35		elintg	$⊢ ⋃ ⋂ G ∖ y \in V \to (⋃ ⋂ G ∖ y \in ⋂ G \leftrightarrow \forall s \in G ⋃ ⋂ G ∖ y \in s)$
36	34 35	syl	$⊢ (φ \land y \in ⋂ G) \to (⋃ ⋂ G ∖ y \in ⋂ G \leftrightarrow \forall s \in G ⋃ ⋂ G ∖ y \in s)$
37	27 36	mpbird	$⊢ (φ \land y \in ⋂ G) \to ⋃ ⋂ G ∖ y \in ⋂ G$
38	37	ralrimiva	$⊢ φ \to \forall y \in ⋂ G ⋃ ⋂ G ∖ y \in ⋂ G$
39	5	ad4ant14	$⊢ (((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \land s \in G) \to s \in SAlg$
40		elpwi	$⊢ y \in 𝒫 ⋂ G \to y \subseteq ⋂ G$
41	40	adantr	$⊢ (y \in 𝒫 ⋂ G \land s \in G) \to y \subseteq ⋂ G$
42		intss1	$⊢ s \in G \to ⋂ G \subseteq s$
43	42	adantl	$⊢ (y \in 𝒫 ⋂ G \land s \in G) \to ⋂ G \subseteq s$
44	41 43	sstrd	$⊢ (y \in 𝒫 ⋂ G \land s \in G) \to y \subseteq s$
45		vex	$⊢ y \in V$
46	45	elpw	$⊢ y \in 𝒫 s \leftrightarrow y \subseteq s$
47	44 46	sylibr	$⊢ (y \in 𝒫 ⋂ G \land s \in G) \to y \in 𝒫 s$
48	47	adantll	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land s \in G) \to y \in 𝒫 s$
49	48	adantlr	$⊢ (((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \land s \in G) \to y \in 𝒫 s$
50		simplr	$⊢ (((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \land s \in G) \to y ≼ ω$
51	39 49 50	salunicl	$⊢ (((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \land s \in G) \to ⋃ y \in s$
52	51	ralrimiva	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \to \forall s \in G ⋃ y \in s$
53		vuniex	$⊢ ⋃ y \in V$
54	53	a1i	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \to ⋃ y \in V$
55		elintg	$⊢ ⋃ y \in V \to (⋃ y \in ⋂ G \leftrightarrow \forall s \in G ⋃ y \in s)$
56	54 55	syl	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \to (⋃ y \in ⋂ G \leftrightarrow \forall s \in G ⋃ y \in s)$
57	52 56	mpbird	$⊢ ((φ \land y \in 𝒫 ⋂ G) \land y ≼ ω) \to ⋃ y \in ⋂ G$
58	57	ex	$⊢ (φ \land y \in 𝒫 ⋂ G) \to (y ≼ ω \to ⋃ y \in ⋂ G)$
59	58	ralrimiva	$⊢ φ \to \forall y \in 𝒫 ⋂ G (y ≼ ω \to ⋃ y \in ⋂ G)$
60	13 38 59	3jca	$⊢ φ \to (\emptyset \in ⋂ G \land \forall y \in ⋂ G ⋃ ⋂ G ∖ y \in ⋂ G \land \forall y \in 𝒫 ⋂ G (y ≼ ω \to ⋃ y \in ⋂ G))$
61		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)))$
62	30 61	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)))$
63	60 62	mpbird	$⊢ φ \to ⋂ G \in SAlg$

Metamath Proof Explorer

Theorem intsal

Proof