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 34138

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 5344	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
2	1	biimpi 216	. . 3 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
3	2	adantr 480	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ V)
4		intssuni 4970	. . . 4 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
5	4	adantr 480	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ ∪ 𝐴)
6		simpr 484	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
7		elpwi 4607	. . . . . 6 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ (sigAlgebra‘𝑂))
8		sigasspw 34117	. . . . . . . 8 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ⊆ 𝒫 𝑂)
9		velpw 4605	. . . . . . . 8 ⊢ (𝑠 ∈ 𝒫 𝒫 𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂)
10	8, 9	sylibr 234	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ∈ 𝒫 𝒫 𝑂)
11	10	ssriv 3987	. . . . . 6 ⊢ (sigAlgebra‘𝑂) ⊆ 𝒫 𝒫 𝑂
12	7, 11	sstrdi 3996	. . . . 5 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
13	6, 12	syl 17	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
14		sspwuni 5100	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝒫 𝑂 ↔ ∪ 𝐴 ⊆ 𝒫 𝑂)
15	13, 14	sylib 218	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∪ 𝐴 ⊆ 𝒫 𝑂)
16	5, 15	sstrd 3994	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ 𝒫 𝑂)
17		simpr 484	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
18		simplr 769	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
19		elelpwi 4610	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑠 ∈ (sigAlgebra‘𝑂))
20	17, 18, 19	syl2anc 584	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ (sigAlgebra‘𝑂))
21		vex 3484	. . . . . . . . 9 ⊢ 𝑠 ∈ V
22		issiga 34113	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))))
23	21, 22	ax-mp 5	. . . . . . . 8 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))))
24	20, 23	sylib 218	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))))
25	24	simprd 495	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))
26	25	simp1d 1143	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑂 ∈ 𝑠)
27	26	ralrimiva 3146	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠)
28		n0 4353	. . . . . . . . 9 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑠 𝑠 ∈ 𝐴)
29	28	biimpi 216	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → ∃𝑠 𝑠 ∈ 𝐴)
30	29	adantr 480	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∃𝑠 𝑠 ∈ 𝐴)
31	20	ex 412	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑠 ∈ 𝐴 → 𝑠 ∈ (sigAlgebra‘𝑂)))
32	31	eximdv 1917	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (∃𝑠 𝑠 ∈ 𝐴 → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂)))
33	30, 32	mpd 15	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂))
34		elfvex 6944	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
35	34	exlimiv 1930	. . . . . 6 ⊢ (∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
36	33, 35	syl 17	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ V)
37		elintg 4954	. . . . 5 ⊢ (𝑂 ∈ V → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
38	36, 37	syl 17	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
39	27, 38	mpbird 257	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ ∩ 𝐴)
40		simpll 767	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
41		simpr 484	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
42	40, 41	jca 511	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
43		elinti 4955	. . . . . . . . 9 ⊢ (𝑥 ∈ ∩ 𝐴 → (𝑠 ∈ 𝐴 → 𝑥 ∈ 𝑠))
44	43	imp 406	. . . . . . . 8 ⊢ ((𝑥 ∈ ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
45	44	adantll 714	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
46	25	simp2d 1144	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠)
47	46	r19.21bi 3251	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝑠) → (𝑂 ∖ 𝑥) ∈ 𝑠)
48	42, 45, 47	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝑂 ∖ 𝑥) ∈ 𝑠)
49	48	ralrimiva 3146	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠)
50	36	difexd 5331	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∖ 𝑥) ∈ V)
51	50	adantr 480	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ V)
52		elintg 4954	. . . . . 6 ⊢ ((𝑂 ∖ 𝑥) ∈ V → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
53	51, 52	syl 17	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
54	49, 53	mpbird 257	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
55	54	ralrimiva 3146	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
56		simplll 775	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
57		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
58	56, 57	jca 511	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
59		simpllr 776	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 ∩ 𝐴)
60		elpwi 4607	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → 𝑥 ⊆ ∩ 𝐴)
61		intss1 4963	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑠)
62	60, 61	sylan9ss 3997	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ⊆ 𝑠)
63		velpw 4605	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠)
64	62, 63	sylibr 234	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
65	59, 64	sylancom 588	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
66	58, 65	jca 511	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠))
67		simplr 769	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ≼ ω)
68	25	simp3d 1145	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
69	68	r19.21bi 3251	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
70	66, 67, 69	sylc 65	. . . . . . 7 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ∪ 𝑥 ∈ 𝑠)
71	70	ralrimiva 3146	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠)
72		uniexg 7760	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → ∪ 𝑥 ∈ V)
73	72	ad2antlr 727	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ V)
74		elintg 4954	. . . . . . 7 ⊢ (∪ 𝑥 ∈ V → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠))
75	73, 74	syl 17	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠))
76	71, 75	mpbird 257	. . . . 5 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ ∩ 𝐴)
77	76	ex 412	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) → (𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴))
78	77	ralrimiva 3146	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴))
79	39, 55, 78	3jca 1129	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))
80		issiga 34113	. . 3 ⊢ (∩ 𝐴 ∈ V → (∩ 𝐴 ∈ (sigAlgebra‘𝑂) ↔ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))))
81	80	biimpar 477	. 2 ⊢ ((∩ 𝐴 ∈ V ∧ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))
82	3, 16, 79, 81	syl12anc 837	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 ∃wex 1779 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 Vcvv 3480 ∖ cdif 3948 ⊆ wss 3951 ∅c0 4333 𝒫 cpw 4600 ∪ cuni 4907 ∩ cint 4946 class class class wbr 5143 ‘cfv 6561 ωcom 7887 ≼ cdom 8983 sigAlgebracsiga 34109

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-iota 6514 df-fun 6563 df-fv 6569 df-siga 34110

This theorem is referenced by: sigagensiga 34142

W3C validator