Step |
Hyp |
Ref |
Expression |
1 |
|
cnvresima |
⊢ ( ◡ ( I ↾ 𝐴 ) “ 𝑥 ) = ( ( ◡ I “ 𝑥 ) ∩ 𝐴 ) |
2 |
|
cnvi |
⊢ ◡ I = I |
3 |
2
|
imaeq1i |
⊢ ( ◡ I “ 𝑥 ) = ( I “ 𝑥 ) |
4 |
|
imai |
⊢ ( I “ 𝑥 ) = 𝑥 |
5 |
3 4
|
eqtri |
⊢ ( ◡ I “ 𝑥 ) = 𝑥 |
6 |
5
|
ineq1i |
⊢ ( ( ◡ I “ 𝑥 ) ∩ 𝐴 ) = ( 𝑥 ∩ 𝐴 ) |
7 |
1 6
|
eqtri |
⊢ ( ◡ ( I ↾ 𝐴 ) “ 𝑥 ) = ( 𝑥 ∩ 𝐴 ) |
8 |
|
ioof |
⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ |
9 |
|
ffn |
⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) ) |
10 |
|
ovelrn |
⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝑥 ∈ ran (,) ↔ ∃ 𝑦 ∈ ℝ* ∃ 𝑧 ∈ ℝ* 𝑥 = ( 𝑦 (,) 𝑧 ) ) ) |
11 |
8 9 10
|
mp2b |
⊢ ( 𝑥 ∈ ran (,) ↔ ∃ 𝑦 ∈ ℝ* ∃ 𝑧 ∈ ℝ* 𝑥 = ( 𝑦 (,) 𝑧 ) ) |
12 |
|
id |
⊢ ( 𝑥 = ( 𝑦 (,) 𝑧 ) → 𝑥 = ( 𝑦 (,) 𝑧 ) ) |
13 |
|
ioombl |
⊢ ( 𝑦 (,) 𝑧 ) ∈ dom vol |
14 |
12 13
|
eqeltrdi |
⊢ ( 𝑥 = ( 𝑦 (,) 𝑧 ) → 𝑥 ∈ dom vol ) |
15 |
14
|
a1i |
⊢ ( ( 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( 𝑥 = ( 𝑦 (,) 𝑧 ) → 𝑥 ∈ dom vol ) ) |
16 |
15
|
rexlimivv |
⊢ ( ∃ 𝑦 ∈ ℝ* ∃ 𝑧 ∈ ℝ* 𝑥 = ( 𝑦 (,) 𝑧 ) → 𝑥 ∈ dom vol ) |
17 |
11 16
|
sylbi |
⊢ ( 𝑥 ∈ ran (,) → 𝑥 ∈ dom vol ) |
18 |
|
id |
⊢ ( 𝐴 ∈ dom vol → 𝐴 ∈ dom vol ) |
19 |
|
inmbl |
⊢ ( ( 𝑥 ∈ dom vol ∧ 𝐴 ∈ dom vol ) → ( 𝑥 ∩ 𝐴 ) ∈ dom vol ) |
20 |
17 18 19
|
syl2anr |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ ran (,) ) → ( 𝑥 ∩ 𝐴 ) ∈ dom vol ) |
21 |
7 20
|
eqeltrid |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ ran (,) ) → ( ◡ ( I ↾ 𝐴 ) “ 𝑥 ) ∈ dom vol ) |
22 |
21
|
ralrimiva |
⊢ ( 𝐴 ∈ dom vol → ∀ 𝑥 ∈ ran (,) ( ◡ ( I ↾ 𝐴 ) “ 𝑥 ) ∈ dom vol ) |
23 |
|
f1oi |
⊢ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴 |
24 |
|
f1of |
⊢ ( ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴 → ( I ↾ 𝐴 ) : 𝐴 ⟶ 𝐴 ) |
25 |
23 24
|
ax-mp |
⊢ ( I ↾ 𝐴 ) : 𝐴 ⟶ 𝐴 |
26 |
|
mblss |
⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ ) |
27 |
|
fss |
⊢ ( ( ( I ↾ 𝐴 ) : 𝐴 ⟶ 𝐴 ∧ 𝐴 ⊆ ℝ ) → ( I ↾ 𝐴 ) : 𝐴 ⟶ ℝ ) |
28 |
25 26 27
|
sylancr |
⊢ ( 𝐴 ∈ dom vol → ( I ↾ 𝐴 ) : 𝐴 ⟶ ℝ ) |
29 |
|
ismbf |
⊢ ( ( I ↾ 𝐴 ) : 𝐴 ⟶ ℝ → ( ( I ↾ 𝐴 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ ( I ↾ 𝐴 ) “ 𝑥 ) ∈ dom vol ) ) |
30 |
28 29
|
syl |
⊢ ( 𝐴 ∈ dom vol → ( ( I ↾ 𝐴 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ ( I ↾ 𝐴 ) “ 𝑥 ) ∈ dom vol ) ) |
31 |
22 30
|
mpbird |
⊢ ( 𝐴 ∈ dom vol → ( I ↾ 𝐴 ) ∈ MblFn ) |