Step |
Hyp |
Ref |
Expression |
1 |
|
i1ff |
|- ( F e. dom S.1 -> F : RR --> RR ) |
2 |
|
ffun |
|- ( F : RR --> RR -> Fun F ) |
3 |
|
inpreima |
|- ( Fun F -> ( `' F " ( A i^i ran F ) ) = ( ( `' F " A ) i^i ( `' F " ran F ) ) ) |
4 |
|
iunid |
|- U_ y e. ( A i^i ran F ) { y } = ( A i^i ran F ) |
5 |
4
|
imaeq2i |
|- ( `' F " U_ y e. ( A i^i ran F ) { y } ) = ( `' F " ( A i^i ran F ) ) |
6 |
|
imaiun |
|- ( `' F " U_ y e. ( A i^i ran F ) { y } ) = U_ y e. ( A i^i ran F ) ( `' F " { y } ) |
7 |
5 6
|
eqtr3i |
|- ( `' F " ( A i^i ran F ) ) = U_ y e. ( A i^i ran F ) ( `' F " { y } ) |
8 |
|
cnvimass |
|- ( `' F " A ) C_ dom F |
9 |
|
cnvimarndm |
|- ( `' F " ran F ) = dom F |
10 |
8 9
|
sseqtrri |
|- ( `' F " A ) C_ ( `' F " ran F ) |
11 |
|
df-ss |
|- ( ( `' F " A ) C_ ( `' F " ran F ) <-> ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( `' F " A ) ) |
12 |
10 11
|
mpbi |
|- ( ( `' F " A ) i^i ( `' F " ran F ) ) = ( `' F " A ) |
13 |
3 7 12
|
3eqtr3g |
|- ( Fun F -> U_ y e. ( A i^i ran F ) ( `' F " { y } ) = ( `' F " A ) ) |
14 |
1 2 13
|
3syl |
|- ( F e. dom S.1 -> U_ y e. ( A i^i ran F ) ( `' F " { y } ) = ( `' F " A ) ) |
15 |
|
i1frn |
|- ( F e. dom S.1 -> ran F e. Fin ) |
16 |
|
inss2 |
|- ( A i^i ran F ) C_ ran F |
17 |
|
ssfi |
|- ( ( ran F e. Fin /\ ( A i^i ran F ) C_ ran F ) -> ( A i^i ran F ) e. Fin ) |
18 |
15 16 17
|
sylancl |
|- ( F e. dom S.1 -> ( A i^i ran F ) e. Fin ) |
19 |
|
i1fmbf |
|- ( F e. dom S.1 -> F e. MblFn ) |
20 |
19
|
adantr |
|- ( ( F e. dom S.1 /\ y e. ( A i^i ran F ) ) -> F e. MblFn ) |
21 |
1
|
adantr |
|- ( ( F e. dom S.1 /\ y e. ( A i^i ran F ) ) -> F : RR --> RR ) |
22 |
1
|
frnd |
|- ( F e. dom S.1 -> ran F C_ RR ) |
23 |
16 22
|
sstrid |
|- ( F e. dom S.1 -> ( A i^i ran F ) C_ RR ) |
24 |
23
|
sselda |
|- ( ( F e. dom S.1 /\ y e. ( A i^i ran F ) ) -> y e. RR ) |
25 |
|
mbfimasn |
|- ( ( F e. MblFn /\ F : RR --> RR /\ y e. RR ) -> ( `' F " { y } ) e. dom vol ) |
26 |
20 21 24 25
|
syl3anc |
|- ( ( F e. dom S.1 /\ y e. ( A i^i ran F ) ) -> ( `' F " { y } ) e. dom vol ) |
27 |
26
|
ralrimiva |
|- ( F e. dom S.1 -> A. y e. ( A i^i ran F ) ( `' F " { y } ) e. dom vol ) |
28 |
|
finiunmbl |
|- ( ( ( A i^i ran F ) e. Fin /\ A. y e. ( A i^i ran F ) ( `' F " { y } ) e. dom vol ) -> U_ y e. ( A i^i ran F ) ( `' F " { y } ) e. dom vol ) |
29 |
18 27 28
|
syl2anc |
|- ( F e. dom S.1 -> U_ y e. ( A i^i ran F ) ( `' F " { y } ) e. dom vol ) |
30 |
14 29
|
eqeltrrd |
|- ( F e. dom S.1 -> ( `' F " A ) e. dom vol ) |