Theorem intsal 42970

Description: The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 42969). (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 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝜑)
2		intsal.ga	. . . . . . 7 ⊢ (𝜑 → 𝐺 ⊆ SAlg)
3	2	sselda 3915	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
4		simpr 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → 𝑠 ∈ SAlg)
5		0sal 42962	. . . . . . 7 ⊢ (𝑠 ∈ SAlg → ∅ ∈ 𝑠)
6	4, 5	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → ∅ ∈ 𝑠)
7	1, 3, 6	syl2anc 587	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∅ ∈ 𝑠)
8	7	ralrimiva 3149	. . . 4 ⊢ (𝜑 → ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠)
9		0ex 5175	. . . . 5 ⊢ ∅ ∈ V
10	9	elint2 4845	. . . 4 ⊢ (∅ ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠)
11	8, 10	sylibr 237	. . 3 ⊢ (𝜑 → ∅ ∈ ∩ 𝐺)
12		intsal.x	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)
13		intsal.gn0	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ≠ ∅)
14	2, 13, 12	intsaluni 42969	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋)
15	14	eqcomd 2804	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ∪ ∩ 𝐺)
16	15	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑋 = ∪ ∩ 𝐺)
17	12, 16	eqtr2d 2834	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ ∩ 𝐺 = ∪ 𝑠)
18	17	difeq1d 4049	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) = (∪ 𝑠 ∖ 𝑦))
19	18	adantlr 714	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) = (∪ 𝑠 ∖ 𝑦))
20	3	adantlr 714	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
21		elinti 4847	. . . . . . . . . 10 ⊢ (𝑦 ∈ ∩ 𝐺 → (𝑠 ∈ 𝐺 → 𝑦 ∈ 𝑠))
22	21	imp 410	. . . . . . . . 9 ⊢ ((𝑦 ∈ ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠)
23	22	adantll 713	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠)
24		saldifcl 42961	. . . . . . . 8 ⊢ ((𝑠 ∈ SAlg ∧ 𝑦 ∈ 𝑠) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠)
25	20, 23, 24	syl2anc 587	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠)
26	19, 25	eqeltrd 2890	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠)
27	26	ralrimiva 3149	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠)
28		intex 5204	. . . . . . . . . . 11 ⊢ (𝐺 ≠ ∅ ↔ ∩ 𝐺 ∈ V)
29	28	biimpi 219	. . . . . . . . . 10 ⊢ (𝐺 ≠ ∅ → ∩ 𝐺 ∈ V)
30	13, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∩ 𝐺 ∈ V)
31	30	uniexd 7448	. . . . . . . 8 ⊢ (𝜑 → ∪ ∩ 𝐺 ∈ V)
32		difexg 5195	. . . . . . . 8 ⊢ (∪ ∩ 𝐺 ∈ V → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V)
33	31, 32	syl 17	. . . . . . 7 ⊢ (𝜑 → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V)
34	33	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V)
35		elintg 4846	. . . . . 6 ⊢ ((∪ ∩ 𝐺 ∖ 𝑦) ∈ V → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠))
36	34, 35	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠))
37	27, 36	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺)
38	37	ralrimiva 3149	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺)
39	3	ad4ant14 751	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
40		elpwi 4506	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 ∩ 𝐺 → 𝑦 ⊆ ∩ 𝐺)
41	40	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ ∩ 𝐺)
42		intss1 4853	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ 𝐺 → ∩ 𝐺 ⊆ 𝑠)
43	42	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → ∩ 𝐺 ⊆ 𝑠)
44	41, 43	sstrd 3925	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ 𝑠)
45		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
46	45	elpw 4501	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 𝑠 ↔ 𝑦 ⊆ 𝑠)
47	44, 46	sylibr 237	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
48	47	adantll 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
49	48	adantlr 714	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
50		simplr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑦 ≼ ω)
51	39, 49, 50	salunicl 42958	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → ∪ 𝑦 ∈ 𝑠)
52	51	ralrimiva 3149	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠)
53		vuniex 7445	. . . . . . . 8 ⊢ ∪ 𝑦 ∈ V
54	53	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ V)
55		elintg 4846	. . . . . . 7 ⊢ (∪ 𝑦 ∈ V → (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠))
56	54, 55	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠))
57	52, 56	mpbird 260	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ ∩ 𝐺)
58	57	ex 416	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) → (𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))
59	58	ralrimiva 3149	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))
60	11, 38, 59	3jca 1125	. 2 ⊢ (𝜑 → (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺)))
61		issal 42956	. . 3 ⊢ (∩ 𝐺 ∈ V → (∩ 𝐺 ∈ SAlg ↔ (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))))
62	30, 61	syl 17	. 2 ⊢ (𝜑 → (∩ 𝐺 ∈ SAlg ↔ (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))))
63	60, 62	mpbird 260	1 ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  Vcvv 3441   ∖ cdif 3878   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  ∪ cuni 4800  ∩ cint 4838   class class class wbr 5030  ωcom 7560   ≼ cdom 8490  SAlgcsalg 42950

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-int 4839  df-br 5031  df-salg 42951

This theorem is referenced by:  salgencl  42972