| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dff1o4 |
|- ( F : (/) -1-1-onto-> A <-> ( F Fn (/) /\ `' F Fn A ) ) |
| 2 |
|
fn0 |
|- ( F Fn (/) <-> F = (/) ) |
| 3 |
2
|
birani |
|- ( ( F Fn (/) /\ `' F Fn A ) -> F = (/) ) |
| 4 |
|
cnveq |
|- ( F = (/) -> `' F = `' (/) ) |
| 5 |
|
cnv0 |
|- `' (/) = (/) |
| 6 |
4 5
|
eqtrdi |
|- ( F = (/) -> `' F = (/) ) |
| 7 |
2 6
|
sylbi |
|- ( F Fn (/) -> `' F = (/) ) |
| 8 |
7
|
fneq1d |
|- ( F Fn (/) -> ( `' F Fn A <-> (/) Fn A ) ) |
| 9 |
8
|
biimpa |
|- ( ( F Fn (/) /\ `' F Fn A ) -> (/) Fn A ) |
| 10 |
9
|
fndmd |
|- ( ( F Fn (/) /\ `' F Fn A ) -> dom (/) = A ) |
| 11 |
|
dm0 |
|- dom (/) = (/) |
| 12 |
10 11
|
eqtr3di |
|- ( ( F Fn (/) /\ `' F Fn A ) -> A = (/) ) |
| 13 |
3 12
|
jca |
|- ( ( F Fn (/) /\ `' F Fn A ) -> ( F = (/) /\ A = (/) ) ) |
| 14 |
2
|
biranri |
|- ( ( F = (/) /\ A = (/) ) -> F Fn (/) ) |
| 15 |
|
eqid |
|- (/) = (/) |
| 16 |
|
fn0 |
|- ( (/) Fn (/) <-> (/) = (/) ) |
| 17 |
15 16
|
mpbir |
|- (/) Fn (/) |
| 18 |
6
|
fneq1d |
|- ( F = (/) -> ( `' F Fn A <-> (/) Fn A ) ) |
| 19 |
|
fneq2 |
|- ( A = (/) -> ( (/) Fn A <-> (/) Fn (/) ) ) |
| 20 |
18 19
|
sylan9bb |
|- ( ( F = (/) /\ A = (/) ) -> ( `' F Fn A <-> (/) Fn (/) ) ) |
| 21 |
17 20
|
mpbiri |
|- ( ( F = (/) /\ A = (/) ) -> `' F Fn A ) |
| 22 |
14 21
|
jca |
|- ( ( F = (/) /\ A = (/) ) -> ( F Fn (/) /\ `' F Fn A ) ) |
| 23 |
13 22
|
impbii |
|- ( ( F Fn (/) /\ `' F Fn A ) <-> ( F = (/) /\ A = (/) ) ) |
| 24 |
1 23
|
bitri |
|- ( F : (/) -1-1-onto-> A <-> ( F = (/) /\ A = (/) ) ) |