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	8 4	raleqtrdv	|- ( ( ph /\ N = NN ) -> A. k e. NN A e. S )
10		sigaclcu2	|- ( ( S e. U. ran sigAlgebra /\ A. k e. NN A e. S ) -> U_ k e. NN A e. S )
11	6 9 10	syl2anc	|- ( ( ph /\ N = NN ) -> U_ k e. NN A e. S )
12	5 11	eqeltrd	|- ( ( ph /\ N = NN ) -> U_ k e. N A e. S )
13		simpr	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> N = ( 1 ..^ M ) )
14	13	iuneq1d	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> U_ k e. N A = U_ k e. ( 1 ..^ M ) A )
15	1	adantr	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> S e. U. ran sigAlgebra )
16	7	adantr	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> A. k e. N A e. S )
17	16 13	raleqtrdv	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> A. k e. ( 1 ..^ M ) A e. S )
18		sigaclfu2	|- ( ( S e. U. ran sigAlgebra /\ A. k e. ( 1 ..^ M ) A e. S ) -> U_ k e. ( 1 ..^ M ) A e. S )
19	15 17 18	syl2anc	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> U_ k e. ( 1 ..^ M ) A e. S )
20	14 19	eqeltrd	|- ( ( ph /\ N = ( 1 ..^ M ) ) -> U_ k e. N A e. S )
21	12 20 2	mpjaodan	|- ( ph -> U_ k e. N A e. S )