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 34134

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 5302	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
2	1	biimpi 216	. . 3 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
3	2	adantr 480	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ V)
4		intssuni 4937	. . . 4 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
5	4	adantr 480	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ ∪ 𝐴)
6		simpr 484	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
7		elpwi 4573	. . . . . 6 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ (sigAlgebra‘𝑂))
8		sigasspw 34113	. . . . . . . 8 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ⊆ 𝒫 𝑂)
9		velpw 4571	. . . . . . . 8 ⊢ (𝑠 ∈ 𝒫 𝒫 𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂)
10	8, 9	sylibr 234	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ∈ 𝒫 𝒫 𝑂)
11	10	ssriv 3953	. . . . . 6 ⊢ (sigAlgebra‘𝑂) ⊆ 𝒫 𝒫 𝑂
12	7, 11	sstrdi 3962	. . . . 5 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
13	6, 12	syl 17	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
14		sspwuni 5067	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝒫 𝑂 ↔ ∪ 𝐴 ⊆ 𝒫 𝑂)
15	13, 14	sylib 218	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∪ 𝐴 ⊆ 𝒫 𝑂)
16	5, 15	sstrd 3960	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ 𝒫 𝑂)
17		simpr 484	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
18		simplr 768	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
19		elelpwi 4576	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑠 ∈ (sigAlgebra‘𝑂))
20	17, 18, 19	syl2anc 584	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ (sigAlgebra‘𝑂))
21		vex 3454	. . . . . . . . 9 ⊢ 𝑠 ∈ V
22		issiga 34109	. . . . . . . . 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 1142	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑂 ∈ 𝑠)
27	26	ralrimiva 3126	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠)
28		n0 4319	. . . . . . . . 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 6899	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
35	34	exlimiv 1930	. . . . . 6 ⊢ (∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
36	33, 35	syl 17	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ V)
37		elintg 4921	. . . . 5 ⊢ (𝑂 ∈ V → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
38	36, 37	syl 17	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
39	27, 38	mpbird 257	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ ∩ 𝐴)
40		simpll 766	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
41		simpr 484	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
42	40, 41	jca 511	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
43		elinti 4922	. . . . . . . . 9 ⊢ (𝑥 ∈ ∩ 𝐴 → (𝑠 ∈ 𝐴 → 𝑥 ∈ 𝑠))
44	43	imp 406	. . . . . . . 8 ⊢ ((𝑥 ∈ ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
45	44	adantll 714	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
46	25	simp2d 1143	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠)
47	46	r19.21bi 3230	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝑠) → (𝑂 ∖ 𝑥) ∈ 𝑠)
48	42, 45, 47	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝑂 ∖ 𝑥) ∈ 𝑠)
49	48	ralrimiva 3126	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠)
50	36	difexd 5289	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∖ 𝑥) ∈ V)
51	50	adantr 480	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ V)
52		elintg 4921	. . . . . 6 ⊢ ((𝑂 ∖ 𝑥) ∈ V → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
53	51, 52	syl 17	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
54	49, 53	mpbird 257	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
55	54	ralrimiva 3126	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
56		simplll 774	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
57		simpr 484	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
58	56, 57	jca 511	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
59		simpllr 775	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 ∩ 𝐴)
60		elpwi 4573	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → 𝑥 ⊆ ∩ 𝐴)
61		intss1 4930	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑠)
62	60, 61	sylan9ss 3963	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ⊆ 𝑠)
63		velpw 4571	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠)
64	62, 63	sylibr 234	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
65	59, 64	sylancom 588	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
66	58, 65	jca 511	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠))
67		simplr 768	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ≼ ω)
68	25	simp3d 1144	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
69	68	r19.21bi 3230	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
70	66, 67, 69	sylc 65	. . . . . . 7 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ∪ 𝑥 ∈ 𝑠)
71	70	ralrimiva 3126	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠)
72		uniexg 7719	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → ∪ 𝑥 ∈ V)
73	72	ad2antlr 727	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ V)
74		elintg 4921	. . . . . . 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 3126	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴))
79	39, 55, 78	3jca 1128	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))
80		issiga 34109	. . 3 ⊢ (∩ 𝐴 ∈ V → (∩ 𝐴 ∈ (sigAlgebra‘𝑂) ↔ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))))
81	80	biimpar 477	. 2 ⊢ ((∩ 𝐴 ∈ V ∧ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))
82	3, 16, 79, 81	syl12anc 836	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∃wex 1779 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 Vcvv 3450 ∖ cdif 3914 ⊆ wss 3917 ∅c0 4299 𝒫 cpw 4566 ∪ cuni 4874 ∩ cint 4913 class class class wbr 5110 ‘cfv 6514 ωcom 7845 ≼ cdom 8919 sigAlgebracsiga 34105

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-br 5111 df-opab 5173 df-mpt 5192 df-id 5536 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-iota 6467 df-fun 6516 df-fv 6522 df-siga 34106

This theorem is referenced by: sigagensiga 34138

W3C validator