Step |
Hyp |
Ref |
Expression |
1 |
|
fifo.1 |
|- F = ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| y ) |
2 |
|
eldifsni |
|- ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) -> y =/= (/) ) |
3 |
|
intex |
|- ( y =/= (/) <-> |^| y e. _V ) |
4 |
2 3
|
sylib |
|- ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) -> |^| y e. _V ) |
5 |
4
|
rgen |
|- A. y e. ( ( ~P A i^i Fin ) \ { (/) } ) |^| y e. _V |
6 |
1
|
fnmpt |
|- ( A. y e. ( ( ~P A i^i Fin ) \ { (/) } ) |^| y e. _V -> F Fn ( ( ~P A i^i Fin ) \ { (/) } ) ) |
7 |
5 6
|
mp1i |
|- ( A e. V -> F Fn ( ( ~P A i^i Fin ) \ { (/) } ) ) |
8 |
|
dffn4 |
|- ( F Fn ( ( ~P A i^i Fin ) \ { (/) } ) <-> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ran F ) |
9 |
7 8
|
sylib |
|- ( A e. V -> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ran F ) |
10 |
|
elfi2 |
|- ( A e. V -> ( x e. ( fi ` A ) <-> E. y e. ( ( ~P A i^i Fin ) \ { (/) } ) x = |^| y ) ) |
11 |
1
|
elrnmpt |
|- ( x e. _V -> ( x e. ran F <-> E. y e. ( ( ~P A i^i Fin ) \ { (/) } ) x = |^| y ) ) |
12 |
11
|
elv |
|- ( x e. ran F <-> E. y e. ( ( ~P A i^i Fin ) \ { (/) } ) x = |^| y ) |
13 |
10 12
|
bitr4di |
|- ( A e. V -> ( x e. ( fi ` A ) <-> x e. ran F ) ) |
14 |
13
|
eqrdv |
|- ( A e. V -> ( fi ` A ) = ran F ) |
15 |
|
foeq3 |
|- ( ( fi ` A ) = ran F -> ( F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) <-> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ran F ) ) |
16 |
14 15
|
syl |
|- ( A e. V -> ( F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) <-> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ran F ) ) |
17 |
9 16
|
mpbird |
|- ( A e. V -> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) ) |