Metamath Proof Explorer

Theorem i1f1lem

Description: Lemma for i1f1 and itg11 . (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypothesis i1f1.1 
|- F = ( x e. RR |-> if ( x e. A , 1 , 0 ) )
Assertion i1f1lem 
|- ( F : RR --> { 0 , 1 } /\ ( A e. dom vol -> ( `' F " { 1 } ) = A ) )

Proof

Step Hyp Ref Expression
1 i1f1.1 
 |-  F = ( x e. RR |-> if ( x e. A , 1 , 0 ) )
2 1elpr01 
 |-  1 e. { 0 , 1 }
3 0elpr01 
 |-  0 e. { 0 , 1 }
4 2 3 ifcli 
 |-  if ( x e. A , 1 , 0 ) e. { 0 , 1 }
5 4 rgenw 
 |-  A. x e. RR if ( x e. A , 1 , 0 ) e. { 0 , 1 }
6 1 fmpt 
 |-  ( A. x e. RR if ( x e. A , 1 , 0 ) e. { 0 , 1 } <-> F : RR --> { 0 , 1 } )
7 5 6 mpbi 
 |-  F : RR --> { 0 , 1 }
8 4 a1i 
 |-  ( ( A e. dom vol /\ x e. RR ) -> if ( x e. A , 1 , 0 ) e. { 0 , 1 } )
9 8 1 fmptd 
 |-  ( A e. dom vol -> F : RR --> { 0 , 1 } )
10 ffn 
 |-  ( F : RR --> { 0 , 1 } -> F Fn RR )
11 elpreima 
 |-  ( F Fn RR -> ( y e. ( `' F " { 1 } ) <-> ( y e. RR /\ ( F ` y ) e. { 1 } ) ) )
12 9 10 11 3syl 
 |-  ( A e. dom vol -> ( y e. ( `' F " { 1 } ) <-> ( y e. RR /\ ( F ` y ) e. { 1 } ) ) )
13 fvex 
 |-  ( F ` y ) e. _V
14 13 elsn 
 |-  ( ( F ` y ) e. { 1 } <-> ( F ` y ) = 1 )
15 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
16 15 ifbid 
 |-  ( x = y -> if ( x e. A , 1 , 0 ) = if ( y e. A , 1 , 0 ) )
17 1ex 
 |-  1 e. _V
18 c0ex 
 |-  0 e. _V
19 17 18 ifex 
 |-  if ( y e. A , 1 , 0 ) e. _V
20 16 1 19 fvmpt 
 |-  ( y e. RR -> ( F ` y ) = if ( y e. A , 1 , 0 ) )
21 20 eqeq1d 
 |-  ( y e. RR -> ( ( F ` y ) = 1 <-> if ( y e. A , 1 , 0 ) = 1 ) )
22 0ne1 
 |-  0 =/= 1
23 iffalse 
 |-  ( -. y e. A -> if ( y e. A , 1 , 0 ) = 0 )
24 23 eqeq1d 
 |-  ( -. y e. A -> ( if ( y e. A , 1 , 0 ) = 1 <-> 0 = 1 ) )
25 24 necon3bbid 
 |-  ( -. y e. A -> ( -. if ( y e. A , 1 , 0 ) = 1 <-> 0 =/= 1 ) )
26 22 25 mpbiri 
 |-  ( -. y e. A -> -. if ( y e. A , 1 , 0 ) = 1 )
27 26 con4i 
 |-  ( if ( y e. A , 1 , 0 ) = 1 -> y e. A )
28 iftrue 
 |-  ( y e. A -> if ( y e. A , 1 , 0 ) = 1 )
29 27 28 impbii 
 |-  ( if ( y e. A , 1 , 0 ) = 1 <-> y e. A )
30 21 29 bitrdi 
 |-  ( y e. RR -> ( ( F ` y ) = 1 <-> y e. A ) )
31 14 30 bitrid 
 |-  ( y e. RR -> ( ( F ` y ) e. { 1 } <-> y e. A ) )
32 31 pm5.32i 
 |-  ( ( y e. RR /\ ( F ` y ) e. { 1 } ) <-> ( y e. RR /\ y e. A ) )
33 12 32 bitrdi 
 |-  ( A e. dom vol -> ( y e. ( `' F " { 1 } ) <-> ( y e. RR /\ y e. A ) ) )
34 mblss 
 |-  ( A e. dom vol -> A C_ RR )
35 34 sseld 
 |-  ( A e. dom vol -> ( y e. A -> y e. RR ) )
36 35 pm4.71rd 
 |-  ( A e. dom vol -> ( y e. A <-> ( y e. RR /\ y e. A ) ) )
37 33 36 bitr4d 
 |-  ( A e. dom vol -> ( y e. ( `' F " { 1 } ) <-> y e. A ) )
38 37 eqrdv 
 |-  ( A e. dom vol -> ( `' F " { 1 } ) = A )
39 7 38 pm3.2i 
 |-  ( F : RR --> { 0 , 1 } /\ ( A e. dom vol -> ( `' F " { 1 } ) = A ) )