Metamath Proof Explorer

Theorem i1f1

Description: Base case simple functions are indicator functions of measurable sets. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypothesis i1f1.1 ⊢F=x∈ℝ⟼ifx∈A10
Assertion i1f1 ⊢A∈dom⁡vol∧vol⁡A∈ℝ→F∈dom⁡∫1

Proof

Step Hyp Ref Expression
1 i1f1.1 ⊢F=x∈ℝ⟼ifx∈A10
2 1 i1f1lem ⊢F:ℝ⟶01∧A∈dom⁡vol→F-11=A
3 2 simpli ⊢F:ℝ⟶01
4 0re ⊢0∈ℝ
5 1re ⊢1∈ℝ
6 prssi ⊢0∈ℝ∧1∈ℝ→01⊆ℝ
7 4 5 6 mp2an ⊢01⊆ℝ
8 fss ⊢F:ℝ⟶01∧01⊆ℝ→F:ℝ⟶ℝ
9 3 7 8 mp2an ⊢F:ℝ⟶ℝ
10 9 a1i ⊢A∈dom⁡vol∧vol⁡A∈ℝ→F:ℝ⟶ℝ
11 prfi ⊢01∈Fin
12 1ex ⊢1∈V
13 12 prid2 ⊢1∈01
14 c0ex ⊢0∈V
15 14 prid1 ⊢0∈01
16 13 15 ifcli ⊢ifx∈A10∈01
17 16 a1i ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧x∈ℝ→ifx∈A10∈01
18 17 1 fmptd ⊢A∈dom⁡vol∧vol⁡A∈ℝ→F:ℝ⟶01
19 frn ⊢F:ℝ⟶01→ran⁡F⊆01
20 18 19 syl ⊢A∈dom⁡vol∧vol⁡A∈ℝ→ran⁡F⊆01
21 ssfi ⊢01∈Fin∧ran⁡F⊆01→ran⁡F∈Fin
22 11 20 21 sylancr ⊢A∈dom⁡vol∧vol⁡A∈ℝ→ran⁡F∈Fin
23 3 19 ax-mp ⊢ran⁡F⊆01
24 df-pr ⊢01=0∪1
25 24 equncomi ⊢01=1∪0
26 23 25 sseqtri ⊢ran⁡F⊆1∪0
27 ssdif ⊢ran⁡F⊆1∪0→ran⁡F∖0⊆1∪0∖0
28 26 27 ax-mp ⊢ran⁡F∖0⊆1∪0∖0
29 difun2 ⊢1∪0∖0=1∖0
30 difss ⊢1∖0⊆1
31 29 30 eqsstri ⊢1∪0∖0⊆1
32 28 31 sstri ⊢ran⁡F∖0⊆1
33 32 sseli ⊢y∈ran⁡F∖0→y∈1
34 elsni ⊢y∈1→y=1
35 33 34 syl ⊢y∈ran⁡F∖0→y=1
36 35 sneqd ⊢y∈ran⁡F∖0→y=1
37 36 imaeq2d ⊢y∈ran⁡F∖0→F-1y=F-11
38 2 simpri ⊢A∈dom⁡vol→F-11=A
39 38 adantr ⊢A∈dom⁡vol∧vol⁡A∈ℝ→F-11=A
40 37 39 sylan9eqr ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧y∈ran⁡F∖0→F-1y=A
41 simpll ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧y∈ran⁡F∖0→A∈dom⁡vol
42 40 41 eqeltrd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧y∈ran⁡F∖0→F-1y∈dom⁡vol
43 40 fveq2d ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧y∈ran⁡F∖0→vol⁡F-1y=vol⁡A
44 simplr ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧y∈ran⁡F∖0→vol⁡A∈ℝ
45 43 44 eqeltrd ⊢A∈dom⁡vol∧vol⁡A∈ℝ∧y∈ran⁡F∖0→vol⁡F-1y∈ℝ
46 10 22 42 45 i1fd ⊢A∈dom⁡vol∧vol⁡A∈ℝ→F∈dom⁡∫1