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