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 30969

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 5124	. . . 4 ⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V)
2	1	biimpi 217	. . 3 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ∈ V)
3	2	adantr 481	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ V)
4		intssuni 4798	. . . 4 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
5	4	adantr 481	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ ∪ 𝐴)
6		simpr 485	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
7		elpwi 4457	. . . . . 6 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ (sigAlgebra‘𝑂))
8		sigasspw 30948	. . . . . . . 8 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ⊆ 𝒫 𝑂)
9		selpw 4454	. . . . . . . 8 ⊢ (𝑠 ∈ 𝒫 𝒫 𝑂 ↔ 𝑠 ⊆ 𝒫 𝑂)
10	8, 9	sylibr 235	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑠 ∈ 𝒫 𝒫 𝑂)
11	10	ssriv 3888	. . . . . 6 ⊢ (sigAlgebra‘𝑂) ⊆ 𝒫 𝒫 𝑂
12	7, 11	syl6ss 3896	. . . . 5 ⊢ (𝐴 ∈ 𝒫 (sigAlgebra‘𝑂) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
13	6, 12	syl 17	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝐴 ⊆ 𝒫 𝒫 𝑂)
14		sspwuni 4915	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝒫 𝑂 ↔ ∪ 𝐴 ⊆ 𝒫 𝑂)
15	13, 14	sylib 219	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∪ 𝐴 ⊆ 𝒫 𝑂)
16	5, 15	sstrd 3894	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ⊆ 𝒫 𝑂)
17		simpr 485	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
18		simplr 765	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂))
19		elelpwi 4460	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑠 ∈ (sigAlgebra‘𝑂))
20	17, 18, 19	syl2anc 584	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ (sigAlgebra‘𝑂))
21		vex 3435	. . . . . . . . 9 ⊢ 𝑠 ∈ V
22		issiga 30944	. . . . . . . . 9 ⊢ (𝑠 ∈ V → (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))))
23	21, 22	ax-mp 5	. . . . . . . 8 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) ↔ (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))))
24	20, 23	sylib 219	. . . . . . 7 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → (𝑠 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))))
25	24	simprd 496	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → (𝑂 ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠)))
26	25	simp1d 1133	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → 𝑂 ∈ 𝑠)
27	26	ralrimiva 3147	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠)
28		n0 4224	. . . . . . . . 9 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑠 𝑠 ∈ 𝐴)
29	28	biimpi 217	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → ∃𝑠 𝑠 ∈ 𝐴)
30	29	adantr 481	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∃𝑠 𝑠 ∈ 𝐴)
31	20	ex 413	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑠 ∈ 𝐴 → 𝑠 ∈ (sigAlgebra‘𝑂)))
32	31	eximdv 1893	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (∃𝑠 𝑠 ∈ 𝐴 → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂)))
33	30, 32	mpd 15	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂))
34		elfvex 6563	. . . . . . 7 ⊢ (𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
35	34	exlimiv 1906	. . . . . 6 ⊢ (∃𝑠 𝑠 ∈ (sigAlgebra‘𝑂) → 𝑂 ∈ V)
36	33, 35	syl 17	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ V)
37		elintg 4784	. . . . 5 ⊢ (𝑂 ∈ V → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
38	36, 37	syl 17	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 𝑂 ∈ 𝑠))
39	27, 38	mpbird 258	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → 𝑂 ∈ ∩ 𝐴)
40		simpll 763	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
41		simpr 485	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
42	40, 41	jca 512	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
43		elinti 4785	. . . . . . . . 9 ⊢ (𝑥 ∈ ∩ 𝐴 → (𝑠 ∈ 𝐴 → 𝑥 ∈ 𝑠))
44	43	imp 407	. . . . . . . 8 ⊢ ((𝑥 ∈ ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
45	44	adantll 710	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝑠)
46	25	simp2d 1134	. . . . . . . 8 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝑠 (𝑂 ∖ 𝑥) ∈ 𝑠)
47	46	r19.21bi 3173	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝑠) → (𝑂 ∖ 𝑥) ∈ 𝑠)
48	42, 45, 47	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) → (𝑂 ∖ 𝑥) ∈ 𝑠)
49	48	ralrimiva 3147	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠)
50		difexg 5115	. . . . . . . 8 ⊢ (𝑂 ∈ V → (𝑂 ∖ 𝑥) ∈ V)
51	36, 50	syl 17	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∖ 𝑥) ∈ V)
52	51	adantr 481	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ V)
53		elintg 4784	. . . . . 6 ⊢ ((𝑂 ∖ 𝑥) ∈ V → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
54	52, 53	syl 17	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → ((𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 (𝑂 ∖ 𝑥) ∈ 𝑠))
55	49, 54	mpbird 258	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ ∩ 𝐴) → (𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
56	55	ralrimiva 3147	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴)
57		simplll 771	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)))
58		simpr 485	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ 𝐴)
59	57, 58	jca 512	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴))
60		simpllr 772	. . . . . . . . . 10 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 ∩ 𝐴)
61		elpwi 4457	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → 𝑥 ⊆ ∩ 𝐴)
62		intss1 4791	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑠)
63	61, 62	sylan9ss 3897	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ⊆ 𝑠)
64		selpw 4454	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝒫 𝑠 ↔ 𝑥 ⊆ 𝑠)
65	63, 64	sylibr 235	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
66	60, 65	sylancom 588	. . . . . . . . 9 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ∈ 𝒫 𝑠)
67	59, 66	jca 512	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠))
68		simplr 765	. . . . . . . 8 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → 𝑥 ≼ ω)
69	25	simp3d 1135	. . . . . . . . 9 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) → ∀𝑥 ∈ 𝒫 𝑠(𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
70	69	r19.21bi 3173	. . . . . . . 8 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑠 ∈ 𝐴) ∧ 𝑥 ∈ 𝒫 𝑠) → (𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑠))
71	67, 68, 70	sylc 65	. . . . . . 7 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) ∧ 𝑠 ∈ 𝐴) → ∪ 𝑥 ∈ 𝑠)
72	71	ralrimiva 3147	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠)
73		uniexg 7316	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 ∩ 𝐴 → ∪ 𝑥 ∈ V)
74	73	ad2antlr 723	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ V)
75		elintg 4784	. . . . . . 7 ⊢ (∪ 𝑥 ∈ V → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠))
76	74, 75	syl 17	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → (∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀𝑠 ∈ 𝐴 ∪ 𝑥 ∈ 𝑠))
77	72, 76	mpbird 258	. . . . 5 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) ∧ 𝑥 ≼ ω) → ∪ 𝑥 ∈ ∩ 𝐴)
78	77	ex 413	. . . 4 ⊢ (((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) ∧ 𝑥 ∈ 𝒫 ∩ 𝐴) → (𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴))
79	78	ralrimiva 3147	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴))
80	39, 56, 79	3jca 1119	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))
81		issiga 30944	. . 3 ⊢ (∩ 𝐴 ∈ V → (∩ 𝐴 ∈ (sigAlgebra‘𝑂) ↔ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))))
82	81	biimpar 478	. 2 ⊢ ((∩ 𝐴 ∈ V ∧ (∩ 𝐴 ⊆ 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴(𝑂 ∖ 𝑥) ∈ ∩ 𝐴 ∧ ∀𝑥 ∈ 𝒫 ∩ 𝐴(𝑥 ≼ ω → ∪ 𝑥 ∈ ∩ 𝐴)))) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))
83	3, 16, 80, 82	syl12anc 833	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ 𝒫 (sigAlgebra‘𝑂)) → ∩ 𝐴 ∈ (sigAlgebra‘𝑂))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1078 ∃wex 1759 ∈ wcel 2079 ≠ wne 2982 ∀wral 3103 Vcvv 3432 ∖ cdif 3851 ⊆ wss 3854 ∅c0 4206 𝒫 cpw 4447 ∪ cuni 4739 ∩ cint 4776 class class class wbr 4956 ‘cfv 6217 ωcom 7427 ≼ cdom 8345 sigAlgebracsiga 30940

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 ax-sep 5088 ax-nul 5095 ax-pow 5150 ax-pr 5214 ax-un 7310

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-fal 1533 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ne 2983 df-ral 3108 df-rex 3109 df-rab 3112 df-v 3434 df-sbc 3702 df-csb 3807 df-dif 3857 df-un 3859 df-in 3861 df-ss 3869 df-nul 4207 df-if 4376 df-pw 4449 df-sn 4467 df-pr 4469 df-op 4473 df-uni 4740 df-int 4777 df-br 4957 df-opab 5019 df-mpt 5036 df-id 5340 df-xp 5441 df-rel 5442 df-cnv 5443 df-co 5444 df-dm 5445 df-iota 6181 df-fun 6219 df-fv 6225 df-siga 30941

This theorem is referenced by: sigagensiga 30973

W3C validator