Theorem unmbl 25495

Description: A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014.)

Assertion

Ref	Expression
unmbl	⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol)

Proof of Theorem unmbl

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mblss 25489	. . . 4 ⊢ (𝐴 ∈ dom vol → 𝐴 ⊆ ℝ)
2		mblss 25489	. . . 4 ⊢ (𝐵 ∈ dom vol → 𝐵 ⊆ ℝ)
3	1, 2	anim12i 613	. . 3 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ))
4		unss 4170	. . 3 ⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ↔ (𝐴 ∪ 𝐵) ⊆ ℝ)
5	3, 4	sylib 218	. 2 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ⊆ ℝ)
6		elpwi 4587	. . . 4 ⊢ (𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ)
7		inss1 4217	. . . . . . . . 9 ⊢ (𝑥 ∩ (𝐴 ∪ 𝐵)) ⊆ 𝑥
8		ovolsscl 25444	. . . . . . . . 9 ⊢ (((𝑥 ∩ (𝐴 ∪ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) ∈ ℝ)
9	7, 8	mp3an1 1450	. . . . . . . 8 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) ∈ ℝ)
10	9	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) ∈ ℝ)
11		inss1 4217	. . . . . . . . . 10 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥
12		ovolsscl 25444	. . . . . . . . . 10 ⊢ (((𝑥 ∩ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ)
13	11, 12	mp3an1 1450	. . . . . . . . 9 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ)
14	13	adantl 481	. . . . . . . 8 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ)
15		inss1 4217	. . . . . . . . 9 ⊢ ((𝑥 ∖ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∖ 𝐴)
16		difss 4116	. . . . . . . . . 10 ⊢ (𝑥 ∖ 𝐴) ⊆ 𝑥
17		simprl 770	. . . . . . . . . 10 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → 𝑥 ⊆ ℝ)
18	16, 17	sstrid 3975	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (𝑥 ∖ 𝐴) ⊆ ℝ)
19		ovolsscl 25444	. . . . . . . . . . 11 ⊢ (((𝑥 ∖ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ)
20	16, 19	mp3an1 1450	. . . . . . . . . 10 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ)
21	20	adantl 481	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ)
22		ovolsscl 25444	. . . . . . . . 9 ⊢ ((((𝑥 ∖ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∖ 𝐴) ∧ (𝑥 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) → (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) ∈ ℝ)
23	15, 18, 21, 22	mp3an2i 1468	. . . . . . . 8 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) ∈ ℝ)
24	14, 23	readdcld 11269	. . . . . . 7 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))) ∈ ℝ)
25		difss 4116	. . . . . . . . 9 ⊢ (𝑥 ∖ (𝐴 ∪ 𝐵)) ⊆ 𝑥
26		ovolsscl 25444	. . . . . . . . 9 ⊢ (((𝑥 ∖ (𝐴 ∪ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))) ∈ ℝ)
27	25, 26	mp3an1 1450	. . . . . . . 8 ⊢ ((𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))) ∈ ℝ)
28	27	adantl 481	. . . . . . 7 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))) ∈ ℝ)
29		incom 4189	. . . . . . . . . . . 12 ⊢ ((𝑥 ∖ 𝐴) ∩ 𝐵) = (𝐵 ∩ (𝑥 ∖ 𝐴))
30		indifcom 4263	. . . . . . . . . . . 12 ⊢ (𝐵 ∩ (𝑥 ∖ 𝐴)) = (𝑥 ∩ (𝐵 ∖ 𝐴))
31	29, 30	eqtri 2759	. . . . . . . . . . 11 ⊢ ((𝑥 ∖ 𝐴) ∩ 𝐵) = (𝑥 ∩ (𝐵 ∖ 𝐴))
32	31	uneq2i 4145	. . . . . . . . . 10 ⊢ ((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵)) = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ (𝐵 ∖ 𝐴)))
33		indi 4264	. . . . . . . . . 10 ⊢ (𝑥 ∩ (𝐴 ∪ (𝐵 ∖ 𝐴))) = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ (𝐵 ∖ 𝐴)))
34		undif2 4457	. . . . . . . . . . 11 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
35	34	ineq2i 4197	. . . . . . . . . 10 ⊢ (𝑥 ∩ (𝐴 ∪ (𝐵 ∖ 𝐴))) = (𝑥 ∩ (𝐴 ∪ 𝐵))
36	32, 33, 35	3eqtr2ri 2766	. . . . . . . . 9 ⊢ (𝑥 ∩ (𝐴 ∪ 𝐵)) = ((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵))
37	36	fveq2i 6884	. . . . . . . 8 ⊢ (vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) = (vol*‘((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵)))
38	11, 17	sstrid 3975	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (𝑥 ∩ 𝐴) ⊆ ℝ)
39	15, 18	sstrid 3975	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → ((𝑥 ∖ 𝐴) ∩ 𝐵) ⊆ ℝ)
40		ovolun 25457	. . . . . . . . 9 ⊢ ((((𝑥 ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) ∧ (((𝑥 ∖ 𝐴) ∩ 𝐵) ⊆ ℝ ∧ (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) ∈ ℝ)) → (vol*‘((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))))
41	38, 14, 39, 23, 40	syl22anc 838	. . . . . . . 8 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))))
42	37, 41	eqbrtrid 5159	. . . . . . 7 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))))
43	10, 24, 28, 42	leadd1dd 11856	. . . . . 6 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))))
44		simplr 768	. . . . . . . . . 10 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → 𝐵 ∈ dom vol)
45		mblsplit 25490	. . . . . . . . . 10 ⊢ ((𝐵 ∈ dom vol ∧ (𝑥 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) → (vol*‘(𝑥 ∖ 𝐴)) = ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘((𝑥 ∖ 𝐴) ∖ 𝐵))))
46	44, 18, 21, 45	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘(𝑥 ∖ 𝐴)) = ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘((𝑥 ∖ 𝐴) ∖ 𝐵))))
47		difun1 4279	. . . . . . . . . . 11 ⊢ (𝑥 ∖ (𝐴 ∪ 𝐵)) = ((𝑥 ∖ 𝐴) ∖ 𝐵)
48	47	fveq2i 6884	. . . . . . . . . 10 ⊢ (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))) = (vol*‘((𝑥 ∖ 𝐴) ∖ 𝐵))
49	48	oveq2i 7421	. . . . . . . . 9 ⊢ ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) = ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘((𝑥 ∖ 𝐴) ∖ 𝐵)))
50	46, 49	eqtr4di 2789	. . . . . . . 8 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘(𝑥 ∖ 𝐴)) = ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))))
51	50	oveq2d 7426	. . . . . . 7 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) = ((vol*‘(𝑥 ∩ 𝐴)) + ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))))))
52		simpll 766	. . . . . . . 8 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → 𝐴 ∈ dom vol)
53		simprr 772	. . . . . . . 8 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘𝑥) ∈ ℝ)
54		mblsplit 25490	. . . . . . . 8 ⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))))
55	52, 17, 53, 54	syl3anc 1373	. . . . . . 7 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))))
56	14	recnd 11268	. . . . . . . 8 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℂ)
57	23	recnd 11268	. . . . . . . 8 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) ∈ ℂ)
58	28	recnd 11268	. . . . . . . 8 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))) ∈ ℂ)
59	56, 57, 58	addassd 11262	. . . . . . 7 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) = ((vol*‘(𝑥 ∩ 𝐴)) + ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))))))
60	51, 55, 59	3eqtr4d 2781	. . . . . 6 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → (vol*‘𝑥) = (((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))))
61	43, 60	breqtrrd 5152	. . . . 5 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ)) → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥))
62	61	expr 456	. . . 4 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ 𝑥 ⊆ ℝ) → ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥)))
63	6, 62	sylan2 593	. . 3 ⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ 𝑥 ∈ 𝒫 ℝ) → ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥)))
64	63	ralrimiva 3133	. 2 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥)))
65		ismbl2 25485	. 2 ⊢ ((𝐴 ∪ 𝐵) ∈ dom vol ↔ ((𝐴 ∪ 𝐵) ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫 ℝ((vol*‘𝑥) ∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥))))
66	5, 64, 65	sylanbrc 583	1 ⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3052   ∖ cdif 3928   ∪ cun 3929   ∩ cin 3930   ⊆ wss 3931  𝒫 cpw 4580   class class class wbr 5124  dom cdm 5659  ‘cfv 6536  (class class class)co 7410  ℝcr 11133   + caddc 11137   ≤ cle 11275  vol*covol 25420  volcvol 25421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211  ax-pre-sup 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-sup 9459  df-inf 9460  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900  df-nn 12246  df-2 12308  df-3 12309  df-n0 12507  df-z 12594  df-uz 12858  df-q 12970  df-rp 13014  df-ioo 13371  df-ico 13373  df-icc 13374  df-fz 13530  df-fl 13814  df-seq 14025  df-exp 14085  df-cj 15123  df-re 15124  df-im 15125  df-sqrt 15259  df-abs 15260  df-ovol 25422  df-vol 25423

This theorem is referenced by:  inmbl  25500  finiunmbl  25502  volun  25503  voliunlem1  25508  icombl1  25521  iccmbl  25524  uniiccmbl  25548  mbfimaicc  25589  mbfeqalem2  25600  mbfres2  25603  mbfmax  25607  itgss3  25773  ismblfin  37690  mbfposadd  37696  cnambfre  37697  itg2addnclem2  37701  iblabsnclem  37712  ftc1anclem1  37722  ftc1anclem5  37726  iocmbl  43204