iunmbl2

Description: The measurable sets are closed under countable union. (Contributed by Mario Carneiro, 18-Mar-2014)

		Ref	Expression
	Assertion	iunmbl2	$⊢ (A ≼ ℕ \land \forall n \in A B \in dom vol) \to ⋃_{n \in A} B \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		brdom2	$⊢ A ≼ ℕ \leftrightarrow (A ≺ ℕ \lor A \approx ℕ)$
2		nnenom	$⊢ ℕ \approx ω$
3		sdomentr	$⊢ (A ≺ ℕ \land ℕ \approx ω) \to A ≺ ω$
4	2 3	mpan2	$⊢ A ≺ ℕ \to A ≺ ω$
5		isfinite	$⊢ A \in Fin \leftrightarrow A ≺ ω$
6		finiunmbl	$⊢ (A \in Fin \land \forall n \in A B \in dom vol) \to ⋃_{n \in A} B \in dom vol$
7	6	ex	$⊢ A \in Fin \to (\forall n \in A B \in dom vol \to ⋃_{n \in A} B \in dom vol)$
8	5 7	sylbir	$⊢ A ≺ ω \to (\forall n \in A B \in dom vol \to ⋃_{n \in A} B \in dom vol)$
9	4 8	syl	$⊢ A ≺ ℕ \to (\forall n \in A B \in dom vol \to ⋃_{n \in A} B \in dom vol)$
10		bren	$⊢ A \approx ℕ \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} ℕ$
11		nfv	$⊢ Ⅎ n f : A \underset{1-1 onto}{⟶} ℕ$
12		nfcv	$⊢ \underline{Ⅎ} n ℕ$
13		nfcsb1v	$⊢ \underline{Ⅎ} n ⦋ f^{-1} (k) / n ⦌ B$
14	13	nfcri	$⊢ Ⅎ n x \in ⦋ f^{-1} (k) / n ⦌ B$
15	12 14	nfrexw	$⊢ Ⅎ n \exists k \in ℕ x \in ⦋ f^{-1} (k) / n ⦌ B$
16		f1of	$⊢ f : A \underset{1-1 onto}{⟶} ℕ \to f : A ⟶ ℕ$
17	16	ffvelcdmda	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land n \in A) \to f (n) \in ℕ$
18	17	3adant3	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land n \in A \land x \in B) \to f (n) \in ℕ$
19		simp3	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land n \in A \land x \in B) \to x \in B$
20		f1ocnvfv1	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land n \in A) \to f^{-1} (f (n)) = n$
21	20	3adant3	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land n \in A \land x \in B) \to f^{-1} (f (n)) = n$
22	21	eqcomd	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land n \in A \land x \in B) \to n = f^{-1} (f (n))$
23		csbeq1a	$⊢ n = f^{-1} (f (n)) \to B = ⦋ f^{-1} (f (n)) / n ⦌ B$
24	22 23	syl	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land n \in A \land x \in B) \to B = ⦋ f^{-1} (f (n)) / n ⦌ B$
25	19 24	eleqtrd	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land n \in A \land x \in B) \to x \in ⦋ f^{-1} (f (n)) / n ⦌ B$
26		fveq2	$⊢ k = f (n) \to f^{-1} (k) = f^{-1} (f (n))$
27	26	csbeq1d	$⊢ k = f (n) \to ⦋ f^{-1} (k) / n ⦌ B = ⦋ f^{-1} (f (n)) / n ⦌ B$
28	27	eleq2d	$⊢ k = f (n) \to (x \in ⦋ f^{-1} (k) / n ⦌ B \leftrightarrow x \in ⦋ f^{-1} (f (n)) / n ⦌ B)$
29	28	rspcev	$⊢ (f (n) \in ℕ \land x \in ⦋ f^{-1} (f (n)) / n ⦌ B) \to \exists k \in ℕ x \in ⦋ f^{-1} (k) / n ⦌ B$
30	18 25 29	syl2anc	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land n \in A \land x \in B) \to \exists k \in ℕ x \in ⦋ f^{-1} (k) / n ⦌ B$
31	30	3exp	$⊢ f : A \underset{1-1 onto}{⟶} ℕ \to (n \in A \to (x \in B \to \exists k \in ℕ x \in ⦋ f^{-1} (k) / n ⦌ B))$
32	11 15 31	rexlimd	$⊢ f : A \underset{1-1 onto}{⟶} ℕ \to (\exists n \in A x \in B \to \exists k \in ℕ x \in ⦋ f^{-1} (k) / n ⦌ B)$
33		f1ocnvdm	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land k \in ℕ) \to f^{-1} (k) \in A$
34		csbeq1a	$⊢ n = f^{-1} (k) \to B = ⦋ f^{-1} (k) / n ⦌ B$
35	34	eleq2d	$⊢ n = f^{-1} (k) \to (x \in B \leftrightarrow x \in ⦋ f^{-1} (k) / n ⦌ B)$
36	14 35	rspce	$⊢ (f^{-1} (k) \in A \land x \in ⦋ f^{-1} (k) / n ⦌ B) \to \exists n \in A x \in B$
37	36	ex	$⊢ f^{-1} (k) \in A \to (x \in ⦋ f^{-1} (k) / n ⦌ B \to \exists n \in A x \in B)$
38	33 37	syl	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land k \in ℕ) \to (x \in ⦋ f^{-1} (k) / n ⦌ B \to \exists n \in A x \in B)$
39	38	rexlimdva	$⊢ f : A \underset{1-1 onto}{⟶} ℕ \to (\exists k \in ℕ x \in ⦋ f^{-1} (k) / n ⦌ B \to \exists n \in A x \in B)$
40	32 39	impbid	$⊢ f : A \underset{1-1 onto}{⟶} ℕ \to (\exists n \in A x \in B \leftrightarrow \exists k \in ℕ x \in ⦋ f^{-1} (k) / n ⦌ B)$
41		eliun	$⊢ x \in ⋃_{n \in A} B \leftrightarrow \exists n \in A x \in B$
42		eliun	$⊢ x \in ⋃_{k \in ℕ} ⦋ f^{-1} (k) / n ⦌ B \leftrightarrow \exists k \in ℕ x \in ⦋ f^{-1} (k) / n ⦌ B$
43	40 41 42	3bitr4g	$⊢ f : A \underset{1-1 onto}{⟶} ℕ \to (x \in ⋃_{n \in A} B \leftrightarrow x \in ⋃_{k \in ℕ} ⦋ f^{-1} (k) / n ⦌ B)$
44	43	eqrdv	$⊢ f : A \underset{1-1 onto}{⟶} ℕ \to ⋃_{n \in A} B = ⋃_{k \in ℕ} ⦋ f^{-1} (k) / n ⦌ B$
45	44	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land \forall n \in A B \in dom vol) \to ⋃_{n \in A} B = ⋃_{k \in ℕ} ⦋ f^{-1} (k) / n ⦌ B$
46		rspcsbela	$⊢ (f^{-1} (k) \in A \land \forall n \in A B \in dom vol) \to ⦋ f^{-1} (k) / n ⦌ B \in dom vol$
47	33 46	sylan	$⊢ ((f : A \underset{1-1 onto}{⟶} ℕ \land k \in ℕ) \land \forall n \in A B \in dom vol) \to ⦋ f^{-1} (k) / n ⦌ B \in dom vol$
48	47	an32s	$⊢ ((f : A \underset{1-1 onto}{⟶} ℕ \land \forall n \in A B \in dom vol) \land k \in ℕ) \to ⦋ f^{-1} (k) / n ⦌ B \in dom vol$
49	48	ralrimiva	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land \forall n \in A B \in dom vol) \to \forall k \in ℕ ⦋ f^{-1} (k) / n ⦌ B \in dom vol$
50		iunmbl	$⊢ \forall k \in ℕ ⦋ f^{-1} (k) / n ⦌ B \in dom vol \to ⋃_{k \in ℕ} ⦋ f^{-1} (k) / n ⦌ B \in dom vol$
51	49 50	syl	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land \forall n \in A B \in dom vol) \to ⋃_{k \in ℕ} ⦋ f^{-1} (k) / n ⦌ B \in dom vol$
52	45 51	eqeltrd	$⊢ (f : A \underset{1-1 onto}{⟶} ℕ \land \forall n \in A B \in dom vol) \to ⋃_{n \in A} B \in dom vol$
53	52	ex	$⊢ f : A \underset{1-1 onto}{⟶} ℕ \to (\forall n \in A B \in dom vol \to ⋃_{n \in A} B \in dom vol)$
54	53	exlimiv	$⊢ \exists f f : A \underset{1-1 onto}{⟶} ℕ \to (\forall n \in A B \in dom vol \to ⋃_{n \in A} B \in dom vol)$
55	10 54	sylbi	$⊢ A \approx ℕ \to (\forall n \in A B \in dom vol \to ⋃_{n \in A} B \in dom vol)$
56	9 55	jaoi	$⊢ (A ≺ ℕ \lor A \approx ℕ) \to (\forall n \in A B \in dom vol \to ⋃_{n \in A} B \in dom vol)$
57	1 56	sylbi	$⊢ A ≼ ℕ \to (\forall n \in A B \in dom vol \to ⋃_{n \in A} B \in dom vol)$
58	57	imp	$⊢ (A ≼ ℕ \land \forall n \in A B \in dom vol) \to ⋃_{n \in A} B \in dom vol$

Metamath Proof Explorer

Theorem iunmbl2

Proof