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 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) )
Assertion i1f1 ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 ∈ dom ∫1 )

Proof

Step Hyp Ref Expression
1 i1f1.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) )
2 1 i1f1lem ⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } ∧ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) )
3 2 simpli ⊢ 𝐹 : ℝ ⟶ { 0 , 1 }
4 0re ⊢ 0 ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 prssi ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → { 0 , 1 } ⊆ ℝ )
7 4 5 6 mp2an ⊢ { 0 , 1 } ⊆ ℝ
8 fss ⊢ ( ( 𝐹 : ℝ ⟶ { 0 , 1 } ∧ { 0 , 1 } ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
9 3 7 8 mp2an ⊢ 𝐹 : ℝ ⟶ ℝ
10 9 a1i ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
11 prfi ⊢ { 0 , 1 } ∈ Fin
12 1elpr01 ⊢ 1 ∈ { 0 , 1 }
13 0elpr01 ⊢ 0 ∈ { 0 , 1 }
14 12 13 ifcli ⊢ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 }
15 14 a1i ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 } )
16 15 1 fmptd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 : ℝ ⟶ { 0 , 1 } )
17 frn ⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } → ran 𝐹 ⊆ { 0 , 1 } )
18 16 17 syl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ran 𝐹 ⊆ { 0 , 1 } )
19 ssfi ⊢ ( ( { 0 , 1 } ∈ Fin ∧ ran 𝐹 ⊆ { 0 , 1 } ) → ran 𝐹 ∈ Fin )
20 11 18 19 sylancr ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ran 𝐹 ∈ Fin )
21 3 17 ax-mp ⊢ ran 𝐹 ⊆ { 0 , 1 }
22 df-pr ⊢ { 0 , 1 } = ( { 0 } ∪ { 1 } )
23 22 equncomi ⊢ { 0 , 1 } = ( { 1 } ∪ { 0 } )
24 21 23 sseqtri ⊢ ran 𝐹 ⊆ ( { 1 } ∪ { 0 } )
25 ssdif ⊢ ( ran 𝐹 ⊆ ( { 1 } ∪ { 0 } ) → ( ran 𝐹 ∖ { 0 } ) ⊆ ( ( { 1 } ∪ { 0 } ) ∖ { 0 } ) )
26 24 25 ax-mp ⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ( ( { 1 } ∪ { 0 } ) ∖ { 0 } )
27 difun2 ⊢ ( ( { 1 } ∪ { 0 } ) ∖ { 0 } ) = ( { 1 } ∖ { 0 } )
28 difss ⊢ ( { 1 } ∖ { 0 } ) ⊆ { 1 }
29 27 28 eqsstri ⊢ ( ( { 1 } ∪ { 0 } ) ∖ { 0 } ) ⊆ { 1 }
30 26 29 sstri ⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ { 1 }
31 30 sseli ⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑦 ∈ { 1 } )
32 elsni ⊢ ( 𝑦 ∈ { 1 } → 𝑦 = 1 )
33 31 32 syl ⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑦 = 1 )
34 33 sneqd ⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → { 𝑦 } = { 1 } )
35 34 imaeq2d ⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → ( ◡ 𝐹 “ { 𝑦 } ) = ( ◡ 𝐹 “ { 1 } ) )
36 2 simpri ⊢ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 )
37 36 adantr ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ◡ 𝐹 “ { 1 } ) = 𝐴 )
38 35 37 sylan9eqr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) = 𝐴 )
39 simpll ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐴 ∈ dom vol )
40 38 39 eqeltrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
41 38 fveq2d ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) = ( vol ‘ 𝐴 ) )
42 simplr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ 𝐴 ) ∈ ℝ )
43 41 42 eqeltrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
44 10 20 40 43 i1fd ⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 ∈ dom ∫1 )