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 ∈ ℝ ⟼ if x ∈ A 1 0
Assertion i1f1 ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → F ∈ dom ⁡ ∫ 1

Proof

Step Hyp Ref Expression
1 i1f1.1 ⊢ F = x ∈ ℝ ⟼ if x ∈ A 1 0
2 1 i1f1lem ⊢ F : ℝ ⟶ 0 1 ∧ A ∈ dom ⁡ vol → F -1 1 = A
3 2 simpli ⊢ F : ℝ ⟶ 0 1
4 0re ⊢ 0 ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 prssi ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ → 0 1 ⊆ ℝ
7 4 5 6 mp2an ⊢ 0 1 ⊆ ℝ
8 fss ⊢ F : ℝ ⟶ 0 1 ∧ 0 1 ⊆ ℝ → F : ℝ ⟶ ℝ
9 3 7 8 mp2an ⊢ F : ℝ ⟶ ℝ
10 9 a1i ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → F : ℝ ⟶ ℝ
11 prfi ⊢ 0 1 ∈ Fin
12 1ex ⊢ 1 ∈ V
13 12 prid2 ⊢ 1 ∈ 0 1
14 c0ex ⊢ 0 ∈ V
15 14 prid1 ⊢ 0 ∈ 0 1
16 13 15 ifcli ⊢ if x ∈ A 1 0 ∈ 0 1
17 16 a1i ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ x ∈ ℝ → if x ∈ A 1 0 ∈ 0 1
18 17 1 fmptd ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → F : ℝ ⟶ 0 1
19 frn ⊢ F : ℝ ⟶ 0 1 → ran ⁡ F ⊆ 0 1
20 18 19 syl ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → ran ⁡ F ⊆ 0 1
21 ssfi ⊢ 0 1 ∈ Fin ∧ ran ⁡ F ⊆ 0 1 → ran ⁡ F ∈ Fin
22 11 20 21 sylancr ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → ran ⁡ F ∈ Fin
23 3 19 ax-mp ⊢ ran ⁡ F ⊆ 0 1
24 df-pr ⊢ 0 1 = 0 ∪ 1
25 24 equncomi ⊢ 0 1 = 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 -1 y = F -1 1
38 2 simpri ⊢ A ∈ dom ⁡ vol → F -1 1 = A
39 38 adantr ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → F -1 1 = A
40 37 39 sylan9eqr ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ y ∈ ran ⁡ F ∖ 0 → F -1 y = 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 -1 y ∈ dom ⁡ vol
43 40 fveq2d ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ y ∈ ran ⁡ F ∖ 0 → vol ⁡ F -1 y = 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 -1 y ∈ ℝ
46 10 22 42 45 i1fd ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ → F ∈ dom ⁡ ∫ 1