Step |
Hyp |
Ref |
Expression |
1 |
|
i1f1.1 |
⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) |
2 |
1
|
i1f1lem |
⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } ∧ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) ) |
3 |
2
|
simpli |
⊢ 𝐹 : ℝ ⟶ { 0 , 1 } |
4 |
|
0re |
⊢ 0 ∈ ℝ |
5 |
|
1re |
⊢ 1 ∈ ℝ |
6 |
|
prssi |
⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → { 0 , 1 } ⊆ ℝ ) |
7 |
4 5 6
|
mp2an |
⊢ { 0 , 1 } ⊆ ℝ |
8 |
|
fss |
⊢ ( ( 𝐹 : ℝ ⟶ { 0 , 1 } ∧ { 0 , 1 } ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ ) |
9 |
3 7 8
|
mp2an |
⊢ 𝐹 : ℝ ⟶ ℝ |
10 |
9
|
a1i |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 : ℝ ⟶ ℝ ) |
11 |
|
prfi |
⊢ { 0 , 1 } ∈ Fin |
12 |
|
1ex |
⊢ 1 ∈ V |
13 |
12
|
prid2 |
⊢ 1 ∈ { 0 , 1 } |
14 |
|
c0ex |
⊢ 0 ∈ V |
15 |
14
|
prid1 |
⊢ 0 ∈ { 0 , 1 } |
16 |
13 15
|
ifcli |
⊢ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 } |
17 |
16
|
a1i |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 } ) |
18 |
17 1
|
fmptd |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 : ℝ ⟶ { 0 , 1 } ) |
19 |
|
frn |
⊢ ( 𝐹 : ℝ ⟶ { 0 , 1 } → ran 𝐹 ⊆ { 0 , 1 } ) |
20 |
18 19
|
syl |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ran 𝐹 ⊆ { 0 , 1 } ) |
21 |
|
ssfi |
⊢ ( ( { 0 , 1 } ∈ Fin ∧ ran 𝐹 ⊆ { 0 , 1 } ) → ran 𝐹 ∈ Fin ) |
22 |
11 20 21
|
sylancr |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ran 𝐹 ∈ Fin ) |
23 |
3 19
|
ax-mp |
⊢ ran 𝐹 ⊆ { 0 , 1 } |
24 |
|
df-pr |
⊢ { 0 , 1 } = ( { 0 } ∪ { 1 } ) |
25 |
24
|
equncomi |
⊢ { 0 , 1 } = ( { 1 } ∪ { 0 } ) |
26 |
23 25
|
sseqtri |
⊢ ran 𝐹 ⊆ ( { 1 } ∪ { 0 } ) |
27 |
|
ssdif |
⊢ ( ran 𝐹 ⊆ ( { 1 } ∪ { 0 } ) → ( ran 𝐹 ∖ { 0 } ) ⊆ ( ( { 1 } ∪ { 0 } ) ∖ { 0 } ) ) |
28 |
26 27
|
ax-mp |
⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ ( ( { 1 } ∪ { 0 } ) ∖ { 0 } ) |
29 |
|
difun2 |
⊢ ( ( { 1 } ∪ { 0 } ) ∖ { 0 } ) = ( { 1 } ∖ { 0 } ) |
30 |
|
difss |
⊢ ( { 1 } ∖ { 0 } ) ⊆ { 1 } |
31 |
29 30
|
eqsstri |
⊢ ( ( { 1 } ∪ { 0 } ) ∖ { 0 } ) ⊆ { 1 } |
32 |
28 31
|
sstri |
⊢ ( ran 𝐹 ∖ { 0 } ) ⊆ { 1 } |
33 |
32
|
sseli |
⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑦 ∈ { 1 } ) |
34 |
|
elsni |
⊢ ( 𝑦 ∈ { 1 } → 𝑦 = 1 ) |
35 |
33 34
|
syl |
⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → 𝑦 = 1 ) |
36 |
35
|
sneqd |
⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → { 𝑦 } = { 1 } ) |
37 |
36
|
imaeq2d |
⊢ ( 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) → ( ◡ 𝐹 “ { 𝑦 } ) = ( ◡ 𝐹 “ { 1 } ) ) |
38 |
2
|
simpri |
⊢ ( 𝐴 ∈ dom vol → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) |
39 |
38
|
adantr |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → ( ◡ 𝐹 “ { 1 } ) = 𝐴 ) |
40 |
37 39
|
sylan9eqr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) = 𝐴 ) |
41 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → 𝐴 ∈ dom vol ) |
42 |
40 41
|
eqeltrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ) |
43 |
40
|
fveq2d |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) = ( vol ‘ 𝐴 ) ) |
44 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ 𝐴 ) ∈ ℝ ) |
45 |
43 44
|
eqeltrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) ∧ 𝑦 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ ) |
46 |
10 22 42 45
|
i1fd |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( vol ‘ 𝐴 ) ∈ ℝ ) → 𝐹 ∈ dom ∫1 ) |