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 1ex 1 ∈ V
13 12 prid2 1 ∈ { 0 , 1 }
14 c0ex 0 ∈ V
15 14 prid1 0 ∈ { 0 , 1 }
16 13 15 ifcli if ( 𝑥𝐴 , 1 , 0 ) ∈ { 0 , 1 }
17 16 a1i ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥𝐴 , 1 , 0 ) ∈ { 0 , 1 } )
18 17 1 fmptd ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 : ℝ ⟶ { 0 , 1 } )
19 frn ( 𝐹 : ℝ ⟶ { 0 , 1 } → ran 𝐹 ⊆ { 0 , 1 } )
20 18 19 syl ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ran 𝐹 ⊆ { 0 , 1 } )
21 ssfi ( ( { 0 , 1 } ∈ Fin ∧ ran 𝐹 ⊆ { 0 , 1 } ) → ran 𝐹 ∈ Fin )
22 11 20 21 sylancr ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ran 𝐹 ∈ Fin )
23 3 19 ax-mp ran 𝐹 ⊆ { 0 , 1 }
24 df-pr { 0 , 1 } = ( { 0 } ∪ { 1 } )
25 24 equncomi { 0 , 1 } = ( { 1 } ∪ { 0 } )
26 23 25 sseqtri ran 𝐹 ⊆ ( { 1 } ∪ { 0 } )
27 ssdif ( ran 𝐹 ⊆ ( { 1 } ∪ { 0 } ) → ( ran 𝐹 ∖ { 0 } ) ⊆ ( ( { 1 } ∪ { 0 } ) ∖ { 0 } ) )
28 26 27 ax-mp ( ran 𝐹 ∖ { 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 𝐹 ∖ { 0 } ) ⊆ { 1 }
33 32 sseli ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑦 ∈ { 1 } )
34 elsni ( 𝑦 ∈ { 1 } → 𝑦 = 1 )
35 33 34 syl ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑦 = 1 )
36 35 sneqd ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → { 𝑦 } = { 1 } )
37 36 imaeq2d ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → ( 𝐹 “ { 𝑦 } ) = ( 𝐹 “ { 1 } ) )
38 2 simpri ( 𝐴 ∈ dom vol → ( 𝐹 “ { 1 } ) = 𝐴 )
39 38 adantr ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( 𝐹 “ { 1 } ) = 𝐴 )
40 37 39 sylan9eqr ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝐹 “ { 𝑦 } ) = 𝐴 )
41 simpll ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐴 ∈ dom vol )
42 40 41 eqeltrd ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝐹 “ { 𝑦 } ) ∈ dom vol )
43 40 fveq2d ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( 𝐹 “ { 𝑦 } ) ) = ( vol ‘ 𝐴 ) )
44 simplr ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ 𝐴 ) ∈ ℝ )
45 43 44 eqeltrd ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
46 10 22 42 45 i1fd ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 ∈ dom ∫1 )