sigaclcu3

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

	Ref	Expression
Hypotheses	sigaclcu3.1	$⊢ φ \to S \in ⋃ ran sigAlgebra$
	sigaclcu3.2	$⊢ φ \to (N = ℕ \lor N = (1 ..^M))$
	sigaclcu3.3	$⊢ (φ \land k \in N) \to A \in S$
Assertion	sigaclcu3	$⊢ φ \to ⋃_{k \in N} A \in S$

Proof

Step	Hyp	Ref	Expression
1		sigaclcu3.1	$⊢ φ \to S \in ⋃ ran sigAlgebra$
2		sigaclcu3.2	$⊢ φ \to (N = ℕ \lor N = (1 ..^M))$
3		sigaclcu3.3	$⊢ (φ \land k \in N) \to A \in S$
4		simpr	$⊢ (φ \land N = ℕ) \to N = ℕ$
5	4	iuneq1d	$⊢ (φ \land N = ℕ) \to ⋃_{k \in N} A = ⋃_{k \in ℕ} A$
6	1	adantr	$⊢ (φ \land N = ℕ) \to S \in ⋃ ran sigAlgebra$
7	3	ralrimiva	$⊢ φ \to \forall k \in N A \in S$
8	7	adantr	$⊢ (φ \land N = ℕ) \to \forall k \in N A \in S$
9	4	raleqdv	$⊢ (φ \land N = ℕ) \to (\forall k \in N A \in S \leftrightarrow \forall k \in ℕ A \in S)$
10	8 9	mpbid	$⊢ (φ \land N = ℕ) \to \forall k \in ℕ A \in S$
11		sigaclcu2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in ℕ A \in S) \to ⋃_{k \in ℕ} A \in S$
12	6 10 11	syl2anc	$⊢ (φ \land N = ℕ) \to ⋃_{k \in ℕ} A \in S$
13	5 12	eqeltrd	$⊢ (φ \land N = ℕ) \to ⋃_{k \in N} A \in S$
14		simpr	$⊢ (φ \land N = (1 ..^M)) \to N = (1 ..^M)$
15	14	iuneq1d	$⊢ (φ \land N = (1 ..^M)) \to ⋃_{k \in N} A = ⋃_{k \in (1 ..^M)} A$
16	1	adantr	$⊢ (φ \land N = (1 ..^M)) \to S \in ⋃ ran sigAlgebra$
17	7	adantr	$⊢ (φ \land N = (1 ..^M)) \to \forall k \in N A \in S$
18	14	raleqdv	$⊢ (φ \land N = (1 ..^M)) \to (\forall k \in N A \in S \leftrightarrow \forall k \in (1 ..^M) A \in S)$
19	17 18	mpbid	$⊢ (φ \land N = (1 ..^M)) \to \forall k \in (1 ..^M) A \in S$
20		sigaclfu2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in (1 ..^M) A \in S) \to ⋃_{k \in (1 ..^M)} A \in S$
21	16 19 20	syl2anc	$⊢ (φ \land N = (1 ..^M)) \to ⋃_{k \in (1 ..^M)} A \in S$
22	15 21	eqeltrd	$⊢ (φ \land N = (1 ..^M)) \to ⋃_{k \in N} A \in S$
23	13 22 2	mpjaodan	$⊢ φ \to ⋃_{k \in N} A \in S$

Metamath Proof Explorer

Theorem sigaclcu3

Proof