Theorem insiga 28954

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	|- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. (sigAlgebra ` O ) )

Proof of Theorem insiga

Dummy variables x s are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		intex 4576	. . . 4 |- ( A =/= (/) <-> |^| A e. _V )
2	1	biimpi 197	. . 3 |- ( A =/= (/) -> |^| A e. _V )
3	2	adantr 466	. 2 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. _V )
4		intssuni 4275	. . . 4 |- ( A =/= (/) -> |^| A C_ U. A )
5	4	adantr 466	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A C_ U. A )
6		simpr 462	. . . . 5 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A e. ~P (sigAlgebra ` O ) )
7		elpwi 3988	. . . . . 6 |- ( A e. ~P (sigAlgebra ` O ) -> A C_ (sigAlgebra ` O ) )
8		sigasspw 28933	. . . . . . . 8 |- ( s e. (sigAlgebra ` O ) -> s C_ ~P O )
9		selpw 3986	. . . . . . . 8 |- ( s e. ~P ~P O <-> s C_ ~P O )
10	8, 9	sylibr 215	. . . . . . 7 |- ( s e. (sigAlgebra ` O ) -> s e. ~P ~P O )
11	10	ssriv 3468	. . . . . 6 |- (sigAlgebra ` O ) C_ ~P ~P O
12	7, 11	syl6ss 3476	. . . . 5 |- ( A e. ~P (sigAlgebra ` O ) -> A C_ ~P ~P O )
13	6, 12	syl 17	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A C_ ~P ~P O )
14		sspwuni 4385	. . . 4 |- ( A C_ ~P ~P O <-> U. A C_ ~P O )
15	13, 14	sylib 199	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> U. A C_ ~P O )
16	5, 15	sstrd 3474	. 2 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A C_ ~P O )
17		simpr 462	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> s e. A )
18		simplr 760	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A e. ~P (sigAlgebra ` O ) )
19		elelpwi 3990	. . . . . . . . 9 |- ( ( s e. A /\ A e. ~P (sigAlgebra ` O ) ) -> s e. (sigAlgebra ` O ) )
20	17, 18, 19	syl2anc 665	. . . . . . . 8 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> s e. (sigAlgebra ` O ) )
21		vex 3084	. . . . . . . . 9 |- s e. _V
22		issiga 28928	. . . . . . . . 9 |- ( s e. _V -> ( s e. (sigAlgebra ` O ) <-> ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ om -> U. x e. s ) ) ) ) )
23	21, 22	ax-mp 5	. . . . . . . 8 |- ( s e. (sigAlgebra ` O ) <-> ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ om -> U. x e. s ) ) ) )
24	20, 23	sylib 199	. . . . . . 7 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> ( s C_ ~P O /\ ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ om -> U. x e. s ) ) ) )
25	24	simprd 464	. . . . . 6 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ om -> U. x e. s ) ) )
26	25	simp1d 1017	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> O e. s )
27	26	ralrimiva 2839	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. s e. A O e. s )
28		n0 3771	. . . . . . . . 9 |- ( A =/= (/) <-> E. s s e. A )
29	28	biimpi 197	. . . . . . . 8 |- ( A =/= (/) -> E. s s e. A )
30	29	adantr 466	. . . . . . 7 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> E. s s e. A )
31	20	ex 435	. . . . . . . 8 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( s e. A -> s e. (sigAlgebra ` O ) ) )
32	31	eximdv 1754	. . . . . . 7 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( E. s s e. A -> E. s s e. (sigAlgebra ` O ) ) )
33	30, 32	mpd 15	. . . . . 6 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> E. s s e. (sigAlgebra ` O ) )
34		elfvex 5904	. . . . . . 7 |- ( s e. (sigAlgebra ` O ) -> O e. _V )
35	34	exlimiv 1766	. . . . . 6 |- ( E. s s e. (sigAlgebra ` O ) -> O e. _V )
36	33, 35	syl 17	. . . . 5 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> O e. _V )
37		elintg 4260	. . . . 5 |- ( O e. _V -> ( O e. |^| A <-> A. s e. A O e. s ) )
38	36, 37	syl 17	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( O e. |^| A <-> A. s e. A O e. s ) )
39	27, 38	mpbird 235	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> O e. |^| A )
40		simpll 758	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) )
41		simpr 462	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> s e. A )
42	40, 41	jca 534	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) )
43		elinti 4261	. . . . . . . . 9 |- ( x e. |^| A -> ( s e. A -> x e. s ) )
44	43	imp 430	. . . . . . . 8 |- ( ( x e. |^| A /\ s e. A ) -> x e. s )
45	44	adantll 718	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> x e. s )
46	25	simp2d 1018	. . . . . . . 8 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A. x e. s ( O \ x ) e. s )
47	46	r19.21bi 2794	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) /\ x e. s ) -> ( O \ x ) e. s )
48	42, 45, 47	syl2anc 665	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( O \ x ) e. s )
49	48	ralrimiva 2839	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> A. s e. A ( O \ x ) e. s )
50		difexg 4568	. . . . . . . 8 |- ( O e. _V -> ( O \ x ) e. _V )
51	36, 50	syl 17	. . . . . . 7 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( O \ x ) e. _V )
52	51	adantr 466	. . . . . 6 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. _V )
53		elintg 4260	. . . . . 6 |- ( ( O \ x ) e. _V -> ( ( O \ x ) e. |^| A <-> A. s e. A ( O \ x ) e. s ) )
54	52, 53	syl 17	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( ( O \ x ) e. |^| A <-> A. s e. A ( O \ x ) e. s ) )
55	49, 54	mpbird 235	. . . 4 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. |^| A )
56	55	ralrimiva 2839	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. x e. |^| A ( O \ x ) e. |^| A )
57		simplll 766	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) )
58		simpr 462	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> s e. A )
59	57, 58	jca 534	. . . . . . . . 9 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) )
60		simpllr 767	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x e. ~P |^| A )
61		elpwi 3988	. . . . . . . . . . . 12 |- ( x e. ~P |^| A -> x C_ |^| A )
62		intss1 4267	. . . . . . . . . . . 12 |- ( s e. A -> |^| A C_ s )
63	61, 62	sylan9ss 3477	. . . . . . . . . . 11 |- ( ( x e. ~P |^| A /\ s e. A ) -> x C_ s )
64		selpw 3986	. . . . . . . . . . 11 |- ( x e. ~P s <-> x C_ s )
65	63, 64	sylibr 215	. . . . . . . . . 10 |- ( ( x e. ~P |^| A /\ s e. A ) -> x e. ~P s )
66	60, 65	sylancom 671	. . . . . . . . 9 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x e. ~P s )
67	59, 66	jca 534	. . . . . . . 8 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) /\ x e. ~P s ) )
68		simplr 760	. . . . . . . 8 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x ~<_ om )
69	25	simp3d 1019	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A. x e. ~P s ( x ~<_ om -> U. x e. s ) )
70	69	r19.21bi 2794	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) /\ x e. ~P s ) -> ( x ~<_ om -> U. x e. s ) )
71	67, 68, 70	sylc 62	. . . . . . 7 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> U. x e. s )
72	71	ralrimiva 2839	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> A. s e. A U. x e. s )
73		uniexg 6598	. . . . . . . 8 |- ( x e. ~P |^| A -> U. x e. _V )
74	73	ad2antlr 731	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> U. x e. _V )
75		elintg 4260	. . . . . . 7 |- ( U. x e. _V -> ( U. x e. |^| A <-> A. s e. A U. x e. s ) )
76	74, 75	syl 17	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> ( U. x e. |^| A <-> A. s e. A U. x e. s ) )
77	72, 76	mpbird 235	. . . . 5 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> U. x e. |^| A )
78	77	ex 435	. . . 4 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) -> ( x ~<_ om -> U. x e. |^| A ) )
79	78	ralrimiva 2839	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. x e. ~P |^| A ( x ~<_ om -> U. x e. |^| A ) )
80	39, 56, 79	3jca 1185	. 2 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( O e. |^| A /\ A. x e. |^| A ( O \ x ) e. |^| A /\ A. x e. ~P |^| A ( x ~<_ om -> U. x e. |^| A ) ) )
81		issiga 28928	. . 3 |- ( |^| A e. _V -> ( |^| A e. (sigAlgebra ` O ) <-> ( |^| A C_ ~P O /\ ( O e. |^| A /\ A. x e. |^| A ( O \ x ) e. |^| A /\ A. x e. ~P |^| A ( x ~<_ om -> U. x e. |^| A ) ) ) ) )
82	81	biimpar 487	. 2 |- ( ( |^| A e. _V /\ ( |^| A C_ ~P O /\ ( O e. |^| A /\ A. x e. |^| A ( O \ x ) e. |^| A /\ A. x e. ~P |^| A ( x ~<_ om -> U. x e. |^| A ) ) ) ) -> |^| A e. (sigAlgebra ` O ) )
83	3, 16, 80, 82	syl12anc 1262	1 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. (sigAlgebra ` O ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   E.wex 1659   e. wcel 1868   =/= wne 2618   A.wral 2775   _Vcvv 3081   \ cdif 3433   C_ wss 3436   (/)c0 3761   ~Pcpw 3979   U.cuni 4216   |^|cint 4252   class class class wbr 4420   ` cfv 5597   omcom 6702   ~<_ cdom 7571  sigAlgebracsiga 28924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-int 4253  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-iota 5561  df-fun 5599  df-fv 5605  df-siga 28925

This theorem is referenced by:  sigagensiga  28958