Theorem pmeasadd

Description: A premeasure on a ring of sets is additive on disjoint countable collections. This is called sigma-additivity. (Contributed by Thierry Arnoux, 19-Jul-2020)

	Ref	Expression
Hypotheses	caraext.1	⊢ ( 𝜑 → 𝑃 : 𝑅 ⟶ ( 0 [,] +∞ ) )
	caraext.2	⊢ ( 𝜑 → ( 𝑃 ‘ ∅ ) = 0 )
	caraext.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑃 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) )
	pmeassubadd.q	⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
	pmeassubadd.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑄 )
	pmeassubadd.2	⊢ ( 𝜑 → 𝐴 ≼ ω )
	pmeassubadd.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑅 )
	pmeasadd.4	⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
Assertion	pmeasadd	⊢ ( 𝜑 → ( 𝑃 ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ* 𝑘 ∈ 𝐴 ( 𝑃 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		caraext.1	⊢ ( 𝜑 → 𝑃 : 𝑅 ⟶ ( 0 [,] +∞ ) )
2		caraext.2	⊢ ( 𝜑 → ( 𝑃 ‘ ∅ ) = 0 )
3		caraext.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑃 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) )
4		pmeassubadd.q	⊢ 𝑄 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∪ 𝑦 ) ∈ 𝑠 ∧ ( 𝑥 ∖ 𝑦 ) ∈ 𝑠 ) ) }
5		pmeassubadd.1	⊢ ( 𝜑 → 𝑅 ∈ 𝑄 )
6		pmeassubadd.2	⊢ ( 𝜑 → 𝐴 ≼ ω )
7		pmeassubadd.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑅 )
8		pmeasadd.4	⊢ ( 𝜑 → Disj 𝑘 ∈ 𝐴 𝐵 )
9	7	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑅 )
10		dfiun3g	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑅 → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
11	9 10	syl	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 = ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
12	11	fveq2d	⊢ ( 𝜑 → ( 𝑃 ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = ( 𝑃 ‘ ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
13		mptct	⊢ ( 𝐴 ≼ ω → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )
14		rnct	⊢ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )
15	6 13 14	3syl	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω )
16		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
17	16	rnmptss	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑅 → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 )
18	9 17	syl	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 )
19		disjrnmpt	⊢ ( Disj 𝑘 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 )
20	8 19	syl	⊢ ( 𝜑 → Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 )
21	15 18 20	3jca	⊢ ( 𝜑 → ( ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ∧ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) )
22	21	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ ( ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ∧ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) ) )
23		ctex	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )
24		mptexg	⊢ ( 𝐴 ∈ V → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
25	6 23 24	3syl	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
26		rnexg	⊢ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
27		breq1	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑥 ≼ ω ↔ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ) )
28		sseq1	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑥 ⊆ 𝑅 ↔ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 ) )
29		disjeq1	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → ( Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) )
30	27 28 29	3anbi123d	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → ( ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ↔ ( ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ∧ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) ) )
31	30	anbi2d	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → ( ( 𝜑 ∧ ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ↔ ( 𝜑 ∧ ( ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ∧ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) ) ) )
32		unieq	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → ∪ 𝑥 = ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
33	32	fveq2d	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑃 ‘ ∪ 𝑥 ) = ( 𝑃 ‘ ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
34		esumeq1	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ( 𝑃 ‘ 𝑦 ) )
35	33 34	eqeq12d	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → ( ( 𝑃 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) ↔ ( 𝑃 ‘ ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ( 𝑃 ‘ 𝑦 ) ) )
36	31 35	imbi12d	⊢ ( 𝑥 = ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) → ( ( ( 𝜑 ∧ ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑃 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ ( ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ∧ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) ) → ( 𝑃 ‘ ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ( 𝑃 ‘ 𝑦 ) ) ) )
37	36 3	vtoclg	⊢ ( ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∈ V → ( ( 𝜑 ∧ ( ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ∧ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) ) → ( 𝑃 ‘ ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ( 𝑃 ‘ 𝑦 ) ) )
38	25 26 37	3syl	⊢ ( 𝜑 → ( ( 𝜑 ∧ ( ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ≼ ω ∧ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑅 ∧ Disj 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ) ) → ( 𝑃 ‘ ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ( 𝑃 ‘ 𝑦 ) ) )
39	22 38	mpd	⊢ ( 𝜑 → ( 𝑃 ‘ ∪ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ( 𝑃 ‘ 𝑦 ) )
40		fveq2	⊢ ( 𝑦 = 𝐵 → ( 𝑃 ‘ 𝑦 ) = ( 𝑃 ‘ 𝐵 ) )
41	6 23	syl	⊢ ( 𝜑 → 𝐴 ∈ V )
42	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑃 : 𝑅 ⟶ ( 0 [,] +∞ ) )
43	42 7	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
44		fveq2	⊢ ( 𝐵 = ∅ → ( 𝑃 ‘ 𝐵 ) = ( 𝑃 ‘ ∅ ) )
45	44	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → ( 𝑃 ‘ 𝐵 ) = ( 𝑃 ‘ ∅ ) )
46	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → ( 𝑃 ‘ ∅ ) = 0 )
47	45 46	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝐵 = ∅ ) → ( 𝑃 ‘ 𝐵 ) = 0 )
48	40 41 43 7 47 8	esumrnmpt2	⊢ ( 𝜑 → Σ* 𝑦 ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ( 𝑃 ‘ 𝑦 ) = Σ* 𝑘 ∈ 𝐴 ( 𝑃 ‘ 𝐵 ) )
49	12 39 48	3eqtrd	⊢ ( 𝜑 → ( 𝑃 ‘ ∪ 𝑘 ∈ 𝐴 𝐵 ) = Σ* 𝑘 ∈ 𝐴 ( 𝑃 ‘ 𝐵 ) )