Theorem omeiunle

Description: The outer measure of the indexed union of a countable set is less than or equal to the extended sum of the outer measures. The proof uses abrexct rather than fnrndomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 17-Aug-2020) (Revised by Vincent Gonzalez, 19-Aug-2026)

	Ref	Expression
Hypotheses	omeiunle.nph	⊢ Ⅎ 𝑛 𝜑
	omeiunle.ne	⊢ Ⅎ 𝑛 𝐸
	omeiunle.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
	omeiunle.x	⊢ 𝑋 = ∪ dom 𝑂
	omeiunle.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
	omeiunle.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝒫 𝑋 )
Assertion	omeiunle	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		omeiunle.nph	⊢ Ⅎ 𝑛 𝜑
2		omeiunle.ne	⊢ Ⅎ 𝑛 𝐸
3		omeiunle.o	⊢ ( 𝜑 → 𝑂 ∈ OutMeas )
4		omeiunle.x	⊢ 𝑋 = ∪ dom 𝑂
5		omeiunle.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
6		omeiunle.e	⊢ ( 𝜑 → 𝐸 : 𝑍 ⟶ 𝒫 𝑋 )
7		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
8	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 𝑋 )
9		elpwi	⊢ ( ( 𝐸 ‘ 𝑛 ) ∈ 𝒫 𝑋 → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
10	8 9	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
11	10	ex	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 → ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 ) )
12	1 11	ralrimi	⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
13		iunss	⊢ ( ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 ↔ ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
14	12 13	sylibr	⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ⊆ 𝑋 )
15	3 4 14	omecl	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
16	7 15	sselid	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ∈ ℝ* )
17	6	ffnd	⊢ ( 𝜑 → 𝐸 Fn 𝑍 )
18	5	fvexi	⊢ 𝑍 ∈ V
19	18	a1i	⊢ ( 𝜑 → 𝑍 ∈ V )
20		fnex	⊢ ( ( 𝐸 Fn 𝑍 ∧ 𝑍 ∈ V ) → 𝐸 ∈ V )
21	17 19 20	syl2anc	⊢ ( 𝜑 → 𝐸 ∈ V )
22		rnexg	⊢ ( 𝐸 ∈ V → ran 𝐸 ∈ V )
23	21 22	syl	⊢ ( 𝜑 → ran 𝐸 ∈ V )
24	3 4	omef	⊢ ( 𝜑 → 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
25	6	frnd	⊢ ( 𝜑 → ran 𝐸 ⊆ 𝒫 𝑋 )
26	24 25	fssresd	⊢ ( 𝜑 → ( 𝑂 ↾ ran 𝐸 ) : ran 𝐸 ⟶ ( 0 [,] +∞ ) )
27	23 26	sge0xrcl	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) ∈ ℝ* )
28	3	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → 𝑂 ∈ OutMeas )
29	28 4 10	omecl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ∈ ( 0 [,] +∞ ) )
30		eqid	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
31	1 29 30	fmptdf	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) : 𝑍 ⟶ ( 0 [,] +∞ ) )
32	19 31	sge0xrcl	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) ∈ ℝ* )
33		fvex	⊢ ( 𝐸 ‘ 𝑛 ) ∈ V
34	33	rgenw	⊢ ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ V
35		dfiun3g	⊢ ( ∀ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ∈ V → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∪ ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
36	34 35	ax-mp	⊢ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∪ ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) )
37	36	a1i	⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∪ ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
38	6	feqmptd	⊢ ( 𝜑 → 𝐸 = ( 𝑚 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑚 ) ) )
39		nfcv	⊢ Ⅎ 𝑛 𝑚
40	2 39	nffv	⊢ Ⅎ 𝑛 ( 𝐸 ‘ 𝑚 )
41		nfcv	⊢ Ⅎ 𝑚 ( 𝐸 ‘ 𝑛 )
42		fveq2	⊢ ( 𝑚 = 𝑛 → ( 𝐸 ‘ 𝑚 ) = ( 𝐸 ‘ 𝑛 ) )
43	40 41 42	cbvmpt	⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑚 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) )
44	43	a1i	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑚 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
45	38 44	eqtrd	⊢ ( 𝜑 → 𝐸 = ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
46	45	rneqd	⊢ ( 𝜑 → ran 𝐸 = ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
47	46	unieqd	⊢ ( 𝜑 → ∪ ran 𝐸 = ∪ ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) )
48	37 47	eqtr4d	⊢ ( 𝜑 → ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) = ∪ ran 𝐸 )
49	48	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) = ( 𝑂 ‘ ∪ ran 𝐸 ) )
50		eqid	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) )
51	50	rnmpt	⊢ ran ( 𝑛 ∈ 𝑍 ↦ ( 𝐸 ‘ 𝑛 ) ) = { 𝑚 ∣ ∃ 𝑛 ∈ 𝑍 𝑚 = ( 𝐸 ‘ 𝑛 ) }
52	46 51	eqtrdi	⊢ ( 𝜑 → ran 𝐸 = { 𝑚 ∣ ∃ 𝑛 ∈ 𝑍 𝑚 = ( 𝐸 ‘ 𝑛 ) } )
53	5	uzct	⊢ 𝑍 ≼ ω
54	53	a1i	⊢ ( 𝜑 → 𝑍 ≼ ω )
55		abrexct	⊢ ( 𝑍 ≼ ω → { 𝑚 ∣ ∃ 𝑛 ∈ 𝑍 𝑚 = ( 𝐸 ‘ 𝑛 ) } ≼ ω )
56	54 55	syl	⊢ ( 𝜑 → { 𝑚 ∣ ∃ 𝑛 ∈ 𝑍 𝑚 = ( 𝐸 ‘ 𝑛 ) } ≼ ω )
57	52 56	eqbrtrd	⊢ ( 𝜑 → ran 𝐸 ≼ ω )
58	3 4 25 57	omeunile	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ ran 𝐸 ) ≤ ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) )
59	49 58	eqbrtrd	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) )
60		ltweuz	⊢ < We ( ℤ≥ ‘ 𝑁 )
61		weeq2	⊢ ( 𝑍 = ( ℤ≥ ‘ 𝑁 ) → ( < We 𝑍 ↔ < We ( ℤ≥ ‘ 𝑁 ) ) )
62	5 61	ax-mp	⊢ ( < We 𝑍 ↔ < We ( ℤ≥ ‘ 𝑁 ) )
63	60 62	mpbir	⊢ < We 𝑍
64	63	a1i	⊢ ( 𝜑 → < We 𝑍 )
65	19 24 6 64	sge0resrn	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) ≤ ( Σ^ ‘ ( 𝑂 ∘ 𝐸 ) ) )
66		fcompt	⊢ ( ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝐸 : 𝑍 ⟶ 𝒫 𝑋 ) → ( 𝑂 ∘ 𝐸 ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) )
67		nfcv	⊢ Ⅎ 𝑛 𝑂
68	67 40	nffv	⊢ Ⅎ 𝑛 ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) )
69		nfcv	⊢ Ⅎ 𝑚 ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) )
70		2fveq3	⊢ ( 𝑚 = 𝑛 → ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) = ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
71	68 69 70	cbvmpt	⊢ ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) )
72	71	a1i	⊢ ( ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝐸 : 𝑍 ⟶ 𝒫 𝑋 ) → ( 𝑚 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑚 ) ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
73	66 72	eqtrd	⊢ ( ( 𝑂 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝐸 : 𝑍 ⟶ 𝒫 𝑋 ) → ( 𝑂 ∘ 𝐸 ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
74	24 6 73	syl2anc	⊢ ( 𝜑 → ( 𝑂 ∘ 𝐸 ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
75	74	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ∘ 𝐸 ) ) = ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
76	65 75	breqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑂 ↾ ran 𝐸 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )
77	16 27 32 59 76	xrletrd	⊢ ( 𝜑 → ( 𝑂 ‘ ∪ 𝑛 ∈ 𝑍 ( 𝐸 ‘ 𝑛 ) ) ≤ ( Σ^ ‘ ( 𝑛 ∈ 𝑍 ↦ ( 𝑂 ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )