Theorem intsal 44561

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

Hypotheses

Ref	Expression
intsal.ga	⊢ (𝜑 → 𝐺 ⊆ SAlg)
intsal.gn0	⊢ (𝜑 → 𝐺 ≠ ∅)
intsal.x	⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)

Assertion

Ref	Expression
intsal	⊢ (𝜑 → ∩ 𝐺 ∈ SAlg)

Distinct variable groups:   𝐺,𝑠   𝑋,𝑠   𝜑,𝑠

Proof of Theorem intsal

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝜑)
2		intsal.ga	. . . . . . 7 ⊢ (𝜑 → 𝐺 ⊆ SAlg)
3	2	sselda 3944	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
4		simpr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → 𝑠 ∈ SAlg)
5		0sal 44551	. . . . . . 7 ⊢ (𝑠 ∈ SAlg → ∅ ∈ 𝑠)
6	4, 5	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → ∅ ∈ 𝑠)
7	1, 3, 6	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∅ ∈ 𝑠)
8	7	ralrimiva 3143	. . . 4 ⊢ (𝜑 → ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠)
9		0ex 5264	. . . . 5 ⊢ ∅ ∈ V
10	9	elint2 4914	. . . 4 ⊢ (∅ ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠)
11	8, 10	sylibr 233	. . 3 ⊢ (𝜑 → ∅ ∈ ∩ 𝐺)
12		intsal.x	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)
13		intsal.gn0	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ≠ ∅)
14	2, 13, 12	intsaluni 44560	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋)
15	14	eqcomd 2742	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ∪ ∩ 𝐺)
16	15	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑋 = ∪ ∩ 𝐺)
17	12, 16	eqtr2d 2777	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ ∩ 𝐺 = ∪ 𝑠)
18	17	difeq1d 4081	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) = (∪ 𝑠 ∖ 𝑦))
19	18	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) = (∪ 𝑠 ∖ 𝑦))
20	3	adantlr 713	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
21		elinti 4916	. . . . . . . . . 10 ⊢ (𝑦 ∈ ∩ 𝐺 → (𝑠 ∈ 𝐺 → 𝑦 ∈ 𝑠))
22	21	imp 407	. . . . . . . . 9 ⊢ ((𝑦 ∈ ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠)
23	22	adantll 712	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠)
24		saldifcl 44550	. . . . . . . 8 ⊢ ((𝑠 ∈ SAlg ∧ 𝑦 ∈ 𝑠) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠)
25	20, 23, 24	syl2anc 584	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠)
26	19, 25	eqeltrd 2838	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠)
27	26	ralrimiva 3143	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠)
28		intex 5294	. . . . . . . . . . 11 ⊢ (𝐺 ≠ ∅ ↔ ∩ 𝐺 ∈ V)
29	28	biimpi 215	. . . . . . . . . 10 ⊢ (𝐺 ≠ ∅ → ∩ 𝐺 ∈ V)
30	13, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∩ 𝐺 ∈ V)
31	30	uniexd 7679	. . . . . . . 8 ⊢ (𝜑 → ∪ ∩ 𝐺 ∈ V)
32	31	difexd 5286	. . . . . . 7 ⊢ (𝜑 → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V)
33	32	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V)
34		elintg 4915	. . . . . 6 ⊢ ((∪ ∩ 𝐺 ∖ 𝑦) ∈ V → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠))
35	33, 34	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠))
36	27, 35	mpbird 256	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺)
37	36	ralrimiva 3143	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺)
38	3	ad4ant14 750	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
39		elpwi 4567	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 ∩ 𝐺 → 𝑦 ⊆ ∩ 𝐺)
40	39	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ ∩ 𝐺)
41		intss1 4924	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ 𝐺 → ∩ 𝐺 ⊆ 𝑠)
42	41	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → ∩ 𝐺 ⊆ 𝑠)
43	40, 42	sstrd 3954	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ 𝑠)
44		vex 3449	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
45	44	elpw 4564	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 𝑠 ↔ 𝑦 ⊆ 𝑠)
46	43, 45	sylibr 233	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
47	46	adantll 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
48	47	adantlr 713	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
49		simplr 767	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑦 ≼ ω)
50	38, 48, 49	salunicl 44547	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → ∪ 𝑦 ∈ 𝑠)
51	50	ralrimiva 3143	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠)
52		vuniex 7676	. . . . . . . 8 ⊢ ∪ 𝑦 ∈ V
53	52	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ V)
54		elintg 4915	. . . . . . 7 ⊢ (∪ 𝑦 ∈ V → (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠))
55	53, 54	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠))
56	51, 55	mpbird 256	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ ∩ 𝐺)
57	56	ex 413	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) → (𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))
58	57	ralrimiva 3143	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))
59	11, 37, 58	3jca 1128	. 2 ⊢ (𝜑 → (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺)))
60		issal 44545	. . 3 ⊢ (∩ 𝐺 ∈ V → (∩ 𝐺 ∈ SAlg ↔ (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))))
61	30, 60	syl 17	. 2 ⊢ (𝜑 → (∩ 𝐺 ∈ SAlg ↔ (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))))
62	59, 61	mpbird 256	1 ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  Vcvv 3445   ∖ cdif 3907   ⊆ wss 3910  ∅c0 4282  𝒫 cpw 4560  ∪ cuni 4865  ∩ cint 4907   class class class wbr 5105  ωcom 7802   ≼ cdom 8881  SAlgcsalg 44539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-br 5106  df-salg 44540

This theorem is referenced by:  salgencl  44563