Step |
Hyp |
Ref |
Expression |
1 |
|
voliun.1 |
|- S = seq 1 ( + , G ) |
2 |
|
voliun.2 |
|- G = ( n e. NN |-> ( vol ` A ) ) |
3 |
|
simpl |
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR ) -> A e. dom vol ) |
4 |
3
|
ralimi |
|- ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) -> A. n e. NN A e. dom vol ) |
5 |
4
|
adantr |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> A. n e. NN A e. dom vol ) |
6 |
|
eqid |
|- ( n e. NN |-> A ) = ( n e. NN |-> A ) |
7 |
6
|
fmpt |
|- ( A. n e. NN A e. dom vol <-> ( n e. NN |-> A ) : NN --> dom vol ) |
8 |
5 7
|
sylib |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( n e. NN |-> A ) : NN --> dom vol ) |
9 |
6
|
fvmpt2 |
|- ( ( n e. NN /\ A e. dom vol ) -> ( ( n e. NN |-> A ) ` n ) = A ) |
10 |
9
|
adantrr |
|- ( ( n e. NN /\ ( A e. dom vol /\ ( vol ` A ) e. RR ) ) -> ( ( n e. NN |-> A ) ` n ) = A ) |
11 |
10
|
ralimiaa |
|- ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) -> A. n e. NN ( ( n e. NN |-> A ) ` n ) = A ) |
12 |
|
disjeq2 |
|- ( A. n e. NN ( ( n e. NN |-> A ) ` n ) = A -> ( Disj_ n e. NN ( ( n e. NN |-> A ) ` n ) <-> Disj_ n e. NN A ) ) |
13 |
11 12
|
syl |
|- ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) -> ( Disj_ n e. NN ( ( n e. NN |-> A ) ` n ) <-> Disj_ n e. NN A ) ) |
14 |
13
|
biimpar |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> Disj_ n e. NN ( ( n e. NN |-> A ) ` n ) ) |
15 |
|
nfcv |
|- F/_ i ( ( n e. NN |-> A ) ` n ) |
16 |
|
nffvmpt1 |
|- F/_ n ( ( n e. NN |-> A ) ` i ) |
17 |
|
fveq2 |
|- ( n = i -> ( ( n e. NN |-> A ) ` n ) = ( ( n e. NN |-> A ) ` i ) ) |
18 |
15 16 17
|
cbvdisj |
|- ( Disj_ n e. NN ( ( n e. NN |-> A ) ` n ) <-> Disj_ i e. NN ( ( n e. NN |-> A ) ` i ) ) |
19 |
14 18
|
sylib |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> Disj_ i e. NN ( ( n e. NN |-> A ) ` i ) ) |
20 |
|
eqid |
|- ( m e. NN |-> ( vol* ` ( x i^i ( ( n e. NN |-> A ) ` m ) ) ) ) = ( m e. NN |-> ( vol* ` ( x i^i ( ( n e. NN |-> A ) ` m ) ) ) ) |
21 |
|
eqid |
|- seq 1 ( + , ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) ) = seq 1 ( + , ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) ) |
22 |
|
nfcv |
|- F/_ m ( vol ` ( ( n e. NN |-> A ) ` n ) ) |
23 |
|
nfcv |
|- F/_ n vol |
24 |
|
nffvmpt1 |
|- F/_ n ( ( n e. NN |-> A ) ` m ) |
25 |
23 24
|
nffv |
|- F/_ n ( vol ` ( ( n e. NN |-> A ) ` m ) ) |
26 |
|
2fveq3 |
|- ( n = m -> ( vol ` ( ( n e. NN |-> A ) ` n ) ) = ( vol ` ( ( n e. NN |-> A ) ` m ) ) ) |
27 |
22 25 26
|
cbvmpt |
|- ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) = ( m e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` m ) ) ) |
28 |
9
|
fveq2d |
|- ( ( n e. NN /\ A e. dom vol ) -> ( vol ` ( ( n e. NN |-> A ) ` n ) ) = ( vol ` A ) ) |
29 |
28
|
eleq1d |
|- ( ( n e. NN /\ A e. dom vol ) -> ( ( vol ` ( ( n e. NN |-> A ) ` n ) ) e. RR <-> ( vol ` A ) e. RR ) ) |
30 |
29
|
biimprd |
|- ( ( n e. NN /\ A e. dom vol ) -> ( ( vol ` A ) e. RR -> ( vol ` ( ( n e. NN |-> A ) ` n ) ) e. RR ) ) |
31 |
30
|
impr |
|- ( ( n e. NN /\ ( A e. dom vol /\ ( vol ` A ) e. RR ) ) -> ( vol ` ( ( n e. NN |-> A ) ` n ) ) e. RR ) |
32 |
31
|
ralimiaa |
|- ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) -> A. n e. NN ( vol ` ( ( n e. NN |-> A ) ` n ) ) e. RR ) |
33 |
32
|
adantr |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> A. n e. NN ( vol ` ( ( n e. NN |-> A ) ` n ) ) e. RR ) |
34 |
|
nfv |
|- F/ i ( vol ` ( ( n e. NN |-> A ) ` n ) ) e. RR |
35 |
23 16
|
nffv |
|- F/_ n ( vol ` ( ( n e. NN |-> A ) ` i ) ) |
36 |
35
|
nfel1 |
|- F/ n ( vol ` ( ( n e. NN |-> A ) ` i ) ) e. RR |
37 |
|
2fveq3 |
|- ( n = i -> ( vol ` ( ( n e. NN |-> A ) ` n ) ) = ( vol ` ( ( n e. NN |-> A ) ` i ) ) ) |
38 |
37
|
eleq1d |
|- ( n = i -> ( ( vol ` ( ( n e. NN |-> A ) ` n ) ) e. RR <-> ( vol ` ( ( n e. NN |-> A ) ` i ) ) e. RR ) ) |
39 |
34 36 38
|
cbvralw |
|- ( A. n e. NN ( vol ` ( ( n e. NN |-> A ) ` n ) ) e. RR <-> A. i e. NN ( vol ` ( ( n e. NN |-> A ) ` i ) ) e. RR ) |
40 |
33 39
|
sylib |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> A. i e. NN ( vol ` ( ( n e. NN |-> A ) ` i ) ) e. RR ) |
41 |
8 19 20 21 27 40
|
voliunlem3 |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( vol ` U. ran ( n e. NN |-> A ) ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) ) , RR* , < ) ) |
42 |
|
dfiun2g |
|- ( A. n e. NN A e. dom vol -> U_ n e. NN A = U. { x | E. n e. NN x = A } ) |
43 |
5 42
|
syl |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> U_ n e. NN A = U. { x | E. n e. NN x = A } ) |
44 |
6
|
rnmpt |
|- ran ( n e. NN |-> A ) = { x | E. n e. NN x = A } |
45 |
44
|
unieqi |
|- U. ran ( n e. NN |-> A ) = U. { x | E. n e. NN x = A } |
46 |
43 45
|
eqtr4di |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> U_ n e. NN A = U. ran ( n e. NN |-> A ) ) |
47 |
46
|
fveq2d |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = ( vol ` U. ran ( n e. NN |-> A ) ) ) |
48 |
|
eqid |
|- NN = NN |
49 |
28
|
adantrr |
|- ( ( n e. NN /\ ( A e. dom vol /\ ( vol ` A ) e. RR ) ) -> ( vol ` ( ( n e. NN |-> A ) ` n ) ) = ( vol ` A ) ) |
50 |
49
|
ralimiaa |
|- ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) -> A. n e. NN ( vol ` ( ( n e. NN |-> A ) ` n ) ) = ( vol ` A ) ) |
51 |
50
|
adantr |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> A. n e. NN ( vol ` ( ( n e. NN |-> A ) ` n ) ) = ( vol ` A ) ) |
52 |
|
mpteq12 |
|- ( ( NN = NN /\ A. n e. NN ( vol ` ( ( n e. NN |-> A ) ` n ) ) = ( vol ` A ) ) -> ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) = ( n e. NN |-> ( vol ` A ) ) ) |
53 |
48 51 52
|
sylancr |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) = ( n e. NN |-> ( vol ` A ) ) ) |
54 |
2 53
|
eqtr4id |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> G = ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) ) |
55 |
54
|
seqeq3d |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> seq 1 ( + , G ) = seq 1 ( + , ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) ) ) |
56 |
1 55
|
eqtrid |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> S = seq 1 ( + , ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) ) ) |
57 |
56
|
rneqd |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ran S = ran seq 1 ( + , ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) ) ) |
58 |
57
|
supeq1d |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> sup ( ran S , RR* , < ) = sup ( ran seq 1 ( + , ( n e. NN |-> ( vol ` ( ( n e. NN |-> A ) ` n ) ) ) ) , RR* , < ) ) |
59 |
41 47 58
|
3eqtr4d |
|- ( ( A. n e. NN ( A e. dom vol /\ ( vol ` A ) e. RR ) /\ Disj_ n e. NN A ) -> ( vol ` U_ n e. NN A ) = sup ( ran S , RR* , < ) ) |