Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> F : A -1-1-> B ) |
2 |
|
f1f |
|- ( F : A -1-1-> B -> F : A --> B ) |
3 |
2
|
adantl |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> F : A --> B ) |
4 |
3
|
ffnd |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> F Fn A ) |
5 |
|
simpll |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> A ~~ B ) |
6 |
3
|
frnd |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> ran F C_ B ) |
7 |
|
df-pss |
|- ( ran F C. B <-> ( ran F C_ B /\ ran F =/= B ) ) |
8 |
7
|
baib |
|- ( ran F C_ B -> ( ran F C. B <-> ran F =/= B ) ) |
9 |
6 8
|
syl |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> ( ran F C. B <-> ran F =/= B ) ) |
10 |
|
simplr |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> B e. Fin ) |
11 |
|
relen |
|- Rel ~~ |
12 |
11
|
brrelex1i |
|- ( A ~~ B -> A e. _V ) |
13 |
5 12
|
syl |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> A e. _V ) |
14 |
10 13
|
elmapd |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> ( F e. ( B ^m A ) <-> F : A --> B ) ) |
15 |
3 14
|
mpbird |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> F e. ( B ^m A ) ) |
16 |
|
f1f1orn |
|- ( F : A -1-1-> B -> F : A -1-1-onto-> ran F ) |
17 |
16
|
adantl |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> F : A -1-1-onto-> ran F ) |
18 |
|
f1oen3g |
|- ( ( F e. ( B ^m A ) /\ F : A -1-1-onto-> ran F ) -> A ~~ ran F ) |
19 |
15 17 18
|
syl2anc |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> A ~~ ran F ) |
20 |
|
php3 |
|- ( ( B e. Fin /\ ran F C. B ) -> ran F ~< B ) |
21 |
20
|
ex |
|- ( B e. Fin -> ( ran F C. B -> ran F ~< B ) ) |
22 |
10 21
|
syl |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> ( ran F C. B -> ran F ~< B ) ) |
23 |
|
ensdomtr |
|- ( ( A ~~ ran F /\ ran F ~< B ) -> A ~< B ) |
24 |
19 22 23
|
syl6an |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> ( ran F C. B -> A ~< B ) ) |
25 |
|
sdomnen |
|- ( A ~< B -> -. A ~~ B ) |
26 |
24 25
|
syl6 |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> ( ran F C. B -> -. A ~~ B ) ) |
27 |
9 26
|
sylbird |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> ( ran F =/= B -> -. A ~~ B ) ) |
28 |
27
|
necon4ad |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> ( A ~~ B -> ran F = B ) ) |
29 |
5 28
|
mpd |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> ran F = B ) |
30 |
|
df-fo |
|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) ) |
31 |
4 29 30
|
sylanbrc |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> F : A -onto-> B ) |
32 |
|
df-f1o |
|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) ) |
33 |
1 31 32
|
sylanbrc |
|- ( ( ( A ~~ B /\ B e. Fin ) /\ F : A -1-1-> B ) -> F : A -1-1-onto-> B ) |
34 |
33
|
ex |
|- ( ( A ~~ B /\ B e. Fin ) -> ( F : A -1-1-> B -> F : A -1-1-onto-> B ) ) |
35 |
|
f1of1 |
|- ( F : A -1-1-onto-> B -> F : A -1-1-> B ) |
36 |
34 35
|
impbid1 |
|- ( ( A ~~ B /\ B e. Fin ) -> ( F : A -1-1-> B <-> F : A -1-1-onto-> B ) ) |