Theorem omsfval 31554

Description: Value of the outer measure evaluated for a given set 𝐴. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)

Assertion

Ref	Expression
omsfval	⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑅   𝑥,𝐴,𝑦,𝑧   𝑥,𝑄,𝑦,𝑧   𝑥,𝑉,𝑦,𝑧

Proof of Theorem omsfval

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp2 1133	. . . 4 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → 𝑅:𝑄⟶(0[,]+∞))
2		simp1 1132	. . . 4 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → 𝑄 ∈ 𝑉)
3		fex 6991	. . . 4 ⊢ ((𝑅:𝑄⟶(0[,]+∞) ∧ 𝑄 ∈ 𝑉) → 𝑅 ∈ V)
4	1, 2, 3	syl2anc 586	. . 3 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → 𝑅 ∈ V)
5		omsval 31553	. . 3 ⊢ (𝑅 ∈ V → (toOMeas‘𝑅) = (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < )))
6	4, 5	syl 17	. 2 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → (toOMeas‘𝑅) = (𝑎 ∈ 𝒫 ∪ dom 𝑅 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < )))
7		simpr 487	. . . . . . . 8 ⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) ∧ 𝑎 = 𝐴) → 𝑎 = 𝐴)
8	7	sseq1d 4000	. . . . . . 7 ⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) ∧ 𝑎 = 𝐴) → (𝑎 ⊆ ∪ 𝑧 ↔ 𝐴 ⊆ ∪ 𝑧))
9	8	anbi1d 631	. . . . . 6 ⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) ∧ 𝑎 = 𝐴) → ((𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)))
10	9	rabbidv 3482	. . . . 5 ⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) ∧ 𝑎 = 𝐴) → {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} = {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)})
11	10	mpteq1d 5157	. . . 4 ⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) ∧ 𝑎 = 𝐴) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)))
12	11	rneqd 5810	. . 3 ⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) ∧ 𝑎 = 𝐴) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)) = ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)))
13	12	infeq1d 8943	. 2 ⊢ (((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) ∧ 𝑎 = 𝐴) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ))
14		simp3 1134	. . . 4 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → 𝐴 ⊆ ∪ 𝑄)
15		fdm 6524	. . . . . 6 ⊢ (𝑅:𝑄⟶(0[,]+∞) → dom 𝑅 = 𝑄)
16	15	3ad2ant2 1130	. . . . 5 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → dom 𝑅 = 𝑄)
17	16	unieqd 4854	. . . 4 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → ∪ dom 𝑅 = ∪ 𝑄)
18	14, 17	sseqtrrd 4010	. . 3 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → 𝐴 ⊆ ∪ dom 𝑅)
19	2	uniexd 7470	. . . . 5 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → ∪ 𝑄 ∈ V)
20		ssexg 5229	. . . . 5 ⊢ ((𝐴 ⊆ ∪ 𝑄 ∧ ∪ 𝑄 ∈ V) → 𝐴 ∈ V)
21	14, 19, 20	syl2anc 586	. . . 4 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → 𝐴 ∈ V)
22		elpwg 4544	. . . 4 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom 𝑅))
23	21, 22	syl 17	. . 3 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom 𝑅))
24	18, 23	mpbird 259	. 2 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → 𝐴 ∈ 𝒫 ∪ dom 𝑅)
25		xrltso 12537	. . . 4 ⊢ < Or ℝ*
26		iccssxr 12822	. . . . 5 ⊢ (0[,]+∞) ⊆ ℝ*
27		soss 5495	. . . . 5 ⊢ ((0[,]+∞) ⊆ ℝ* → ( < Or ℝ* → < Or (0[,]+∞)))
28	26, 27	ax-mp 5	. . . 4 ⊢ ( < Or ℝ* → < Or (0[,]+∞))
29	25, 28	mp1i 13	. . 3 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → < Or (0[,]+∞))
30	29	infexd 8949	. 2 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ) ∈ V)
31	6, 13, 24, 30	fvmptd 6777	1 ⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑅‘𝑦)), (0[,]+∞), < ))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  {crab 3144  Vcvv 3496   ⊆ wss 3938  𝒫 cpw 4541  ∪ cuni 4840   class class class wbr 5068   ↦ cmpt 5148   Or wor 5475  dom cdm 5557  ran crn 5558  ⟶wf 6353  ‘cfv 6357  (class class class)co 7158  ωcom 7582   ≼ cdom 8509  infcinf 8907  0cc0 10539  +∞cpnf 10674  ℝ^*cxr 10676   < clt 10677  [,]cicc 12744  Σ^*cesum 31288  toOMeascoms 31551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-pre-lttri 10613  ax-pre-lttrn 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-po 5476  df-so 5477  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-1st 7691  df-2nd 7692  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-sup 8908  df-inf 8909  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-icc 12748  df-esum 31289  df-oms 31552

This theorem is referenced by:  omsf  31556  oms0  31557  omsmon  31558  omssubaddlem  31559  omssubadd  31560