Metamath Proof Explorer


Theorem mbfss

Description: Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses mbfss.1 φ A B
mbfss.2 φ B dom vol
mbfss.3 φ x A C V
mbfss.4 φ x B A C = 0
mbfss.5 φ x A C MblFn
Assertion mbfss φ x B C MblFn

Proof

Step Hyp Ref Expression
1 mbfss.1 φ A B
2 mbfss.2 φ B dom vol
3 mbfss.3 φ x A C V
4 mbfss.4 φ x B A C = 0
5 mbfss.5 φ x A C MblFn
6 elun x A B A x A x B A
7 undif2 A B A = A B
8 ssequn1 A B A B = B
9 1 8 sylib φ A B = B
10 7 9 syl5eq φ A B A = B
11 10 eleq2d φ x A B A x B
12 6 11 bitr3id φ x A x B A x B
13 12 biimpar φ x B x A x B A
14 5 3 mbfmptcl φ x A C
15 0cn 0
16 4 15 eqeltrdi φ x B A C
17 14 16 jaodan φ x A x B A C
18 13 17 syldan φ x B C
19 18 recld φ x B C
20 19 fmpttd φ x B C : B
21 1 resmptd φ x B C A = x A C
22 14 ismbfcn2 φ x A C MblFn x A C MblFn x A C MblFn
23 5 22 mpbid φ x A C MblFn x A C MblFn
24 23 simpld φ x A C MblFn
25 21 24 eqeltrd φ x B C A MblFn
26 difss B A B
27 resmpt B A B x B C B A = x B A C
28 26 27 ax-mp x B C B A = x B A C
29 4 fveq2d φ x B A C = 0
30 re0 0 = 0
31 29 30 eqtrdi φ x B A C = 0
32 31 mpteq2dva φ x B A C = x B A 0
33 28 32 syl5eq φ x B C B A = x B A 0
34 fconstmpt B A × 0 = x B A 0
35 5 3 mbfdm2 φ A dom vol
36 difmbl B dom vol A dom vol B A dom vol
37 2 35 36 syl2anc φ B A dom vol
38 mbfconst B A dom vol 0 B A × 0 MblFn
39 37 15 38 sylancl φ B A × 0 MblFn
40 34 39 eqeltrrid φ x B A 0 MblFn
41 33 40 eqeltrd φ x B C B A MblFn
42 20 25 41 10 mbfres2 φ x B C MblFn
43 18 imcld φ x B C
44 43 fmpttd φ x B C : B
45 1 resmptd φ x B C A = x A C
46 23 simprd φ x A C MblFn
47 45 46 eqeltrd φ x B C A MblFn
48 resmpt B A B x B C B A = x B A C
49 26 48 ax-mp x B C B A = x B A C
50 4 fveq2d φ x B A C = 0
51 im0 0 = 0
52 50 51 eqtrdi φ x B A C = 0
53 52 mpteq2dva φ x B A C = x B A 0
54 49 53 syl5eq φ x B C B A = x B A 0
55 54 40 eqeltrd φ x B C B A MblFn
56 44 47 55 10 mbfres2 φ x B C MblFn
57 18 ismbfcn2 φ x B C MblFn x B C MblFn x B C MblFn
58 42 56 57 mpbir2and φ x B C MblFn