Step |
Hyp |
Ref |
Expression |
1 |
|
mbfres2.1 |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ ) |
2 |
|
mbfres2.2 |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) ∈ MblFn ) |
3 |
|
mbfres2.3 |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ MblFn ) |
4 |
|
mbfres2.4 |
⊢ ( 𝜑 → ( 𝐵 ∪ 𝐶 ) = 𝐴 ) |
5 |
4
|
reseq2d |
⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 ∪ 𝐶 ) ) = ( 𝐹 ↾ 𝐴 ) ) |
6 |
|
ffn |
⊢ ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 Fn 𝐴 ) |
7 |
|
fnresdm |
⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
8 |
1 6 7
|
3syl |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
9 |
5 8
|
eqtr2d |
⊢ ( 𝜑 → 𝐹 = ( 𝐹 ↾ ( 𝐵 ∪ 𝐶 ) ) ) |
10 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → 𝐹 = ( 𝐹 ↾ ( 𝐵 ∪ 𝐶 ) ) ) |
11 |
|
resundi |
⊢ ( 𝐹 ↾ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝐹 ↾ 𝐵 ) ∪ ( 𝐹 ↾ 𝐶 ) ) |
12 |
10 11
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → 𝐹 = ( ( 𝐹 ↾ 𝐵 ) ∪ ( 𝐹 ↾ 𝐶 ) ) ) |
13 |
12
|
cnveqd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ◡ 𝐹 = ◡ ( ( 𝐹 ↾ 𝐵 ) ∪ ( 𝐹 ↾ 𝐶 ) ) ) |
14 |
|
cnvun |
⊢ ◡ ( ( 𝐹 ↾ 𝐵 ) ∪ ( 𝐹 ↾ 𝐶 ) ) = ( ◡ ( 𝐹 ↾ 𝐵 ) ∪ ◡ ( 𝐹 ↾ 𝐶 ) ) |
15 |
13 14
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ◡ 𝐹 = ( ◡ ( 𝐹 ↾ 𝐵 ) ∪ ◡ ( 𝐹 ↾ 𝐶 ) ) ) |
16 |
15
|
imaeq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ( ◡ 𝐹 “ 𝑥 ) = ( ( ◡ ( 𝐹 ↾ 𝐵 ) ∪ ◡ ( 𝐹 ↾ 𝐶 ) ) “ 𝑥 ) ) |
17 |
|
imaundir |
⊢ ( ( ◡ ( 𝐹 ↾ 𝐵 ) ∪ ◡ ( 𝐹 ↾ 𝐶 ) ) “ 𝑥 ) = ( ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑥 ) ∪ ( ◡ ( 𝐹 ↾ 𝐶 ) “ 𝑥 ) ) |
18 |
16 17
|
eqtrdi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ( ◡ 𝐹 “ 𝑥 ) = ( ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑥 ) ∪ ( ◡ ( 𝐹 ↾ 𝐶 ) “ 𝑥 ) ) ) |
19 |
|
ssun1 |
⊢ 𝐵 ⊆ ( 𝐵 ∪ 𝐶 ) |
20 |
19 4
|
sseqtrid |
⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 ) |
21 |
1 20
|
fssresd |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ℝ ) |
22 |
|
ismbf |
⊢ ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ℝ → ( ( 𝐹 ↾ 𝐵 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑥 ) ∈ dom vol ) ) |
23 |
21 22
|
syl |
⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑥 ) ∈ dom vol ) ) |
24 |
2 23
|
mpbid |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ran (,) ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑥 ) ∈ dom vol ) |
25 |
24
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑥 ) ∈ dom vol ) |
26 |
|
ssun2 |
⊢ 𝐶 ⊆ ( 𝐵 ∪ 𝐶 ) |
27 |
26 4
|
sseqtrid |
⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 ) |
28 |
1 27
|
fssresd |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ℝ ) |
29 |
|
ismbf |
⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ℝ → ( ( 𝐹 ↾ 𝐶 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ ( 𝐹 ↾ 𝐶 ) “ 𝑥 ) ∈ dom vol ) ) |
30 |
28 29
|
syl |
⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐶 ) ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ ( 𝐹 ↾ 𝐶 ) “ 𝑥 ) ∈ dom vol ) ) |
31 |
3 30
|
mpbid |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ran (,) ( ◡ ( 𝐹 ↾ 𝐶 ) “ 𝑥 ) ∈ dom vol ) |
32 |
31
|
r19.21bi |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ( ◡ ( 𝐹 ↾ 𝐶 ) “ 𝑥 ) ∈ dom vol ) |
33 |
|
unmbl |
⊢ ( ( ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( 𝐹 ↾ 𝐶 ) “ 𝑥 ) ∈ dom vol ) → ( ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑥 ) ∪ ( ◡ ( 𝐹 ↾ 𝐶 ) “ 𝑥 ) ) ∈ dom vol ) |
34 |
25 32 33
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ( ( ◡ ( 𝐹 ↾ 𝐵 ) “ 𝑥 ) ∪ ( ◡ ( 𝐹 ↾ 𝐶 ) “ 𝑥 ) ) ∈ dom vol ) |
35 |
18 34
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) |
36 |
35
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) |
37 |
|
ismbf |
⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) ) |
38 |
1 37
|
syl |
⊢ ( 𝜑 → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) ) |
39 |
36 38
|
mpbird |
⊢ ( 𝜑 → 𝐹 ∈ MblFn ) |