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 32005

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 5256	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
2	1	biimpi 215	. . 3 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
3	2	adantr 480	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ V)
4		intssuni 4898	. . . 4 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
5	4	adantr 480	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ ∪ 𝐴)
6		simpr 484	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
7		elpwi 4539	. . . . . 6 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ (sigAlgebra‘𝑂))
8		sigasspw 31984	. . . . . . . 8 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ⊆ 𝒫 𝑂)
9		velpw 4535	. . . . . . . 8 ⊢ (𝑠 ∈ 𝒫 𝒫 𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂)
10	8, 9	sylibr 233	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ∈ 𝒫 𝒫 𝑂)
11	10	ssriv 3921	. . . . . 6 ⊢ (sigAlgebra‘𝑂) ⊆ 𝒫 𝒫 𝑂
12	7, 11	sstrdi 3929	. . . . 5 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
13	6, 12	syl 17	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
14		sspwuni 5025	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝒫 𝑂 ↔ ∪ 𝐴 ⊆ 𝒫 𝑂)
15	13, 14	sylib 217	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∪ 𝐴 ⊆ 𝒫 𝑂)
16	5, 15	sstrd 3927	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ 𝒫 𝑂)
17		simpr 484	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
18		simplr 765	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
19		elelpwi 4542	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑠 ∈ (sigAlgebra‘𝑂))
20	17, 18, 19	syl2anc 583	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ (sigAlgebra‘𝑂))
21		vex 3426	. . . . . . . . 9 ⊢ 𝑠 ∈ V
22		issiga 31980	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))))
23	21, 22	ax-mp 5	. . . . . . . 8 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))))
24	20, 23	sylib 217	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))))
25	24	simprd 495	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))
26	25	simp1d 1140	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑂 ∈ 𝑠)
27	26	ralrimiva 3107	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠)
28		n0 4277	. . . . . . . . 9 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑠 𝑠 ∈ 𝐴)
29	28	biimpi 215	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → ∃𝑠 𝑠 ∈ 𝐴)
30	29	adantr 480	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∃𝑠 𝑠 ∈ 𝐴)
31	20	ex 412	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑠 ∈ 𝐴 → 𝑠 ∈ (sigAlgebra‘𝑂)))
32	31	eximdv 1921	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (∃𝑠 𝑠 ∈ 𝐴 → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂)))
33	30, 32	mpd 15	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂))
34		elfvex 6789	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
35	34	exlimiv 1934	. . . . . 6 ⊢ (∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
36	33, 35	syl 17	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ V)
37		elintg 4884	. . . . 5 ⊢ (𝑂 ∈ V → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
38	36, 37	syl 17	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
39	27, 38	mpbird 256	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ ∩ 𝐴)
40		simpll 763	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
41		simpr 484	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
42	40, 41	jca 511	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
43		elinti 4885	. . . . . . . . 9 ⊢ (𝑥 ∈ ∩ 𝐴 → (𝑠 ∈ 𝐴 → 𝑥 ∈ 𝑠))
44	43	imp 406	. . . . . . . 8 ⊢ ((𝑥 ∈ ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
45	44	adantll 710	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
46	25	simp2d 1141	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠)
47	46	r19.21bi 3132	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝑠) → (𝑂 ∖ 𝑥) ∈ 𝑠)
48	42, 45, 47	syl2anc 583	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝑂 ∖ 𝑥) ∈ 𝑠)
49	48	ralrimiva 3107	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠)
50	36	difexd 5248	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∖ 𝑥) ∈ V)
51	50	adantr 480	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ V)
52		elintg 4884	. . . . . 6 ⊢ ((𝑂 ∖ 𝑥) ∈ V → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
53	51, 52	syl 17	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
54	49, 53	mpbird 256	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
55	54	ralrimiva 3107	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
56		simplll 771	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
57		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
58	56, 57	jca 511	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
59		simpllr 772	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 ∩ 𝐴)
60		elpwi 4539	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → 𝑥 ⊆ ∩ 𝐴)
61		intss1 4891	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑠)
62	60, 61	sylan9ss 3930	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ⊆ 𝑠)
63		velpw 4535	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠)
64	62, 63	sylibr 233	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
65	59, 64	sylancom 587	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
66	58, 65	jca 511	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠))
67		simplr 765	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ≼ ω)
68	25	simp3d 1142	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
69	68	r19.21bi 3132	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
70	66, 67, 69	sylc 65	. . . . . . 7 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ∪ 𝑥 ∈ 𝑠)
71	70	ralrimiva 3107	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠)
72		uniexg 7571	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → ∪ 𝑥 ∈ V)
73	72	ad2antlr 723	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ V)
74		elintg 4884	. . . . . . 7 ⊢ (∪ 𝑥 ∈ V → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠))
75	73, 74	syl 17	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠))
76	71, 75	mpbird 256	. . . . 5 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ ∩ 𝐴)
77	76	ex 412	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) → (𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴))
78	77	ralrimiva 3107	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴))
79	39, 55, 78	3jca 1126	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))
80		issiga 31980	. . 3 ⊢ (∩ 𝐴 ∈ V → (∩ 𝐴 ∈ (sigAlgebra‘𝑂) ↔ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))))
81	80	biimpar 477	. 2 ⊢ ((∩ 𝐴 ∈ V ∧ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))
82	3, 16, 79, 81	syl12anc 833	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 ∃wex 1783 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 Vcvv 3422 ∖ cdif 3880 ⊆ wss 3883 ∅c0 4253 𝒫 cpw 4530 ∪ cuni 4836 ∩ cint 4876 class class class wbr 5070 ‘cfv 6418 ωcom 7687 ≼ cdom 8689 sigAlgebracsiga 31976

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-int 4877 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-iota 6376 df-fun 6420 df-fv 6426 df-siga 31977

This theorem is referenced by: sigagensiga 32009

W3C validator