Theorem sigaclcu3

Description: A sigma-algebra is closed under countable or finite union. (Contributed by Thierry Arnoux, 6-Mar-2017)

	Ref	Expression
Hypotheses	sigaclcu3.1	|- ( ph -> S e. U. ran sigAlgebra )
	sigaclcu3.2	|- ( ph -> ( N = NN \/ N = ( 1 ..^ M ) ) )
	sigaclcu3.3	|- ( ( ph /\ k e. N ) -> A e. S )
Assertion	sigaclcu3	|- ( ph -> U_ k e. N A e. S )

Proof

Step	Hyp	Ref	Expression
1		sigaclcu3.1	|- ( ph -> S e. U. ran sigAlgebra )
2		sigaclcu3.2	|- ( ph -> ( N = NN \/ N = ( 1 ..^ M ) ) )
3		sigaclcu3.3	|- ( ( ph /\ k e. N ) -> A e. S )
4		simpr	|- ( ( ph /\ N = NN ) -> N = NN )
5	4	iuneq1d	|- ( ( ph /\ N = NN ) -> U_ k e. N A = U_ k e. NN A )
6	1	adantr	|- ( ( ph /\ N = NN ) -> S e. U. ran sigAlgebra )
7	3	ralrimiva	|- ( ph -> A. k e. N A e. S )
8	7	adantr	|- ( ( ph /\ N = NN ) -> A. k e. N A e. S )
9	4	raleqdv	|- ( ( ph /\ N = NN ) -> ( A. k e. N A e. S <-> A. k e. NN A e. S ) )
10	8 9	mpbid	|- ( ( ph /\ N = NN ) -> A. k e. NN A e. S )
11		sigaclcu2	|- ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> U_ k e. NN A e. S )
12	6 10 11	syl2anc	|- ( ( ph /\ N = NN ) -> U_ k e. NN A e. S )
13	5 12	eqeltrd	|- ( ( ph /\ N = NN ) -> U_ k e. N A e. S )
14		simpr	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> N = ( 1 ..^ M ) )
15	14	iuneq1d	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> U_ k e. N A = U_ k e. ( 1 ..^ M ) A )
16	1	adantr	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> S e. U. ran sigAlgebra )
17	7	adantr	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> A. k e. N A e. S )
18	14	raleqdv	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> ( A. k e. N A e. S <-> A. k e. ( 1 ..^ M ) A e. S ) )
19	17 18	mpbid	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> A. k e. ( 1 ..^ M ) A e. S )
20		sigaclfu2	|- ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1 ..^ M ) A e. S ) -> U_ k e. ( 1 ..^ M ) A e. S )
21	16 19 20	syl2anc	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> U_ k e. ( 1 ..^ M ) A e. S )
22	15 21	eqeltrd	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> U_ k e. N A e. S )
23	13 22 2	mpjaodan	|- ( ph -> U_ k e. N A e. S )