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 )