Theorem intsal 47284

Description: The arbitrary intersection of sigma-algebra (on the same set 𝑋) is a sigma-algebra ( on the same set 𝑋, see intsaluni 47283). (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 488	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝜑)
2		intsal.ga	. . . . . . 7 ⊢ (𝜑 → 𝐺 ⊆ SAlg)
3	2	sselda 3931	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
4		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → 𝑠 ∈ SAlg)
5		0sal 47274	. . . . . . 7 ⊢ (𝑠 ∈ SAlg → ∅ ∈ 𝑠)
6	4, 5	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → ∅ ∈ 𝑠)
7	1, 3, 6	syl2anc 596	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∅ ∈ 𝑠)
8	7	ralrimiva 3155	. . . 4 ⊢ (𝜑 → ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠)
9		0ex 5261	. . . . 5 ⊢ ∅ ∈ V
10	9	elint2 4914	. . . 4 ⊢ (∅ ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠)
11	8, 10	sylibr 237	. . 3 ⊢ (𝜑 → ∅ ∈ ∩ 𝐺)
12		intsal.x	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋)
13		intsal.gn0	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 ≠ ∅)
14	2, 13, 12	intsaluni 47283	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋)
15	14	eqcomd 2767	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 = ∪ ∩ 𝐺)
16	15	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑋 = ∪ ∩ 𝐺)
17	12, 16	eqtr2d 2797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ ∩ 𝐺 = ∪ 𝑠)
18	17	difeq1d 4073	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) = (∪ 𝑠 ∖ 𝑦))
19	18	adantlr 728	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) = (∪ 𝑠 ∖ 𝑦))
20	3	adantlr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
21		elinti 4916	. . . . . . . . . 10 ⊢ (𝑦 ∈ ∩ 𝐺 → (𝑠 ∈ 𝐺 → 𝑦 ∈ 𝑠))
22	21	imp 412	. . . . . . . . 9 ⊢ ((𝑦 ∈ ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠)
23	22	adantll 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠)
24		saldifcl 47273	. . . . . . . 8 ⊢ ((𝑠 ∈ SAlg ∧ 𝑦 ∈ 𝑠) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠)
25	20, 23, 24	syl2anc 596	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠)
26	19, 25	eqeltrd 2861	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠)
27	26	ralrimiva 3155	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠)
28		intex 5305	. . . . . . . . . . 11 ⊢ (𝐺 ≠ ∅ ↔ ∩ 𝐺 ∈ V)
29	28	biimpi 219	. . . . . . . . . 10 ⊢ (𝐺 ≠ ∅ → ∩ 𝐺 ∈ V)
30	13, 29	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ∩ 𝐺 ∈ V)
31	30	uniexd 7748	. . . . . . . 8 ⊢ (𝜑 → ∪ ∩ 𝐺 ∈ V)
32	31	difexd 5293	. . . . . . 7 ⊢ (𝜑 → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V)
33	32	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V)
34		elintg 4915	. . . . . 6 ⊢ ((∪ ∩ 𝐺 ∖ 𝑦) ∈ V → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠))
35	33, 34	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺 ∖ 𝑦) ∈ 𝑠))
36	27, 35	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺)
37	36	ralrimiva 3155	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺)
38	3	ad4ant14 765	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg)
39		elpwi 4564	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝒫 ∩ 𝐺 → 𝑦 ⊆ ∩ 𝐺)
40	39	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ ∩ 𝐺)
41		intss1 4923	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ 𝐺 → ∩ 𝐺 ⊆ 𝑠)
42	41	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → ∩ 𝐺 ⊆ 𝑠)
43	40, 42	sstrd 3941	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ 𝑠)
44		vex 3455	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
45	44	elpw 4561	. . . . . . . . . . 11 ⊢ (𝑦 ∈ 𝒫 𝑠 ↔ 𝑦 ⊆ 𝑠)
46	43, 45	sylibr 237	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺 ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
47	46	adantll 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
48	47	adantlr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠)
49		simplr 781	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → 𝑦 ≼ ω)
50	38, 48, 49	salunicl 47270	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) ∧ 𝑠 ∈ 𝐺) → ∪ 𝑦 ∈ 𝑠)
51	50	ralrimiva 3155	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠)
52		vuniex 7745	. . . . . . . 8 ⊢ ∪ 𝑦 ∈ V
53	52	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ V)
54		elintg 4915	. . . . . . 7 ⊢ (∪ 𝑦 ∈ V → (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠))
55	53, 54	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠))
56	51, 55	mpbird 260	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) ∧ 𝑦 ≼ ω) → ∪ 𝑦 ∈ ∩ 𝐺)
57	56	ex 418	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺) → (𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))
58	57	ralrimiva 3155	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))
59	11, 37, 58	3jca 1146	. 2 ⊢ (𝜑 → (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺)))
60		issal 47268	. . 3 ⊢ (∩ 𝐺 ∈ V → (∩ 𝐺 ∈ SAlg ↔ (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))))
61	30, 60	syl 18	. 2 ⊢ (𝜑 → (∩ 𝐺 ∈ SAlg ↔ (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦 ∈ ∩ 𝐺))))
62	59, 61	mpbird 260	1 ⊢ (𝜑 → ∩ 𝐺 ∈ SAlg)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  Vcvv 3451   ∖ cdif 3896   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  ∪ cuni 4867  ∩ cint 4907   class class class wbr 5103  ωcom 7866   ≼ cdom 8955  SAlgcsalg 47262

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-br 5104  df-salg 47263

This theorem is used by:  salgencl  47286