Theorem insiga 24473

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 4316	. . . 4 |- ( A =/= (/) <-> |^| A e. _V )
2	1	biimpi 187	. . 3 |- ( A =/= (/) -> |^| A e. _V )
3	2	adantr 452	. 2 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. _V )
4		intssuni 4032	. . . 4 |- ( A =/= (/) -> |^| A C_ U. A )
5	4	adantr 452	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A C_ U. A )
6		simpr 448	. . . . 5 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A e. ~P (sigAlgebra ` O ) )
7		elpwi 3767	. . . . . 6 |- ( A e. ~P (sigAlgebra ` O ) -> A C_ (sigAlgebra ` O ) )
8		sigasspw 24452	. . . . . . . 8 |- ( s e. (sigAlgebra ` O ) -> s C_ ~P O )
9		vex 2919	. . . . . . . . 9 |- s e. _V
10	9	elpw 3765	. . . . . . . 8 |- ( s e. ~P ~P O <-> s C_ ~P O )
11	8, 10	sylibr 204	. . . . . . 7 |- ( s e. (sigAlgebra ` O ) -> s e. ~P ~P O )
12	11	ssriv 3312	. . . . . 6 |- (sigAlgebra ` O ) C_ ~P ~P O
13	7, 12	syl6ss 3320	. . . . 5 |- ( A e. ~P (sigAlgebra ` O ) -> A C_ ~P ~P O )
14	6, 13	syl 16	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A C_ ~P ~P O )
15		sspwuni 4136	. . . 4 |- ( A C_ ~P ~P O <-> U. A C_ ~P O )
16	14, 15	sylib 189	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> U. A C_ ~P O )
17	5, 16	sstrd 3318	. 2 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A C_ ~P O )
18		simpr 448	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> s e. A )
19		simplr 732	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A e. ~P (sigAlgebra ` O ) )
20		elelpwi 3769	. . . . . . . . 9 |- ( ( s e. A /\ A e. ~P (sigAlgebra ` O ) ) -> s e. (sigAlgebra ` O ) )
21	18, 19, 20	syl2anc 643	. . . . . . . 8 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> s e. (sigAlgebra ` O ) )
22		issiga 24447	. . . . . . . . 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	9, 22	ax-mp 8	. . . . . . . 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	21, 23	sylib 189	. . . . . . 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 450	. . . . . 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 969	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> O e. s )
27	26	ralrimiva 2749	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. s e. A O e. s )
28		n0 3597	. . . . . . . . 9 |- ( A =/= (/) <-> E. s s e. A )
29	28	biimpi 187	. . . . . . . 8 |- ( A =/= (/) -> E. s s e. A )
30	29	adantr 452	. . . . . . 7 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> E. s s e. A )
31	21	ex 424	. . . . . . . 8 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( s e. A -> s e. (sigAlgebra ` O ) ) )
32	31	eximdv 1629	. . . . . . 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 5717	. . . . . . 7 |- ( s e. (sigAlgebra ` O ) -> O e. _V )
35	34	exlimiv 1641	. . . . . 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 4018	. . . . 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 224	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> O e. |^| A )
40		simpll 731	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) )
41		simpr 448	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> s e. A )
42	40, 41	jca 519	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) )
43		elinti 4019	. . . . . . . . 9 |- ( x e. |^| A -> ( s e. A -> x e. s ) )
44	43	imp 419	. . . . . . . 8 |- ( ( x e. |^| A /\ s e. A ) -> x e. s )
45	44	adantll 695	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> x e. s )
46	25	simp2d 970	. . . . . . . 8 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A. x e. s ( O \ x ) e. s )
47	46	r19.21bi 2764	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) /\ x e. s ) -> ( O \ x ) e. s )
48	42, 45, 47	syl2anc 643	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( O \ x ) e. s )
49	48	ralrimiva 2749	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> A. s e. A ( O \ x ) e. s )
50		difexg 4311	. . . . . . . 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 452	. . . . . 6 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. _V )
53		elintg 4018	. . . . . 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 224	. . . 4 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. |^| A )
56	55	ralrimiva 2749	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. x e. |^| A ( O \ x ) e. |^| A )
57		simplll 735	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) )
58		simpr 448	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> s e. A )
59	57, 58	jca 519	. . . . . . . . 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 736	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x e. ~P |^| A )
61		elpwi 3767	. . . . . . . . . . . 12 |- ( x e. ~P |^| A -> x C_ |^| A )
62		intss1 4025	. . . . . . . . . . . 12 |- ( s e. A -> |^| A C_ s )
63	61, 62	sylan9ss 3321	. . . . . . . . . . 11 |- ( ( x e. ~P |^| A /\ s e. A ) -> x C_ s )
64		vex 2919	. . . . . . . . . . . 12 |- x e. _V
65	64	elpw 3765	. . . . . . . . . . 11 |- ( x e. ~P s <-> x C_ s )
66	63, 65	sylibr 204	. . . . . . . . . 10 |- ( ( x e. ~P |^| A /\ s e. A ) -> x e. ~P s )
67	60, 66	sylancom 649	. . . . . . . . 9 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x e. ~P s )
68	59, 67	jca 519	. . . . . . . 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 ) )
69		simplr 732	. . . . . . . 8 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x ~<_ om )
70	25	simp3d 971	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A. x e. ~P s ( x ~<_ om -> U. x e. s ) )
71	70	r19.21bi 2764	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) /\ x e. ~P s ) -> ( x ~<_ om -> U. x e. s ) )
72	68, 69, 71	sylc 58	. . . . . . 7 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> U. x e. s )
73	72	ralrimiva 2749	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> A. s e. A U. x e. s )
74		uniexg 4665	. . . . . . . 8 |- ( x e. ~P |^| A -> U. x e. _V )
75	74	ad2antlr 708	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> U. x e. _V )
76		elintg 4018	. . . . . . 7 |- ( U. x e. _V -> ( U. x e. |^| A <-> A. s e. A U. x e. s ) )
77	75, 76	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 ) )
78	73, 77	mpbird 224	. . . . 5 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> U. x e. |^| A )
79	78	ex 424	. . . 4 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) -> ( x ~<_ om -> U. x e. |^| A ) )
80	79	ralrimiva 2749	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. x e. ~P |^| A ( x ~<_ om -> U. x e. |^| A ) )
81	39, 56, 80	3jca 1134	. 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 ) ) )
82		issiga 24447	. . 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 ) ) ) ) )
83	82	biimpar 472	. 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 ) )
84	3, 17, 81, 83	syl12anc 1182	1 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. (sigAlgebra ` O ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   E.wex 1547   e. wcel 1721   =/= wne 2567   A.wral 2666   _Vcvv 2916   \ cdif 3277   C_ wss 3280   (/)c0 3588   ~Pcpw 3759   U.cuni 3975   |^|cint 4010   class class class wbr 4172   omcom 4804   ` cfv 5413   ~<_ cdom 7066  sigAlgebracsiga 24443

This theorem is referenced by:  sigagensiga  24477

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-int 4011  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421  df-siga 24444