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