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

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 1ex 
 |-  1 e. _V
3 2 prid2 
 |-  1 e. { 0 , 1 }
4 c0ex 
 |-  0 e. _V
5 4 prid1 
 |-  0 e. { 0 , 1 }
6 3 5 ifcli 
 |-  if ( x e. A , 1 , 0 ) e. { 0 , 1 }
7 6 rgenw 
 |-  A. x e. RR if ( x e. A , 1 , 0 ) e. { 0 , 1 }
8 1 fmpt 
 |-  ( A. x e. RR if ( x e. A , 1 , 0 ) e. { 0 , 1 } <-> F : RR --> { 0 , 1 } )
9 7 8 mpbi 
 |-  F : RR --> { 0 , 1 }
10 6 a1i 
 |-  ( ( A e. dom vol /\ x e. RR ) -> if ( x e. A , 1 , 0 ) e. { 0 , 1 } )
11 10 1 fmptd 
 |-  ( A e. dom vol -> F : RR --> { 0 , 1 } )
12 ffn 
 |-  ( F : RR --> { 0 , 1 } -> F Fn RR )
13 elpreima 
 |-  ( F Fn RR -> ( y e. ( `' F " { 1 } ) <-> ( y e. RR /\ ( F ` y ) e. { 1 } ) ) )
14 11 12 13 3syl 
 |-  ( A e. dom vol -> ( y e. ( `' F " { 1 } ) <-> ( y e. RR /\ ( F ` y ) e. { 1 } ) ) )
15 fvex 
 |-  ( F ` y ) e. _V
16 15 elsn 
 |-  ( ( F ` y ) e. { 1 } <-> ( F ` y ) = 1 )
17 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
18 17 ifbid 
 |-  ( x = y -> if ( x e. A , 1 , 0 ) = if ( y e. A , 1 , 0 ) )
19 2 4 ifex 
 |-  if ( y e. A , 1 , 0 ) e. _V
20 18 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 16 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 14 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 9 38 pm3.2i 
 |-  ( F : RR --> { 0 , 1 } /\ ( A e. dom vol -> ( `' F " { 1 } ) = A ) )