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 syl5bb
 |-  ( 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 ) )