Step |
Hyp |
Ref |
Expression |
1 |
|
fo1st |
|- 1st : _V -onto-> _V |
2 |
|
fofn |
|- ( 1st : _V -onto-> _V -> 1st Fn _V ) |
3 |
1 2
|
ax-mp |
|- 1st Fn _V |
4 |
|
ffn |
|- ( F : A --> ( B X. C ) -> F Fn A ) |
5 |
|
dffn2 |
|- ( F Fn A <-> F : A --> _V ) |
6 |
4 5
|
sylib |
|- ( F : A --> ( B X. C ) -> F : A --> _V ) |
7 |
|
fnfco |
|- ( ( 1st Fn _V /\ F : A --> _V ) -> ( 1st o. F ) Fn A ) |
8 |
3 6 7
|
sylancr |
|- ( F : A --> ( B X. C ) -> ( 1st o. F ) Fn A ) |
9 |
|
rnco |
|- ran ( 1st o. F ) = ran ( 1st |` ran F ) |
10 |
|
frn |
|- ( F : A --> ( B X. C ) -> ran F C_ ( B X. C ) ) |
11 |
|
ssres2 |
|- ( ran F C_ ( B X. C ) -> ( 1st |` ran F ) C_ ( 1st |` ( B X. C ) ) ) |
12 |
|
rnss |
|- ( ( 1st |` ran F ) C_ ( 1st |` ( B X. C ) ) -> ran ( 1st |` ran F ) C_ ran ( 1st |` ( B X. C ) ) ) |
13 |
10 11 12
|
3syl |
|- ( F : A --> ( B X. C ) -> ran ( 1st |` ran F ) C_ ran ( 1st |` ( B X. C ) ) ) |
14 |
|
f1stres |
|- ( 1st |` ( B X. C ) ) : ( B X. C ) --> B |
15 |
|
frn |
|- ( ( 1st |` ( B X. C ) ) : ( B X. C ) --> B -> ran ( 1st |` ( B X. C ) ) C_ B ) |
16 |
14 15
|
ax-mp |
|- ran ( 1st |` ( B X. C ) ) C_ B |
17 |
13 16
|
sstrdi |
|- ( F : A --> ( B X. C ) -> ran ( 1st |` ran F ) C_ B ) |
18 |
9 17
|
eqsstrid |
|- ( F : A --> ( B X. C ) -> ran ( 1st o. F ) C_ B ) |
19 |
|
df-f |
|- ( ( 1st o. F ) : A --> B <-> ( ( 1st o. F ) Fn A /\ ran ( 1st o. F ) C_ B ) ) |
20 |
8 18 19
|
sylanbrc |
|- ( F : A --> ( B X. C ) -> ( 1st o. F ) : A --> B ) |