Theorem unelsiga

Description: A sigma-algebra is closed under pairwise unions. (Contributed by Thierry Arnoux, 13-Dec-2016)

	Ref	Expression
Assertion	unelsiga	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A u. B ) e. S )

Proof

Step	Hyp	Ref	Expression
1		uniprg	|- ( ( A e. S /\ B e. S ) -> U. { A , B } = ( A u. B ) )
2	1	3adant1	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> U. { A , B } = ( A u. B ) )
3		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 ) ) ) )
4	3	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 ) ) )
5	4	simp3d	|- ( S e. U. ran sigAlgebra -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
6	5	3ad2ant1	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
7		prct	|- ( ( A e. S /\ B e. S ) -> { A , B } ~<_ _om )
8	7	3adant1	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> { A , B } ~<_ _om )
9		prelpwi	|- ( ( A e. S /\ B e. S ) -> { A , B } e. ~P S )
10		breq1	|- ( x = { A , B } -> ( x ~<_ _om <-> { A , B } ~<_ _om ) )
11		unieq	|- ( x = { A , B } -> U. x = U. { A , B } )
12	11	eleq1d	|- ( x = { A , B } -> ( U. x e. S <-> U. { A , B } e. S ) )
13	10 12	imbi12d	|- ( x = { A , B } -> ( ( x ~<_ _om -> U. x e. S ) <-> ( { A , B } ~<_ _om -> U. { A , B } e. S ) ) )
14	13	rspcv	|- ( { A , B } e. ~P S -> ( A. x e. ~P S ( x ~<_ _om -> U. x e. S ) -> ( { A , B } ~<_ _om -> U. { A , B } e. S ) ) )
15	9 14	syl	|- ( ( A e. S /\ B e. S ) -> ( A. x e. ~P S ( x ~<_ _om -> U. x e. S ) -> ( { A , B } ~<_ _om -> U. { A , B } e. S ) ) )
16	15	3adant1	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A. x e. ~P S ( x ~<_ _om -> U. x e. S ) -> ( { A , B } ~<_ _om -> U. { A , B } e. S ) ) )
17	6 8 16	mp2d	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> U. { A , B } e. S )
18	2 17	eqeltrrd	|- ( ( S e. U. ran sigAlgebra /\ A e. S /\ B e. S ) -> ( A u. B ) e. S )