Step |
Hyp |
Ref |
Expression |
1 |
|
brdom2 |
|- ( A ~<_ NN <-> ( A ~< NN \/ A ~~ NN ) ) |
2 |
|
nnenom |
|- NN ~~ _om |
3 |
|
sdomentr |
|- ( ( A ~< NN /\ NN ~~ _om ) -> A ~< _om ) |
4 |
2 3
|
mpan2 |
|- ( A ~< NN -> A ~< _om ) |
5 |
|
isfinite |
|- ( A e. Fin <-> A ~< _om ) |
6 |
|
finiunmbl |
|- ( ( A e. Fin /\ A. n e. A B e. dom vol ) -> U_ n e. A B e. dom vol ) |
7 |
6
|
ex |
|- ( A e. Fin -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) ) |
8 |
5 7
|
sylbir |
|- ( A ~< _om -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) ) |
9 |
4 8
|
syl |
|- ( A ~< NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) ) |
10 |
|
bren |
|- ( A ~~ NN <-> E. f f : A -1-1-onto-> NN ) |
11 |
|
nfv |
|- F/ n f : A -1-1-onto-> NN |
12 |
|
nfcv |
|- F/_ n NN |
13 |
|
nfcsb1v |
|- F/_ n [_ ( `' f ` k ) / n ]_ B |
14 |
13
|
nfcri |
|- F/ n x e. [_ ( `' f ` k ) / n ]_ B |
15 |
12 14
|
nfrex |
|- F/ n E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B |
16 |
|
f1of |
|- ( f : A -1-1-onto-> NN -> f : A --> NN ) |
17 |
16
|
ffvelrnda |
|- ( ( f : A -1-1-onto-> NN /\ n e. A ) -> ( f ` n ) e. NN ) |
18 |
17
|
3adant3 |
|- ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> ( f ` n ) e. NN ) |
19 |
|
simp3 |
|- ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> x e. B ) |
20 |
|
f1ocnvfv1 |
|- ( ( f : A -1-1-onto-> NN /\ n e. A ) -> ( `' f ` ( f ` n ) ) = n ) |
21 |
20
|
3adant3 |
|- ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> ( `' f ` ( f ` n ) ) = n ) |
22 |
21
|
eqcomd |
|- ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> n = ( `' f ` ( f ` n ) ) ) |
23 |
|
csbeq1a |
|- ( n = ( `' f ` ( f ` n ) ) -> B = [_ ( `' f ` ( f ` n ) ) / n ]_ B ) |
24 |
22 23
|
syl |
|- ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> B = [_ ( `' f ` ( f ` n ) ) / n ]_ B ) |
25 |
19 24
|
eleqtrd |
|- ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> x e. [_ ( `' f ` ( f ` n ) ) / n ]_ B ) |
26 |
|
fveq2 |
|- ( k = ( f ` n ) -> ( `' f ` k ) = ( `' f ` ( f ` n ) ) ) |
27 |
26
|
csbeq1d |
|- ( k = ( f ` n ) -> [_ ( `' f ` k ) / n ]_ B = [_ ( `' f ` ( f ` n ) ) / n ]_ B ) |
28 |
27
|
eleq2d |
|- ( k = ( f ` n ) -> ( x e. [_ ( `' f ` k ) / n ]_ B <-> x e. [_ ( `' f ` ( f ` n ) ) / n ]_ B ) ) |
29 |
28
|
rspcev |
|- ( ( ( f ` n ) e. NN /\ x e. [_ ( `' f ` ( f ` n ) ) / n ]_ B ) -> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B ) |
30 |
18 25 29
|
syl2anc |
|- ( ( f : A -1-1-onto-> NN /\ n e. A /\ x e. B ) -> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B ) |
31 |
30
|
3exp |
|- ( f : A -1-1-onto-> NN -> ( n e. A -> ( x e. B -> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B ) ) ) |
32 |
11 15 31
|
rexlimd |
|- ( f : A -1-1-onto-> NN -> ( E. n e. A x e. B -> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B ) ) |
33 |
|
f1ocnvdm |
|- ( ( f : A -1-1-onto-> NN /\ k e. NN ) -> ( `' f ` k ) e. A ) |
34 |
|
csbeq1a |
|- ( n = ( `' f ` k ) -> B = [_ ( `' f ` k ) / n ]_ B ) |
35 |
34
|
eleq2d |
|- ( n = ( `' f ` k ) -> ( x e. B <-> x e. [_ ( `' f ` k ) / n ]_ B ) ) |
36 |
14 35
|
rspce |
|- ( ( ( `' f ` k ) e. A /\ x e. [_ ( `' f ` k ) / n ]_ B ) -> E. n e. A x e. B ) |
37 |
36
|
ex |
|- ( ( `' f ` k ) e. A -> ( x e. [_ ( `' f ` k ) / n ]_ B -> E. n e. A x e. B ) ) |
38 |
33 37
|
syl |
|- ( ( f : A -1-1-onto-> NN /\ k e. NN ) -> ( x e. [_ ( `' f ` k ) / n ]_ B -> E. n e. A x e. B ) ) |
39 |
38
|
rexlimdva |
|- ( f : A -1-1-onto-> NN -> ( E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B -> E. n e. A x e. B ) ) |
40 |
32 39
|
impbid |
|- ( f : A -1-1-onto-> NN -> ( E. n e. A x e. B <-> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B ) ) |
41 |
|
eliun |
|- ( x e. U_ n e. A B <-> E. n e. A x e. B ) |
42 |
|
eliun |
|- ( x e. U_ k e. NN [_ ( `' f ` k ) / n ]_ B <-> E. k e. NN x e. [_ ( `' f ` k ) / n ]_ B ) |
43 |
40 41 42
|
3bitr4g |
|- ( f : A -1-1-onto-> NN -> ( x e. U_ n e. A B <-> x e. U_ k e. NN [_ ( `' f ` k ) / n ]_ B ) ) |
44 |
43
|
eqrdv |
|- ( f : A -1-1-onto-> NN -> U_ n e. A B = U_ k e. NN [_ ( `' f ` k ) / n ]_ B ) |
45 |
44
|
adantr |
|- ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) -> U_ n e. A B = U_ k e. NN [_ ( `' f ` k ) / n ]_ B ) |
46 |
|
rspcsbela |
|- ( ( ( `' f ` k ) e. A /\ A. n e. A B e. dom vol ) -> [_ ( `' f ` k ) / n ]_ B e. dom vol ) |
47 |
33 46
|
sylan |
|- ( ( ( f : A -1-1-onto-> NN /\ k e. NN ) /\ A. n e. A B e. dom vol ) -> [_ ( `' f ` k ) / n ]_ B e. dom vol ) |
48 |
47
|
an32s |
|- ( ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) /\ k e. NN ) -> [_ ( `' f ` k ) / n ]_ B e. dom vol ) |
49 |
48
|
ralrimiva |
|- ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) -> A. k e. NN [_ ( `' f ` k ) / n ]_ B e. dom vol ) |
50 |
|
iunmbl |
|- ( A. k e. NN [_ ( `' f ` k ) / n ]_ B e. dom vol -> U_ k e. NN [_ ( `' f ` k ) / n ]_ B e. dom vol ) |
51 |
49 50
|
syl |
|- ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) -> U_ k e. NN [_ ( `' f ` k ) / n ]_ B e. dom vol ) |
52 |
45 51
|
eqeltrd |
|- ( ( f : A -1-1-onto-> NN /\ A. n e. A B e. dom vol ) -> U_ n e. A B e. dom vol ) |
53 |
52
|
ex |
|- ( f : A -1-1-onto-> NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) ) |
54 |
53
|
exlimiv |
|- ( E. f f : A -1-1-onto-> NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) ) |
55 |
10 54
|
sylbi |
|- ( A ~~ NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) ) |
56 |
9 55
|
jaoi |
|- ( ( A ~< NN \/ A ~~ NN ) -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) ) |
57 |
1 56
|
sylbi |
|- ( A ~<_ NN -> ( A. n e. A B e. dom vol -> U_ n e. A B e. dom vol ) ) |
58 |
57
|
imp |
|- ( ( A ~<_ NN /\ A. n e. A B e. dom vol ) -> U_ n e. A B e. dom vol ) |