sigaclfu2

Description: A sigma-algebra is closed under finite union - indexing on ( 1 ..^ N ) . (Contributed by Thierry Arnoux, 28-Dec-2016)

		Ref	Expression
	Assertion	sigaclfu2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in (1 ..^N) A \in S) \to ⋃_{k \in (1 ..^N)} A \in S$

Proof

Step	Hyp	Ref	Expression
1		iunxun	$⊢ ⋃_{k \in (1 ..^N) \cup (ℕ ∖ (1 ..^N))} if (k \in (1 ..^N), A, \emptyset) = ⋃_{k \in (1 ..^N)} if (k \in (1 ..^N), A, \emptyset) \cup ⋃_{k \in ℕ ∖ (1 ..^N)} if (k \in (1 ..^N), A, \emptyset)$
2		fzossnn	$⊢ (1 ..^N) \subseteq ℕ$
3		undif	$⊢ (1 ..^N) \subseteq ℕ \leftrightarrow (1 ..^N) \cup (ℕ ∖ (1 ..^N)) = ℕ$
4	2 3	mpbi	$⊢ (1 ..^N) \cup (ℕ ∖ (1 ..^N)) = ℕ$
5		iuneq1	$⊢ (1 ..^N) \cup (ℕ ∖ (1 ..^N)) = ℕ \to ⋃_{k \in (1 ..^N) \cup (ℕ ∖ (1 ..^N))} if (k \in (1 ..^N), A, \emptyset) = ⋃_{k \in ℕ} if (k \in (1 ..^N), A, \emptyset)$
6	4 5	ax-mp	$⊢ ⋃_{k \in (1 ..^N) \cup (ℕ ∖ (1 ..^N))} if (k \in (1 ..^N), A, \emptyset) = ⋃_{k \in ℕ} if (k \in (1 ..^N), A, \emptyset)$
7		iftrue	$⊢ k \in (1 ..^N) \to if (k \in (1 ..^N), A, \emptyset) = A$
8	7	iuneq2i	$⊢ ⋃_{k \in (1 ..^N)} if (k \in (1 ..^N), A, \emptyset) = ⋃_{k \in (1 ..^N)} A$
9		eldifn	$⊢ k \in (ℕ ∖ (1 ..^N)) \to \neg k \in (1 ..^N)$
10	9	iffalsed	$⊢ k \in (ℕ ∖ (1 ..^N)) \to if (k \in (1 ..^N), A, \emptyset) = \emptyset$
11	10	iuneq2i	$⊢ ⋃_{k \in ℕ ∖ (1 ..^N)} if (k \in (1 ..^N), A, \emptyset) = ⋃_{k \in ℕ ∖ (1 ..^N)} \emptyset$
12		iun0	$⊢ ⋃_{k \in ℕ ∖ (1 ..^N)} \emptyset = \emptyset$
13	11 12	eqtri	$⊢ ⋃_{k \in ℕ ∖ (1 ..^N)} if (k \in (1 ..^N), A, \emptyset) = \emptyset$
14	8 13	uneq12i	$⊢ ⋃_{k \in (1 ..^N)} if (k \in (1 ..^N), A, \emptyset) \cup ⋃_{k \in ℕ ∖ (1 ..^N)} if (k \in (1 ..^N), A, \emptyset) = ⋃_{k \in (1 ..^N)} A \cup \emptyset$
15	1 6 14	3eqtr3i	$⊢ ⋃_{k \in ℕ} if (k \in (1 ..^N), A, \emptyset) = ⋃_{k \in (1 ..^N)} A \cup \emptyset$
16		un0	$⊢ ⋃_{k \in (1 ..^N)} A \cup \emptyset = ⋃_{k \in (1 ..^N)} A$
17	15 16	eqtri	$⊢ ⋃_{k \in ℕ} if (k \in (1 ..^N), A, \emptyset) = ⋃_{k \in (1 ..^N)} A$
18		0elsiga	$⊢ S \in ⋃ ran sigAlgebra \to \emptyset \in S$
19		simpr	$⊢ (((\emptyset \in S \land (k \in (1 ..^N) \to A \in S)) \land k \in ℕ) \land k \in (1 ..^N)) \to k \in (1 ..^N)$
20		simpllr	$⊢ (((\emptyset \in S \land (k \in (1 ..^N) \to A \in S)) \land k \in ℕ) \land k \in (1 ..^N)) \to (k \in (1 ..^N) \to A \in S)$
21	19 20	mpd	$⊢ (((\emptyset \in S \land (k \in (1 ..^N) \to A \in S)) \land k \in ℕ) \land k \in (1 ..^N)) \to A \in S$
22		simplll	$⊢ (((\emptyset \in S \land (k \in (1 ..^N) \to A \in S)) \land k \in ℕ) \land \neg k \in (1 ..^N)) \to \emptyset \in S$
23	21 22	ifclda	$⊢ ((\emptyset \in S \land (k \in (1 ..^N) \to A \in S)) \land k \in ℕ) \to if (k \in (1 ..^N), A, \emptyset) \in S$
24	23	exp31	$⊢ \emptyset \in S \to ((k \in (1 ..^N) \to A \in S) \to (k \in ℕ \to if (k \in (1 ..^N), A, \emptyset) \in S))$
25	24	ralimdv2	$⊢ \emptyset \in S \to (\forall k \in (1 ..^N) A \in S \to \forall k \in ℕ if (k \in (1 ..^N), A, \emptyset) \in S)$
26	25	imp	$⊢ (\emptyset \in S \land \forall k \in (1 ..^N) A \in S) \to \forall k \in ℕ if (k \in (1 ..^N), A, \emptyset) \in S$
27	18 26	sylan	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in (1 ..^N) A \in S) \to \forall k \in ℕ if (k \in (1 ..^N), A, \emptyset) \in S$
28		sigaclcu2	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in ℕ if (k \in (1 ..^N), A, \emptyset) \in S) \to ⋃_{k \in ℕ} if (k \in (1 ..^N), A, \emptyset) \in S$
29	27 28	syldan	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in (1 ..^N) A \in S) \to ⋃_{k \in ℕ} if (k \in (1 ..^N), A, \emptyset) \in S$
30	17 29	eqeltrrid	$⊢ (S \in ⋃ ran sigAlgebra \land \forall k \in (1 ..^N) A \in S) \to ⋃_{k \in (1 ..^N)} A \in S$

Metamath Proof Explorer

Theorem sigaclfu2

Proof