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