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 e. RR |-> if ( x e. A , 1 , 0 ) )
Assertion i1f1 
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> F e. dom S.1 )

Proof

Step Hyp Ref Expression
1 i1f1.1 
 |-  F = ( x e. RR |-> if ( x e. A , 1 , 0 ) )
2 1 i1f1lem 
 |-  ( F : RR --> { 0 , 1 } /\ ( A e. dom vol -> ( `' F " { 1 } ) = A ) )
3 2 simpli 
 |-  F : RR --> { 0 , 1 }
4 0re 
 |-  0 e. RR
5 1re 
 |-  1 e. RR
6 prssi 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> { 0 , 1 } C_ RR )
7 4 5 6 mp2an 
 |-  { 0 , 1 } C_ RR
8 fss 
 |-  ( ( F : RR --> { 0 , 1 } /\ { 0 , 1 } C_ RR ) -> F : RR --> RR )
9 3 7 8 mp2an 
 |-  F : RR --> RR
10 9 a1i 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> F : RR --> RR )
11 prfi 
 |-  { 0 , 1 } e. Fin
12 1ex 
 |-  1 e. _V
13 12 prid2 
 |-  1 e. { 0 , 1 }
14 c0ex 
 |-  0 e. _V
15 14 prid1 
 |-  0 e. { 0 , 1 }
16 13 15 ifcli 
 |-  if ( x e. A , 1 , 0 ) e. { 0 , 1 }
17 16 a1i 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ x e. RR ) -> if ( x e. A , 1 , 0 ) e. { 0 , 1 } )
18 17 1 fmptd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> F : RR --> { 0 , 1 } )
19 frn 
 |-  ( F : RR --> { 0 , 1 } -> ran F C_ { 0 , 1 } )
20 18 19 syl 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ran F C_ { 0 , 1 } )
21 ssfi 
 |-  ( ( { 0 , 1 } e. Fin /\ ran F C_ { 0 , 1 } ) -> ran F e. Fin )
22 11 20 21 sylancr 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ran F e. Fin )
23 3 19 ax-mp 
 |-  ran F C_ { 0 , 1 }
24 df-pr 
 |-  { 0 , 1 } = ( { 0 } u. { 1 } )
25 24 equncomi 
 |-  { 0 , 1 } = ( { 1 } u. { 0 } )
26 23 25 sseqtri 
 |-  ran F C_ ( { 1 } u. { 0 } )
27 ssdif 
 |-  ( ran F C_ ( { 1 } u. { 0 } ) -> ( ran F \ { 0 } ) C_ ( ( { 1 } u. { 0 } ) \ { 0 } ) )
28 26 27 ax-mp 
 |-  ( ran F \ { 0 } ) C_ ( ( { 1 } u. { 0 } ) \ { 0 } )
29 difun2 
 |-  ( ( { 1 } u. { 0 } ) \ { 0 } ) = ( { 1 } \ { 0 } )
30 difss 
 |-  ( { 1 } \ { 0 } ) C_ { 1 }
31 29 30 eqsstri 
 |-  ( ( { 1 } u. { 0 } ) \ { 0 } ) C_ { 1 }
32 28 31 sstri 
 |-  ( ran F \ { 0 } ) C_ { 1 }
33 32 sseli 
 |-  ( y e. ( ran F \ { 0 } ) -> y e. { 1 } )
34 elsni 
 |-  ( y e. { 1 } -> y = 1 )
35 33 34 syl 
 |-  ( y e. ( ran F \ { 0 } ) -> y = 1 )
36 35 sneqd 
 |-  ( y e. ( ran F \ { 0 } ) -> { y } = { 1 } )
37 36 imaeq2d 
 |-  ( y e. ( ran F \ { 0 } ) -> ( `' F " { y } ) = ( `' F " { 1 } ) )
38 2 simpri 
 |-  ( A e. dom vol -> ( `' F " { 1 } ) = A )
39 38 adantr 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( `' F " { 1 } ) = A )
40 37 39 sylan9eqr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. ( ran F \ { 0 } ) ) -> ( `' F " { y } ) = A )
41 simpll 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. ( ran F \ { 0 } ) ) -> A e. dom vol )
42 40 41 eqeltrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. ( ran F \ { 0 } ) ) -> ( `' F " { y } ) e. dom vol )
43 40 fveq2d 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) = ( vol ` A ) )
44 simplr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. ( ran F \ { 0 } ) ) -> ( vol ` A ) e. RR )
45 43 44 eqeltrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ y e. ( ran F \ { 0 } ) ) -> ( vol ` ( `' F " { y } ) ) e. RR )
46 10 22 42 45 i1fd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> F e. dom S.1 )