Theorem insiga 28310

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 4612	. . . 4 |- ( A =/= (/) <-> |^| A e. _V )
2	1	biimpi 194	. . 3 |- ( A =/= (/) -> |^| A e. _V )
3	2	adantr 465	. 2 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. _V )
4		intssuni 4311	. . . 4 |- ( A =/= (/) -> |^| A C_ U. A )
5	4	adantr 465	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A C_ U. A )
6		simpr 461	. . . . 5 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A e. ~P (sigAlgebra ` O ) )
7		elpwi 4024	. . . . . 6 |- ( A e. ~P (sigAlgebra ` O ) -> A C_ (sigAlgebra ` O ) )
8		sigasspw 28289	. . . . . . . 8 |- ( s e. (sigAlgebra ` O ) -> s C_ ~P O )
9		selpw 4022	. . . . . . . 8 |- ( s e. ~P ~P O <-> s C_ ~P O )
10	8, 9	sylibr 212	. . . . . . 7 |- ( s e. (sigAlgebra ` O ) -> s e. ~P ~P O )
11	10	ssriv 3503	. . . . . 6 |- (sigAlgebra ` O ) C_ ~P ~P O
12	7, 11	syl6ss 3511	. . . . 5 |- ( A e. ~P (sigAlgebra ` O ) -> A C_ ~P ~P O )
13	6, 12	syl 16	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A C_ ~P ~P O )
14		sspwuni 4421	. . . 4 |- ( A C_ ~P ~P O <-> U. A C_ ~P O )
15	13, 14	sylib 196	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> U. A C_ ~P O )
16	5, 15	sstrd 3509	. 2 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A C_ ~P O )
17		simpr 461	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> s e. A )
18		simplr 755	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A e. ~P (sigAlgebra ` O ) )
19		elelpwi 4026	. . . . . . . . 9 |- ( ( s e. A /\ A e. ~P (sigAlgebra ` O ) ) -> s e. (sigAlgebra ` O ) )
20	17, 18, 19	syl2anc 661	. . . . . . . 8 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> s e. (sigAlgebra ` O ) )
21		vex 3112	. . . . . . . . 9 |- s e. _V
22		issiga 28284	. . . . . . . . 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 196	. . . . . . 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 463	. . . . . 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 1008	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> O e. s )
27	26	ralrimiva 2871	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. s e. A O e. s )
28		n0 3803	. . . . . . . . 9 |- ( A =/= (/) <-> E. s s e. A )
29	28	biimpi 194	. . . . . . . 8 |- ( A =/= (/) -> E. s s e. A )
30	29	adantr 465	. . . . . . 7 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> E. s s e. A )
31	20	ex 434	. . . . . . . 8 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( s e. A -> s e. (sigAlgebra ` O ) ) )
32	31	eximdv 1711	. . . . . . 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 5899	. . . . . . 7 |- ( s e. (sigAlgebra ` O ) -> O e. _V )
35	34	exlimiv 1723	. . . . . 6 |- ( E. s s e. (sigAlgebra ` O ) -> O e. _V )
36	33, 35	syl 16	. . . . 5 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> O e. _V )
37		elintg 4296	. . . . 5 |- ( O e. _V -> ( O e. |^| A <-> A. s e. A O e. s ) )
38	36, 37	syl 16	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( O e. |^| A <-> A. s e. A O e. s ) )
39	27, 38	mpbird 232	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> O e. |^| A )
40		simpll 753	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) )
41		simpr 461	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> s e. A )
42	40, 41	jca 532	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) )
43		elinti 4297	. . . . . . . . 9 |- ( x e. |^| A -> ( s e. A -> x e. s ) )
44	43	imp 429	. . . . . . . 8 |- ( ( x e. |^| A /\ s e. A ) -> x e. s )
45	44	adantll 713	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> x e. s )
46	25	simp2d 1009	. . . . . . . 8 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A. x e. s ( O \ x ) e. s )
47	46	r19.21bi 2826	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) /\ x e. s ) -> ( O \ x ) e. s )
48	42, 45, 47	syl2anc 661	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( O \ x ) e. s )
49	48	ralrimiva 2871	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> A. s e. A ( O \ x ) e. s )
50		difexg 4604	. . . . . . . 8 |- ( O e. _V -> ( O \ x ) e. _V )
51	36, 50	syl 16	. . . . . . 7 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( O \ x ) e. _V )
52	51	adantr 465	. . . . . 6 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. _V )
53		elintg 4296	. . . . . 6 |- ( ( O \ x ) e. _V -> ( ( O \ x ) e. |^| A <-> A. s e. A ( O \ x ) e. s ) )
54	52, 53	syl 16	. . . . 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 232	. . . 4 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. |^| A )
56	55	ralrimiva 2871	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. x e. |^| A ( O \ x ) e. |^| A )
57		simplll 759	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) )
58		simpr 461	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> s e. A )
59	57, 58	jca 532	. . . . . . . . 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 760	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x e. ~P |^| A )
61		elpwi 4024	. . . . . . . . . . . 12 |- ( x e. ~P |^| A -> x C_ |^| A )
62		intss1 4303	. . . . . . . . . . . 12 |- ( s e. A -> |^| A C_ s )
63	61, 62	sylan9ss 3512	. . . . . . . . . . 11 |- ( ( x e. ~P |^| A /\ s e. A ) -> x C_ s )
64		selpw 4022	. . . . . . . . . . 11 |- ( x e. ~P s <-> x C_ s )
65	63, 64	sylibr 212	. . . . . . . . . 10 |- ( ( x e. ~P |^| A /\ s e. A ) -> x e. ~P s )
66	60, 65	sylancom 667	. . . . . . . . 9 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x e. ~P s )
67	59, 66	jca 532	. . . . . . . 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 755	. . . . . . . 8 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x ~<_ om )
69	25	simp3d 1010	. . . . . . . . 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 2826	. . . . . . . 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 60	. . . . . . 7 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> U. x e. s )
72	71	ralrimiva 2871	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> A. s e. A U. x e. s )
73		uniexg 6596	. . . . . . . 8 |- ( x e. ~P |^| A -> U. x e. _V )
74	73	ad2antlr 726	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> U. x e. _V )
75		elintg 4296	. . . . . . 7 |- ( U. x e. _V -> ( U. x e. |^| A <-> A. s e. A U. x e. s ) )
76	74, 75	syl 16	. . . . . 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 232	. . . . 5 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> U. x e. |^| A )
78	77	ex 434	. . . 4 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) -> ( x ~<_ om -> U. x e. |^| A ) )
79	78	ralrimiva 2871	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. x e. ~P |^| A ( x ~<_ om -> U. x e. |^| A ) )
80	39, 56, 79	3jca 1176	. 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 28284	. . 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 485	. 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 1226	1 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. (sigAlgebra ` O ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   E.wex 1613   e. wcel 1819   =/= wne 2652   A.wral 2807   _Vcvv 3109   \ cdif 3468   C_ wss 3471   (/)c0 3793   ~Pcpw 4015   U.cuni 4251   |^|cint 4288   class class class wbr 4456   ` cfv 5594   omcom 6699   ~<_ cdom 7533  sigAlgebracsiga 28280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-int 4289  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-iota 5557  df-fun 5596  df-fv 5602  df-siga 28281

This theorem is referenced by:  sigagensiga  28314