Theorem sigaclci

Description: A sigma-algebra is closed under countable intersections. Deduction version. The proof uses abrexct rather than abrexdom2jm , and so does not require ax-ac . (Contributed by Thierry Arnoux, 19-Sep-2016) (Revised by Vincent Gonzalez, 19-Aug-2026)

	Ref	Expression
Assertion	sigaclci	|- ( ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) /\ ( A ~<_ _om /\ A =/= (/) ) ) -> |^| A e. S )

Proof

Step	Hyp	Ref	Expression
1		isrnsigau	|- ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
2	1	simprd	|- ( S e. U. ran sigAlgebra -> ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
3	2	simp2d	|- ( S e. U. ran sigAlgebra -> A. x e. S ( U. S \ x ) e. S )
4	3	adantr	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A. x e. S ( U. S \ x ) e. S )
5		elpwi	|- ( A e. ~P S -> A C_ S )
6		ssrexv	|- ( A C_ S -> ( E. z e. A y = ( U. S \ z ) -> E. z e. S y = ( U. S \ z ) ) )
7	5 6	syl	|- ( A e. ~P S -> ( E. z e. A y = ( U. S \ z ) -> E. z e. S y = ( U. S \ z ) ) )
8	7	ss2abdv	|- ( A e. ~P S -> { y | E. z e. A y = ( U. S \ z ) } C_ { y | E. z e. S y = ( U. S \ z ) } )
9		isrnsigau	|- ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. z e. S ( U. S \ z ) e. S /\ A. z e. ~P S ( z ~<_ _om -> U. z e. S ) ) ) )
10	9	simprd	|- ( S e. U. ran sigAlgebra -> ( U. S e. S /\ A. z e. S ( U. S \ z ) e. S /\ A. z e. ~P S ( z ~<_ _om -> U. z e. S ) ) )
11	10	simp2d	|- ( S e. U. ran sigAlgebra -> A. z e. S ( U. S \ z ) e. S )
12		uniiunlem	|- ( A. z e. S ( U. S \ z ) e. S -> ( A. z e. S ( U. S \ z ) e. S <-> { y | E. z e. S y = ( U. S \ z ) } C_ S ) )
13	11 12	syl	|- ( S e. U. ran sigAlgebra -> ( A. z e. S ( U. S \ z ) e. S <-> { y | E. z e. S y = ( U. S \ z ) } C_ S ) )
14	11 13	mpbid	|- ( S e. U. ran sigAlgebra -> { y | E. z e. S y = ( U. S \ z ) } C_ S )
15	8 14	sylan9ssr	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> { y | E. z e. A y = ( U. S \ z ) } C_ S )
16		abrexexg	|- ( A e. ~P S -> { y | E. z e. A y = ( U. S \ z ) } e. _V )
17		elpwg	|- ( { y | E. z e. A y = ( U. S \ z ) } e. _V -> ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S <-> { y | E. z e. A y = ( U. S \ z ) } C_ S ) )
18	16 17	syl	|- ( A e. ~P S -> ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S <-> { y | E. z e. A y = ( U. S \ z ) } C_ S ) )
19	18	adantl	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S <-> { y | E. z e. A y = ( U. S \ z ) } C_ S ) )
20	15 19	mpbird	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> { y | E. z e. A y = ( U. S \ z ) } e. ~P S )
21	2	simp3d	|- ( S e. U. ran sigAlgebra -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
22	21	adantr	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
23	20 22	jca	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
24		abrexct	|- ( A ~<_ _om -> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om )
25	24	adantl	|- ( ( A e. ~P S /\ A ~<_ _om ) -> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om )
26	25	ex	|- ( A e. ~P S -> ( A ~<_ _om -> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om ) )
27	26	adantl	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A ~<_ _om -> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om ) )
28		breq1	|- ( x = { y | E. z e. A y = ( U. S \ z ) } -> ( x ~<_ _om <-> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om ) )
29		unieq	|- ( x = { y | E. z e. A y = ( U. S \ z ) } -> U. x = U. { y | E. z e. A y = ( U. S \ z ) } )
30	29	eleq1d	|- ( x = { y | E. z e. A y = ( U. S \ z ) } -> ( U. x e. S <-> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
31	28 30	imbi12d	|- ( x = { y | E. z e. A y = ( U. S \ z ) } -> ( ( x ~<_ _om -> U. x e. S ) <-> ( { y | E. z e. A y = ( U. S \ z ) } ~<_ _om -> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) ) )
32	31	rspcva	|- ( ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) -> ( { y | E. z e. A y = ( U. S \ z ) } ~<_ _om -> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
33	23 27 32	sylsyld	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A ~<_ _om -> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
34	5	adantl	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A C_ S )
35	11	adantr	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A. z e. S ( U. S \ z ) e. S )
36		ssralv	|- ( A C_ S -> ( A. z e. S ( U. S \ z ) e. S -> A. z e. A ( U. S \ z ) e. S ) )
37	34 35 36	sylc	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A. z e. A ( U. S \ z ) e. S )
38		dfiun2g	|- ( A. z e. A ( U. S \ z ) e. S -> U_ z e. A ( U. S \ z ) = U. { y | E. z e. A y = ( U. S \ z ) } )
39		eleq1	|- ( U_ z e. A ( U. S \ z ) = U. { y | E. z e. A y = ( U. S \ z ) } -> ( U_ z e. A ( U. S \ z ) e. S <-> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
40	37 38 39	3syl	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( U_ z e. A ( U. S \ z ) e. S <-> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
41	33 40	sylibrd	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A ~<_ _om -> U_ z e. A ( U. S \ z ) e. S ) )
42		difeq2	|- ( x = U_ z e. A ( U. S \ z ) -> ( U. S \ x ) = ( U. S \ U_ z e. A ( U. S \ z ) ) )
43	42	eleq1d	|- ( x = U_ z e. A ( U. S \ z ) -> ( ( U. S \ x ) e. S <-> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
44	43	rspccv	|- ( A. x e. S ( U. S \ x ) e. S -> ( U_ z e. A ( U. S \ z ) e. S -> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
45	4 41 44	sylsyld	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A ~<_ _om -> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
46	45	adantrd	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( ( A ~<_ _om /\ A =/= (/) ) -> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
47	46	imp	|- ( ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) /\ ( A ~<_ _om /\ A =/= (/) ) ) -> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S )
48		simpr	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A e. ~P S )
49		pwuni	|- S C_ ~P U. S
50	5 49	sstrdi	|- ( A e. ~P S -> A C_ ~P U. S )
51		iundifdifd	|- ( A C_ ~P U. S -> ( A =/= (/) -> |^| A = ( U. S \ U_ z e. A ( U. S \ z ) ) ) )
52	48 50 51	3syl	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A =/= (/) -> |^| A = ( U. S \ U_ z e. A ( U. S \ z ) ) ) )
53	52	adantld	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( ( A ~<_ _om /\ A =/= (/) ) -> |^| A = ( U. S \ U_ z e. A ( U. S \ z ) ) ) )
54		eleq1	|- ( |^| A = ( U. S \ U_ z e. A ( U. S \ z ) ) -> ( |^| A e. S <-> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
55	53 54	syl6	|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( ( A ~<_ _om /\ A =/= (/) ) -> ( |^| A e. S <-> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) ) )
56	55	imp	|- ( ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) /\ ( A ~<_ _om /\ A =/= (/) ) ) -> ( |^| A e. S <-> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
57	47 56	mpbird	|- ( ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) /\ ( A ~<_ _om /\ A =/= (/) ) ) -> |^| A e. S )