Theorem carsgclctun 32267

Description: The Caratheodory measurable sets are closed under countable union. (Contributed by Thierry Arnoux, 21-May-2020.)

Hypotheses

Ref	Expression
carsgval.1	⊢ (𝜑 → 𝑂 ∈ 𝑉)
carsgval.2	⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))
carsgsiga.1	⊢ (𝜑 → (𝑀‘∅) = 0)
carsgsiga.2	⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))
carsgsiga.3	⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦))
carsgclctun.1	⊢ (𝜑 → 𝐴 ≼ ω)
carsgclctun.2	⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))

Assertion

Ref	Expression
carsgclctun	⊢ (𝜑 → ∪ 𝐴 ∈ (toCaraSiga‘𝑀))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝑀,𝑦   𝑥,𝑂,𝑦   𝜑,𝑥,𝑦

Allowed substitution hints:   𝑉(𝑥,𝑦)

Proof of Theorem carsgclctun

Dummy variable 𝑒 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		carsgclctun.2	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ (toCaraSiga‘𝑀))
2	1	unissd 4854	. . 3 ⊢ (𝜑 → ∪ 𝐴 ⊆ ∪ (toCaraSiga‘𝑀))
3		carsgval.1	. . . 4 ⊢ (𝜑 → 𝑂 ∈ 𝑉)
4		carsgval.2	. . . 4 ⊢ (𝜑 → 𝑀:𝒫 𝑂⟶(0[,]+∞))
5		carsgsiga.1	. . . 4 ⊢ (𝜑 → (𝑀‘∅) = 0)
6	3, 4, 5	carsguni 32254	. . 3 ⊢ (𝜑 → ∪ (toCaraSiga‘𝑀) = 𝑂)
7	2, 6	sseqtrd 3965	. 2 ⊢ (𝜑 → ∪ 𝐴 ⊆ 𝑂)
8	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝑂 ∈ 𝑉)
9	4	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝑀:𝒫 𝑂⟶(0[,]+∞))
10	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘∅) = 0)
11		carsgsiga.2	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))
12	11	3adant1r 1175	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦))
13		carsgsiga.3	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦))
14	13	3adant1r 1175	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝒫 𝑂) → (𝑀‘𝑥) ≤ (𝑀‘𝑦))
15		carsgclctun.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ≼ ω)
16	15	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝐴 ≼ ω)
17	1	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝐴 ⊆ (toCaraSiga‘𝑀))
18		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → 𝑒 ∈ 𝒫 𝑂)
19	8, 9, 10, 12, 14, 16, 17, 18	carsgclctunlem3 32266	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ≤ (𝑀‘𝑒))
20		inex1g 5246	. . . . . . . . 9 ⊢ (𝑒 ∈ 𝒫 𝑂 → (𝑒 ∩ ∪ 𝐴) ∈ V)
21	20	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∩ ∪ 𝐴) ∈ V)
22		difexg 5254	. . . . . . . . 9 ⊢ (𝑒 ∈ 𝒫 𝑂 → (𝑒 ∖ ∪ 𝐴) ∈ V)
23	22	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∖ ∪ 𝐴) ∈ V)
24		prct 31028	. . . . . . . 8 ⊢ (((𝑒 ∩ ∪ 𝐴) ∈ V ∧ (𝑒 ∖ ∪ 𝐴) ∈ V) → {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω)
25	21, 23, 24	syl2anc 583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω)
26	18	elpwincl1 30853	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∩ ∪ 𝐴) ∈ 𝒫 𝑂)
27	18	elpwdifcl 30854	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑒 ∖ ∪ 𝐴) ∈ 𝒫 𝑂)
28		prssi 4759	. . . . . . . 8 ⊢ (((𝑒 ∩ ∪ 𝐴) ∈ 𝒫 𝑂 ∧ (𝑒 ∖ ∪ 𝐴) ∈ 𝒫 𝑂) → {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂)
29	26, 27, 28	syl2anc 583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂)
30		prex 5358	. . . . . . . . 9 ⊢ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ∈ V
31		breq1 5081	. . . . . . . . . . . 12 ⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → (𝑥 ≼ ω ↔ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω))
32		sseq1 3950	. . . . . . . . . . . 12 ⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → (𝑥 ⊆ 𝒫 𝑂 ↔ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂))
33	31, 32	3anbi23d 1437	. . . . . . . . . . 11 ⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → ((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) ↔ (𝜑 ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂)))
34		unieq 4855	. . . . . . . . . . . . 13 ⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → ∪ 𝑥 = ∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)})
35	34	fveq2d 6772	. . . . . . . . . . . 12 ⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → (𝑀‘∪ 𝑥) = (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}))
36		esumeq1 31981	. . . . . . . . . . . 12 ⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → Σ*𝑦 ∈ 𝑥(𝑀‘𝑦) = Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦))
37	35, 36	breq12d 5091	. . . . . . . . . . 11 ⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → ((𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦) ↔ (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) ≤ Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦)))
38	33, 37	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑥 = {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} → (((𝜑 ∧ 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝒫 𝑂) → (𝑀‘∪ 𝑥) ≤ Σ*𝑦 ∈ 𝑥(𝑀‘𝑦)) ↔ ((𝜑 ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂) → (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) ≤ Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦))))
39	38, 11	vtoclg 3503	. . . . . . . . 9 ⊢ ({(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ∈ V → ((𝜑 ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂) → (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) ≤ Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦)))
40	30, 39	ax-mp 5	. . . . . . . 8 ⊢ ((𝜑 ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂) → (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) ≤ Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦))
41	40	3adant1r 1175	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ≼ ω ∧ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} ⊆ 𝒫 𝑂) → (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) ≤ Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦))
42	25, 29, 41	mpd3an23 1461	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) ≤ Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦))
43		uniprg 4861	. . . . . . . . 9 ⊢ (((𝑒 ∩ ∪ 𝐴) ∈ 𝒫 𝑂 ∧ (𝑒 ∖ ∪ 𝐴) ∈ 𝒫 𝑂) → ∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} = ((𝑒 ∩ ∪ 𝐴) ∪ (𝑒 ∖ ∪ 𝐴)))
44	26, 27, 43	syl2anc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} = ((𝑒 ∩ ∪ 𝐴) ∪ (𝑒 ∖ ∪ 𝐴)))
45		inundif 4417	. . . . . . . 8 ⊢ ((𝑒 ∩ ∪ 𝐴) ∪ (𝑒 ∖ ∪ 𝐴)) = 𝑒
46	44, 45	eqtrdi 2795	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} = 𝑒)
47	46	fveq2d 6772	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘∪ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)}) = (𝑀‘𝑒))
48		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑦 = (𝑒 ∩ ∪ 𝐴)) → 𝑦 = (𝑒 ∩ ∪ 𝐴))
49	48	fveq2d 6772	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑦 = (𝑒 ∩ ∪ 𝐴)) → (𝑀‘𝑦) = (𝑀‘(𝑒 ∩ ∪ 𝐴)))
50		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑦 = (𝑒 ∖ ∪ 𝐴)) → 𝑦 = (𝑒 ∖ ∪ 𝐴))
51	50	fveq2d 6772	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ 𝑦 = (𝑒 ∖ ∪ 𝐴)) → (𝑀‘𝑦) = (𝑀‘(𝑒 ∖ ∪ 𝐴)))
52	9, 26	ffvelrnd 6956	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∩ ∪ 𝐴)) ∈ (0[,]+∞))
53	9, 27	ffvelrnd 6956	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∖ ∪ 𝐴)) ∈ (0[,]+∞))
54		ineq2 4145	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴) → ((𝑒 ∩ ∪ 𝐴) ∩ (𝑒 ∩ ∪ 𝐴)) = ((𝑒 ∩ ∪ 𝐴) ∩ (𝑒 ∖ ∪ 𝐴)))
55		inidm 4157	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∩ ∪ 𝐴) ∩ (𝑒 ∩ ∪ 𝐴)) = (𝑒 ∩ ∪ 𝐴)
56		inindif 30842	. . . . . . . . . . . . 13 ⊢ ((𝑒 ∩ ∪ 𝐴) ∩ (𝑒 ∖ ∪ 𝐴)) = ∅
57	54, 55, 56	3eqtr3g 2802	. . . . . . . . . . . 12 ⊢ ((𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴) → (𝑒 ∩ ∪ 𝐴) = ∅)
58	57	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → (𝑒 ∩ ∪ 𝐴) = ∅)
59	58	fveq2d 6772	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → (𝑀‘(𝑒 ∩ ∪ 𝐴)) = (𝑀‘∅))
60	5	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → (𝑀‘∅) = 0)
61	59, 60	eqtrd 2779	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → (𝑀‘(𝑒 ∩ ∪ 𝐴)) = 0)
62	61	orcd 869	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) ∧ (𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴)) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) = 0 ∨ (𝑀‘(𝑒 ∩ ∪ 𝐴)) = +∞))
63	62	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑒 ∩ ∪ 𝐴) = (𝑒 ∖ ∪ 𝐴) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) = 0 ∨ (𝑀‘(𝑒 ∩ ∪ 𝐴)) = +∞)))
64	49, 51, 26, 27, 52, 53, 63	esumpr2 32014	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → Σ*𝑦 ∈ {(𝑒 ∩ ∪ 𝐴), (𝑒 ∖ ∪ 𝐴)} (𝑀‘𝑦) = ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))))
65	42, 47, 64	3brtr3d 5109	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘𝑒) ≤ ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))))
66	19, 65	jca 511	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ≤ (𝑀‘𝑒) ∧ (𝑀‘𝑒) ≤ ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴)))))
67		iccssxr 13144	. . . . . . 7 ⊢ (0[,]+∞) ⊆ ℝ*
68	67, 52	sselid 3923	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∩ ∪ 𝐴)) ∈ ℝ*)
69	67, 53	sselid 3923	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘(𝑒 ∖ ∪ 𝐴)) ∈ ℝ*)
70	68, 69	xaddcld 13017	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ∈ ℝ*)
71	4	ffvelrnda 6955	. . . . . 6 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘𝑒) ∈ (0[,]+∞))
72	67, 71	sselid 3923	. . . . 5 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (𝑀‘𝑒) ∈ ℝ*)
73		xrletri3 12870	. . . . 5 ⊢ ((((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ∈ ℝ* ∧ (𝑀‘𝑒) ∈ ℝ*) → (((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒) ↔ (((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ≤ (𝑀‘𝑒) ∧ (𝑀‘𝑒) ≤ ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))))))
74	70, 72, 73	syl2anc 583	. . . 4 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → (((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒) ↔ (((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) ≤ (𝑀‘𝑒) ∧ (𝑀‘𝑒) ≤ ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))))))
75	66, 74	mpbird 256	. . 3 ⊢ ((𝜑 ∧ 𝑒 ∈ 𝒫 𝑂) → ((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒))
76	75	ralrimiva 3109	. 2 ⊢ (𝜑 → ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒))
77	3, 4	elcarsg 32251	. 2 ⊢ (𝜑 → (∪ 𝐴 ∈ (toCaraSiga‘𝑀) ↔ (∪ 𝐴 ⊆ 𝑂 ∧ ∀𝑒 ∈ 𝒫 𝑂((𝑀‘(𝑒 ∩ ∪ 𝐴)) +𝑒 (𝑀‘(𝑒 ∖ ∪ 𝐴))) = (𝑀‘𝑒))))
78	7, 76, 77	mpbir2and 709	1 ⊢ (𝜑 → ∪ 𝐴 ∈ (toCaraSiga‘𝑀))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1541   ∈ wcel 2109  ∀wral 3065  Vcvv 3430   ∖ cdif 3888   ∪ cun 3889   ∩ cin 3890   ⊆ wss 3891  ∅c0 4261  𝒫 cpw 4538  {cpr 4568  ∪ cuni 4844   class class class wbr 5078  ⟶wf 6426  ‘cfv 6430  (class class class)co 7268  ωcom 7700   ≼ cdom 8705  0cc0 10855  +∞cpnf 10990  ℝ^*cxr 10992   ≤ cle 10994   +_𝑒 cxad 12828  [,]cicc 13064  Σ^*cesum 31974  toCaraSigaccarsg 32247

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-rep 5213  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-inf2 9360  ax-ac2 10203  ax-cnex 10911  ax-resscn 10912  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-mulcom 10919  ax-addass 10920  ax-mulass 10921  ax-distr 10922  ax-i2m1 10923  ax-1ne0 10924  ax-1rid 10925  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928  ax-pre-lttri 10929  ax-pre-lttrn 10930  ax-pre-ltadd 10931  ax-pre-mulgt0 10932  ax-pre-sup 10933  ax-addf 10934  ax-mulf 10935

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3072  df-rmo 3073  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-int 4885  df-iun 4931  df-iin 4932  df-disj 5044  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-se 5544  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-isom 6439  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-of 7524  df-om 7701  df-1st 7817  df-2nd 7818  df-supp 7962  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-1o 8281  df-2o 8282  df-er 8472  df-map 8591  df-pm 8592  df-ixp 8660  df-en 8708  df-dom 8709  df-sdom 8710  df-fin 8711  df-fsupp 9090  df-fi 9131  df-sup 9162  df-inf 9163  df-oi 9230  df-dju 9643  df-card 9681  df-acn 9684  df-ac 9856  df-pnf 10995  df-mnf 10996  df-xr 10997  df-ltxr 10998  df-le 10999  df-sub 11190  df-neg 11191  df-div 11616  df-nn 11957  df-2 12019  df-3 12020  df-4 12021  df-5 12022  df-6 12023  df-7 12024  df-8 12025  df-9 12026  df-n0 12217  df-z 12303  df-dec 12420  df-uz 12565  df-q 12671  df-rp 12713  df-xneg 12830  df-xadd 12831  df-xmul 12832  df-ioo 13065  df-ioc 13066  df-ico 13067  df-icc 13068  df-fz 13222  df-fzo 13365  df-fl 13493  df-mod 13571  df-seq 13703  df-exp 13764  df-fac 13969  df-bc 13998  df-hash 14026  df-shft 14759  df-cj 14791  df-re 14792  df-im 14793  df-sqrt 14927  df-abs 14928  df-limsup 15161  df-clim 15178  df-rlim 15179  df-sum 15379  df-ef 15758  df-sin 15760  df-cos 15761  df-pi 15763  df-struct 16829  df-sets 16846  df-slot 16864  df-ndx 16876  df-base 16894  df-ress 16923  df-plusg 16956  df-mulr 16957  df-starv 16958  df-sca 16959  df-vsca 16960  df-ip 16961  df-tset 16962  df-ple 16963  df-ds 16965  df-unif 16966  df-hom 16967  df-cco 16968  df-rest 17114  df-topn 17115  df-0g 17133  df-gsum 17134  df-topgen 17135  df-pt 17136  df-prds 17139  df-ordt 17193  df-xrs 17194  df-qtop 17199  df-imas 17200  df-xps 17202  df-mre 17276  df-mrc 17277  df-acs 17279  df-ps 18265  df-tsr 18266  df-plusf 18306  df-mgm 18307  df-sgrp 18356  df-mnd 18367  df-mhm 18411  df-submnd 18412  df-grp 18561  df-minusg 18562  df-sbg 18563  df-mulg 18682  df-subg 18733  df-cntz 18904  df-cmn 19369  df-abl 19370  df-mgp 19702  df-ur 19719  df-ring 19766  df-cring 19767  df-subrg 20003  df-abv 20058  df-lmod 20106  df-scaf 20107  df-sra 20415  df-rgmod 20416  df-psmet 20570  df-xmet 20571  df-met 20572  df-bl 20573  df-mopn 20574  df-fbas 20575  df-fg 20576  df-cnfld 20579  df-top 22024  df-topon 22041  df-topsp 22063  df-bases 22077  df-cld 22151  df-ntr 22152  df-cls 22153  df-nei 22230  df-lp 22268  df-perf 22269  df-cn 22359  df-cnp 22360  df-haus 22447  df-tx 22694  df-hmeo 22887  df-fil 22978  df-fm 23070  df-flim 23071  df-flf 23072  df-tmd 23204  df-tgp 23205  df-tsms 23259  df-trg 23292  df-xms 23454  df-ms 23455  df-tms 23456  df-nm 23719  df-ngp 23720  df-nrg 23722  df-nlm 23723  df-ii 24021  df-cncf 24022  df-limc 25011  df-dv 25012  df-log 25693  df-esum 31975  df-carsg 32248

This theorem is referenced by:  carsgsiga  32268  omsmeas  32269