| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-rn |
|- ran F = dom `' F |
| 2 |
1
|
ineq1i |
|- ( ran F i^i ( A i^i ran F ) ) = ( dom `' F i^i ( A i^i ran F ) ) |
| 3 |
|
dfss2 |
|- ( A C_ ran F <-> ( A i^i ran F ) = A ) |
| 4 |
3
|
biimpi |
|- ( A C_ ran F -> ( A i^i ran F ) = A ) |
| 5 |
4
|
ineq2d |
|- ( A C_ ran F -> ( ran F i^i ( A i^i ran F ) ) = ( ran F i^i A ) ) |
| 6 |
|
sseqin2 |
|- ( A C_ ran F <-> ( ran F i^i A ) = A ) |
| 7 |
6
|
biimpi |
|- ( A C_ ran F -> ( ran F i^i A ) = A ) |
| 8 |
5 7
|
eqtrd |
|- ( A C_ ran F -> ( ran F i^i ( A i^i ran F ) ) = A ) |
| 9 |
8
|
3ad2ant2 |
|- ( ( Fun F /\ A C_ ran F /\ ( `' F " A ) = (/) ) -> ( ran F i^i ( A i^i ran F ) ) = A ) |
| 10 |
|
fimacnvinrn |
|- ( Fun F -> ( `' F " A ) = ( `' F " ( A i^i ran F ) ) ) |
| 11 |
10
|
eqeq1d |
|- ( Fun F -> ( ( `' F " A ) = (/) <-> ( `' F " ( A i^i ran F ) ) = (/) ) ) |
| 12 |
11
|
biimpa |
|- ( ( Fun F /\ ( `' F " A ) = (/) ) -> ( `' F " ( A i^i ran F ) ) = (/) ) |
| 13 |
12
|
3adant2 |
|- ( ( Fun F /\ A C_ ran F /\ ( `' F " A ) = (/) ) -> ( `' F " ( A i^i ran F ) ) = (/) ) |
| 14 |
|
imadisj |
|- ( ( `' F " ( A i^i ran F ) ) = (/) <-> ( dom `' F i^i ( A i^i ran F ) ) = (/) ) |
| 15 |
13 14
|
sylib |
|- ( ( Fun F /\ A C_ ran F /\ ( `' F " A ) = (/) ) -> ( dom `' F i^i ( A i^i ran F ) ) = (/) ) |
| 16 |
2 9 15
|
3eqtr3a |
|- ( ( Fun F /\ A C_ ran F /\ ( `' F " A ) = (/) ) -> A = (/) ) |
| 17 |
16
|
3expia |
|- ( ( Fun F /\ A C_ ran F ) -> ( ( `' F " A ) = (/) -> A = (/) ) ) |
| 18 |
17
|
necon3d |
|- ( ( Fun F /\ A C_ ran F ) -> ( A =/= (/) -> ( `' F " A ) =/= (/) ) ) |
| 19 |
18
|
3impia |
|- ( ( Fun F /\ A C_ ran F /\ A =/= (/) ) -> ( `' F " A ) =/= (/) ) |