Theorem insiga 28971

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 4562	. . . 4 |- ( A =/= (/) <-> |^| A e. _V )
2	1	biimpi 198	. . 3 |- ( A =/= (/) -> |^| A e. _V )
3	2	adantr 467	. 2 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. _V )
4		intssuni 4260	. . . 4 |- ( A =/= (/) -> |^| A C_ U. A )
5	4	adantr 467	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A C_ U. A )
6		simpr 463	. . . . 5 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A e. ~P (sigAlgebra ` O ) )
7		elpwi 3962	. . . . . 6 |- ( A e. ~P (sigAlgebra ` O ) -> A C_ (sigAlgebra ` O ) )
8		sigasspw 28950	. . . . . . . 8 |- ( s e. (sigAlgebra ` O ) -> s C_ ~P O )
9		selpw 3960	. . . . . . . 8 |- ( s e. ~P ~P O <-> s C_ ~P O )
10	8, 9	sylibr 216	. . . . . . 7 |- ( s e. (sigAlgebra ` O ) -> s e. ~P ~P O )
11	10	ssriv 3438	. . . . . 6 |- (sigAlgebra ` O ) C_ ~P ~P O
12	7, 11	syl6ss 3446	. . . . 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 4370	. . . 4 |- ( A C_ ~P ~P O <-> U. A C_ ~P O )
15	13, 14	sylib 200	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> U. A C_ ~P O )
16	5, 15	sstrd 3444	. 2 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A C_ ~P O )
17		simpr 463	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> s e. A )
18		simplr 763	. . . . . . . . 9 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A e. ~P (sigAlgebra ` O ) )
19		elelpwi 3964	. . . . . . . . 9 |- ( ( s e. A /\ A e. ~P (sigAlgebra ` O ) ) -> s e. (sigAlgebra ` O ) )
20	17, 18, 19	syl2anc 667	. . . . . . . 8 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> s e. (sigAlgebra ` O ) )
21		vex 3050	. . . . . . . . 9 |- s e. _V
22		issiga 28945	. . . . . . . . 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 200	. . . . . . 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 465	. . . . . 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 1021	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> O e. s )
27	26	ralrimiva 2804	. . . 4 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. s e. A O e. s )
28		n0 3743	. . . . . . . . 9 |- ( A =/= (/) <-> E. s s e. A )
29	28	biimpi 198	. . . . . . . 8 |- ( A =/= (/) -> E. s s e. A )
30	29	adantr 467	. . . . . . 7 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> E. s s e. A )
31	20	ex 436	. . . . . . . 8 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> ( s e. A -> s e. (sigAlgebra ` O ) ) )
32	31	eximdv 1766	. . . . . . 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 5897	. . . . . . 7 |- ( s e. (sigAlgebra ` O ) -> O e. _V )
35	34	exlimiv 1778	. . . . . 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 4245	. . . . 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 236	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> O e. |^| A )
40		simpll 761	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) )
41		simpr 463	. . . . . . . 8 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> s e. A )
42	40, 41	jca 535	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) )
43		elinti 4246	. . . . . . . . 9 |- ( x e. |^| A -> ( s e. A -> x e. s ) )
44	43	imp 431	. . . . . . . 8 |- ( ( x e. |^| A /\ s e. A ) -> x e. s )
45	44	adantll 721	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> x e. s )
46	25	simp2d 1022	. . . . . . . 8 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) -> A. x e. s ( O \ x ) e. s )
47	46	r19.21bi 2759	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ s e. A ) /\ x e. s ) -> ( O \ x ) e. s )
48	42, 45, 47	syl2anc 667	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( O \ x ) e. s )
49	48	ralrimiva 2804	. . . . 5 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> A. s e. A ( O \ x ) e. s )
50		difexg 4554	. . . . . . . 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 467	. . . . . 6 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. _V )
53		elintg 4245	. . . . . 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 236	. . . 4 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. |^| A )
56	55	ralrimiva 2804	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. x e. |^| A ( O \ x ) e. |^| A )
57		simplll 769	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) )
58		simpr 463	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> s e. A )
59	57, 58	jca 535	. . . . . . . . 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 770	. . . . . . . . . 10 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x e. ~P |^| A )
61		elpwi 3962	. . . . . . . . . . . 12 |- ( x e. ~P |^| A -> x C_ |^| A )
62		intss1 4252	. . . . . . . . . . . 12 |- ( s e. A -> |^| A C_ s )
63	61, 62	sylan9ss 3447	. . . . . . . . . . 11 |- ( ( x e. ~P |^| A /\ s e. A ) -> x C_ s )
64		selpw 3960	. . . . . . . . . . 11 |- ( x e. ~P s <-> x C_ s )
65	63, 64	sylibr 216	. . . . . . . . . 10 |- ( ( x e. ~P |^| A /\ s e. A ) -> x e. ~P s )
66	60, 65	sylancom 674	. . . . . . . . 9 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x e. ~P s )
67	59, 66	jca 535	. . . . . . . 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 763	. . . . . . . 8 |- ( ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) /\ s e. A ) -> x ~<_ om )
69	25	simp3d 1023	. . . . . . . . 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 2759	. . . . . . . 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 2804	. . . . . 6 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> A. s e. A U. x e. s )
73		uniexg 6593	. . . . . . . 8 |- ( x e. ~P |^| A -> U. x e. _V )
74	73	ad2antlr 734	. . . . . . 7 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> U. x e. _V )
75		elintg 4245	. . . . . . 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 236	. . . . 5 |- ( ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ om ) -> U. x e. |^| A )
78	77	ex 436	. . . 4 |- ( ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) /\ x e. ~P |^| A ) -> ( x ~<_ om -> U. x e. |^| A ) )
79	78	ralrimiva 2804	. . 3 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> A. x e. ~P |^| A ( x ~<_ om -> U. x e. |^| A ) )
80	39, 56, 79	3jca 1189	. 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 28945	. . 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 488	. 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 1267	1 |- ( ( A =/= (/) /\ A e. ~P (sigAlgebra ` O ) ) -> |^| A e. (sigAlgebra ` O ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 986   E.wex 1665   e. wcel 1889   =/= wne 2624   A.wral 2739   _Vcvv 3047   \ cdif 3403   C_ wss 3406   (/)c0 3733   ~Pcpw 3953   U.cuni 4201   |^|cint 4237   class class class wbr 4405   ` cfv 5585   omcom 6697   ~<_ cdom 7572  sigAlgebracsiga 28941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-fal 1452  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-int 4238  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5549  df-fun 5587  df-fv 5593  df-siga 28942

This theorem is referenced by:  sigagensiga  28975