Theorem insiga 27777

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 4603	. . . 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 4304	. . . 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 4019	. . . . . 6 |- ( A e. ~P (sigAlgebra ` O ) -> A C_ (sigAlgebra ` O ) )
8		sigasspw 27756	. . . . . . . 8 |- ( s e. (sigAlgebra ` O ) -> s C_ ~P O )
9		selpw 4017	. . . . . . . 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 3508	. . . . . 6 |- (sigAlgebra ` O ) C_ ~P ~P O
12	7, 11	syl6ss 3516	. . . . 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 4411	. . . 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 3514	. 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 754	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A e. ~P (sigAlgebra ` O ) )
19		elelpwi 4021	. . . . . . . . 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 3116	. . . . . . . . 9 |- s e. _V
22		issiga 27751	. . . . . . . . 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 2878	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. s e. A O e. s )
28		n0 3794	. . . . . . . . 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 1686	. . . . . . 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 5891	. . . . . . 7 |- ( s e. (sigAlgebra ` O ) -> O e. _V )
35	34	exlimiv 1698	. . . . . 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 4290	. . . . 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 4291	. . . . . . . . 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 2833	. . . . . . 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 2878	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> A. s e. A ( O \ x ) e. s )
50		difexg 4595	. . . . . . . 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 4290	. . . . . 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 2878	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. x e. |^| A ( O \ x ) e. |^| A )
57		simplll 757	. . . . . . . . . 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 758	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x e. ~P |^| A )
61		elpwi 4019	. . . . . . . . . . . 12 |- ( x e. ~P |^| A -> x C_ |^| A )
62		intss1 4297	. . . . . . . . . . . 12 |- ( s e. A -> |^| A C_ s )
63	61, 62	sylan9ss 3517	. . . . . . . . . . 11 |- ( ( x e. ~P |^| A /\ s e. A ) -> x C_ s )
64		selpw 4017	. . . . . . . . . . 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 754	. . . . . . . 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 2833	. . . . . . . 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 2878	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> A. s e. A U. x e. s )
73		uniexg 6579	. . . . . . . 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 4290	. . . . . . 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 2878	. . 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 27751	. . 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 1596   e. wcel 1767   =/= wne 2662   A.wral 2814   _Vcvv 3113   \ cdif 3473   C_ wss 3476   (/)c0 3785   ~Pcpw 4010   U.cuni 4245   |^|cint 4282   class class class wbr 4447   ` cfv 5586   omcom 6678   ~<_ cdom 7511  sigAlgebracsiga 27747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-int 4283  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5549  df-fun 5588  df-fv 5594  df-siga 27748

This theorem is referenced by:  sigagensiga  27781