This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )