Theorem intsal 46868

Description: The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 46867). (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 3936	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
4		simpr 488	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → 𝑠 ∈ SAlg)
5		0sal 46858	. . . . . . 7 ⊢ (𝑠 ∈ SAlg → ∅ ∈ 𝑠)
6	4, 5	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → ∅ ∈ 𝑠)
7	1, 3, 6	syl2anc 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∅ ∈ 𝑠)
8	7	ralrimiva 3153	. . . 4 ⊢ (𝜑 → ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠)
9		0ex 5256	. . . . 5 ⊢ ∅ ∈ V
10	9	elint2 4911	. . . 4 ⊢ (∅ ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠)
11	8, 10	sylibr 236	. . 3 ⊢ (𝜑 → ∅ ∈ ∩ 𝐺)
12		intsal.x	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)
13		intsal.gn0	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ≠ ∅)
14	2, 13, 12	intsaluni 46867	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋)
15	14	eqcomd 2767	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ∪ ∩ 𝐺)
16	15	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑋 = ∪ ∩ 𝐺)
17	12, 16	eqtr2d 2797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ ∩ 𝐺 = ∪ 𝑠)
18	17	difeq1d 4079	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) = (∪ 𝑠 ∖ 𝑦))
19	18	adantlr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) = (∪ 𝑠 ∖ 𝑦))
20	3	adantlr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
21		elinti 4913	. . . . . . . . . 10 ⊢ (𝑦 ∈ ∩ 𝐺 → (𝑠 ∈ 𝐺 → 𝑦 ∈ 𝑠))
22	21	imp 410	. . . . . . . . 9 ⊢ ((𝑦 ∈ ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠)
23	22	adantll 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠)
24		saldifcl 46857	. . . . . . . 8 ⊢ ((𝑠 ∈ SAlg ∧ 𝑦 ∈ 𝑠) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠)
25	20, 23, 24	syl2anc 593	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠)
26	19, 25	eqeltrd 2861	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠)
27	26	ralrimiva 3153	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠)
28		intex 5299	. . . . . . . . . . 11 ⊢ (𝐺 ≠ ∅ ↔ ∩ 𝐺 ∈ V)
29	28	biimpi 218	. . . . . . . . . 10 ⊢ (𝐺 ≠ ∅ → ∩ 𝐺 ∈ V)
30	13, 29	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∩ 𝐺 ∈ V)
31	30	uniexd 7721	. . . . . . . 8 ⊢ (𝜑 → ∪ ∩ 𝐺 ∈ V)
32	31	difexd 5286	. . . . . . 7 ⊢ (𝜑 → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V)
33	32	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V)
34		elintg 4912	. . . . . 6 ⊢ ((∪ ∩ 𝐺 ∖ 𝑦) ∈ V → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠))
35	33, 34	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠))
36	27, 35	mpbird 259	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺)
37	36	ralrimiva 3153	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺)
38	3	ad4ant14 762	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
39		elpwi 4561	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 ∩ 𝐺 → 𝑦 ⊆ ∩ 𝐺)
40	39	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ ∩ 𝐺)
41		intss1 4920	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ 𝐺 → ∩ 𝐺 ⊆ 𝑠)
42	41	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → ∩ 𝐺 ⊆ 𝑠)
43	40, 42	sstrd 3946	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ 𝑠)
44		vex 3457	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
45	44	elpw 4558	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 𝑠 ↔ 𝑦 ⊆ 𝑠)
46	43, 45	sylibr 236	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
47	46	adantll 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
48	47	adantlr 725	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
49		simplr 778	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑦 ≼ ω)
50	38, 48, 49	salunicl 46854	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → ∪ 𝑦 ∈ 𝑠)
51	50	ralrimiva 3153	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠)
52		vuniex 7718	. . . . . . . 8 ⊢ ∪ 𝑦 ∈ V
53	52	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ V)
54		elintg 4912	. . . . . . 7 ⊢ (∪ 𝑦 ∈ V → (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠))
55	53, 54	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠))
56	51, 55	mpbird 259	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ ∩ 𝐺)
57	56	ex 416	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) → (𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))
58	57	ralrimiva 3153	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))
59	11, 37, 58	3jca 1140	. 2 ⊢ (𝜑 → (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺)))
60		issal 46852	. . 3 ⊢ (∩ 𝐺 ∈ V → (∩ 𝐺 ∈ SAlg ↔ (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))))
61	30, 60	syl 17	. 2 ⊢ (𝜑 → (∩ 𝐺 ∈ SAlg ↔ (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))))
62	59, 61	mpbird 259	1 ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141   ≠ wne 2956  ∀wral 3075  Vcvv 3453   ∖ cdif 3901   ⊆ wss 3904  ∅c0 4285  𝒫 cpw 4554  ∪ cuni 4864  ∩ cint 4904   class class class wbr 5099  ωcom 7842   ≼ cdom 8921  SAlgcsalg 46846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4905  df-br 5100  df-salg 46847

This theorem is referenced by:  salgencl  46870