insiga - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > insiga		Structured version Visualization version GIF version

Theorem insiga 34471

Description: The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)

**Assertion**
Ref	Expression
insiga	⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))

Proof of Theorem insiga Dummy variables 𝑥 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		intex 5315	. . 3 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
2	1	birani 508	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ V)
3		intssuni 4939	. . . 4 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
4	3	adantr 485	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ ∪ 𝐴)
5		simpr 489	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
6		elpwi 4574	. . . . . 6 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ (sigAlgebra‘𝑂))
7		sigasspw 34450	. . . . . . . 8 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ⊆ 𝒫 𝑂)
8		velpw 4572	. . . . . . . 8 ⊢ (𝑠 ∈ 𝒫 𝒫 𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂)
9	7, 8	sylibr 237	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ∈ 𝒫 𝒫 𝑂)
10	9	ssriv 3949	. . . . . 6 ⊢ (sigAlgebra‘𝑂) ⊆ 𝒫 𝒫 𝑂
11	6, 10	sstrdi 3957	. . . . 5 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
12	5, 11	syl 18	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
13		sspwuni 5070	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝒫 𝑂 ↔ ∪ 𝐴 ⊆ 𝒫 𝑂)
14	12, 13	sylib 221	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∪ 𝐴 ⊆ 𝒫 𝑂)
15	4, 14	sstrd 3955	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ 𝒫 𝑂)
16		simpr 489	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
17		simplr 780	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
18		elelpwi 4577	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑠 ∈ (sigAlgebra‘𝑂))
19	16, 17, 18	syl2anc 595	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ (sigAlgebra‘𝑂))
20		vex 3467	. . . . . . . . 9 ⊢ 𝑠 ∈ V
21		issiga 34446	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))))
22	20, 21	ax-mp 5	. . . . . . . 8 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))))
23	19, 22	sylib 221	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))))
24	23	simprd 500	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))
25	24	simp1d 1158	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑂 ∈ 𝑠)
26	25	ralrimiva 3163	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠)
27		n0 4315	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑠 𝑠 ∈ 𝐴)
28	27	birani 508	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∃𝑠 𝑠 ∈ 𝐴)
29	19	ex 417	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑠 ∈ 𝐴 → 𝑠 ∈ (sigAlgebra‘𝑂)))
30	29	eximdv 1944	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (∃𝑠 𝑠 ∈ 𝐴 → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂)))
31	28, 30	mpd 16	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂))
32		elfvex 6917	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
33	32	exlimiv 1957	. . . . . 6 ⊢ (∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
34	31, 33	syl 18	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ V)
35		elintg 4924	. . . . 5 ⊢ (𝑂 ∈ V → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
36	34, 35	syl 18	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
37	26, 36	mpbird 260	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ ∩ 𝐴)
38		simpll 778	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
39		simpr 489	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
40	38, 39	jca 520	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
41		elinti 4925	. . . . . . . . 9 ⊢ (𝑥 ∈ ∩ 𝐴 → (𝑠 ∈ 𝐴 → 𝑥 ∈ 𝑠))
42	41	imp 411	. . . . . . . 8 ⊢ ((𝑥 ∈ ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
43	42	adantll 726	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
44	24	simp2d 1159	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠)
45	44	r19.21bi 3263	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝑠) → (𝑂 ∖ 𝑥) ∈ 𝑠)
46	40, 43, 45	syl2anc 595	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝑂 ∖ 𝑥) ∈ 𝑠)
47	46	ralrimiva 3163	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠)
48	34	difexd 5302	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∖ 𝑥) ∈ V)
49	48	adantr 485	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ V)
50		elintg 4924	. . . . . 6 ⊢ ((𝑂 ∖ 𝑥) ∈ V → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
51	49, 50	syl 18	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
52	47, 51	mpbird 260	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
53	52	ralrimiva 3163	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
54		simplll 786	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
55		simpr 489	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
56	54, 55	jca 520	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
57		simpllr 787	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 ∩ 𝐴)
58		elpwi 4574	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → 𝑥 ⊆ ∩ 𝐴)
59		intss1 4932	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑠)
60	58, 59	sylan9ss 3958	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ⊆ 𝑠)
61		velpw 4572	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠)
62	60, 61	sylibr 237	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
63	57, 62	sylancom 599	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
64	56, 63	jca 520	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠))
65		simplr 780	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ≼ ω)
66	24	simp3d 1160	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
67	66	r19.21bi 3263	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
68	64, 65, 67	sylc 66	. . . . . . 7 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ∪ 𝑥 ∈ 𝑠)
69	68	ralrimiva 3163	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠)
70		uniexg 7738	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → ∪ 𝑥 ∈ V)
71	70	ad2antlr 739	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ V)
72		elintg 4924	. . . . . . 7 ⊢ (∪ 𝑥 ∈ V → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠))
73	71, 72	syl 18	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠))
74	69, 73	mpbird 260	. . . . 5 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ ∩ 𝐴)
75	74	ex 417	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) → (𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴))
76	75	ralrimiva 3163	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴))
77	37, 53, 76	3jca 1144	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))
78		issiga 34446	. . 3 ⊢ (∩ 𝐴 ∈ V → (∩ 𝐴 ∈ (sigAlgebra‘𝑂) ↔ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))))
79	78	biimpar 482	. 2 ⊢ ((∩ 𝐴 ∈ V ∧ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))
80	2, 15, 77, 79	syl12anc 849	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 ∃wex 1806 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 Vcvv 3463 ∖ cdif 3910 ⊆ wss 3913 ∅c0 4294 𝒫 cpw 4567 ∪ cuni 4876 ∩ cint 4916 class class class wbr 5113 ‘cfv 6537 ωcom 7861 ≼ cdom 8940 sigAlgebracsiga 34442

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-iota 6493 df-fun 6539 df-fv 6545 df-siga 34443

This theorem is referenced by: sigagensiga 34475

W3C validator