Step | Hyp | Ref
| Expression |
1 | | simp2 1062 |
. 2
measures
sigAlgebra
sigAlgebra |
2 | | measfrge0 30266 |
. . . . 5
measures
|
3 | 2 | 3ad2ant1 1082 |
. . . 4
measures
sigAlgebra
|
4 | | simp3 1063 |
. . . 4
measures
sigAlgebra
|
5 | 3, 4 | fssresd 6071 |
. . 3
measures
sigAlgebra
|
6 | | 0elsiga 30177 |
. . . . 5
sigAlgebra |
7 | | fvres 6207 |
. . . . 5
|
8 | 1, 6, 7 | 3syl 18 |
. . . 4
measures
sigAlgebra
|
9 | | measvnul 30269 |
. . . . 5
measures
|
10 | 9 | 3ad2ant1 1082 |
. . . 4
measures
sigAlgebra
|
11 | 8, 10 | eqtrd 2656 |
. . 3
measures
sigAlgebra
|
12 | | simp11 1091 |
. . . . . . 7
measures
sigAlgebra
Disj measures |
13 | | simp13 1093 |
. . . . . . . 8
measures
sigAlgebra
Disj |
14 | | simp2 1062 |
. . . . . . . 8
measures
sigAlgebra
Disj |
15 | | sspwb 4917 |
. . . . . . . . 9
|
16 | | ssel2 3598 |
. . . . . . . . 9
|
17 | 15, 16 | sylanb 489 |
. . . . . . . 8
|
18 | 13, 14, 17 | syl2anc 693 |
. . . . . . 7
measures
sigAlgebra
Disj |
19 | | simp3 1063 |
. . . . . . 7
measures
sigAlgebra
Disj Disj |
20 | | measvun 30272 |
. . . . . . 7
measures
Disj Σ* |
21 | 12, 18, 19, 20 | syl3anc 1326 |
. . . . . 6
measures
sigAlgebra
Disj Σ* |
22 | 1 | 3ad2ant1 1082 |
. . . . . . . 8
measures
sigAlgebra
Disj sigAlgebra |
23 | | simp3l 1089 |
. . . . . . . 8
measures
sigAlgebra
Disj |
24 | | sigaclcu 30180 |
. . . . . . . 8
sigAlgebra
|
25 | 22, 14, 23, 24 | syl3anc 1326 |
. . . . . . 7
measures
sigAlgebra
Disj |
26 | | fvres 6207 |
. . . . . . 7
|
27 | 25, 26 | syl 17 |
. . . . . 6
measures
sigAlgebra
Disj |
28 | | elpwi 4168 |
. . . . . . . . . . 11
|
29 | 28 | sselda 3603 |
. . . . . . . . . 10
|
30 | 29 | adantll 750 |
. . . . . . . . 9
measures
sigAlgebra
|
31 | | fvres 6207 |
. . . . . . . . 9
|
32 | 30, 31 | syl 17 |
. . . . . . . 8
measures
sigAlgebra
|
33 | 32 | esumeq2dv 30100 |
. . . . . . 7
measures
sigAlgebra Σ*
Σ* |
34 | 33 | 3adant3 1081 |
. . . . . 6
measures
sigAlgebra
Disj Σ* Σ* |
35 | 21, 27, 34 | 3eqtr4d 2666 |
. . . . 5
measures
sigAlgebra
Disj Σ* |
36 | 35 | 3expia 1267 |
. . . 4
measures
sigAlgebra Disj
Σ* |
37 | 36 | ralrimiva 2966 |
. . 3
measures
sigAlgebra
Disj Σ* |
38 | 5, 11, 37 | 3jca 1242 |
. 2
measures
sigAlgebra
Disj Σ* |
39 | | ismeas 30262 |
. . 3
sigAlgebra measures
Disj Σ* |
40 | 39 | biimprd 238 |
. 2
sigAlgebra
Disj Σ* measures |
41 | 1, 38, 40 | sylc 65 |
1
measures
sigAlgebra
measures |