Step |
Hyp |
Ref |
Expression |
1 |
|
ioran |
|- ( -. ( ( F ''' A ) = (/) \/ ( F ''' A ) = _V ) <-> ( -. ( F ''' A ) = (/) /\ -. ( F ''' A ) = _V ) ) |
2 |
|
df-ne |
|- ( ( F ''' A ) =/= _V <-> -. ( F ''' A ) = _V ) |
3 |
|
afvnufveq |
|- ( ( F ''' A ) =/= _V -> ( F ''' A ) = ( F ` A ) ) |
4 |
2 3
|
sylbir |
|- ( -. ( F ''' A ) = _V -> ( F ''' A ) = ( F ` A ) ) |
5 |
|
eqeq1 |
|- ( ( F ''' A ) = ( F ` A ) -> ( ( F ''' A ) = (/) <-> ( F ` A ) = (/) ) ) |
6 |
5
|
notbid |
|- ( ( F ''' A ) = ( F ` A ) -> ( -. ( F ''' A ) = (/) <-> -. ( F ` A ) = (/) ) ) |
7 |
6
|
biimpd |
|- ( ( F ''' A ) = ( F ` A ) -> ( -. ( F ''' A ) = (/) -> -. ( F ` A ) = (/) ) ) |
8 |
4 7
|
syl |
|- ( -. ( F ''' A ) = _V -> ( -. ( F ''' A ) = (/) -> -. ( F ` A ) = (/) ) ) |
9 |
8
|
impcom |
|- ( ( -. ( F ''' A ) = (/) /\ -. ( F ''' A ) = _V ) -> -. ( F ` A ) = (/) ) |
10 |
1 9
|
sylbi |
|- ( -. ( ( F ''' A ) = (/) \/ ( F ''' A ) = _V ) -> -. ( F ` A ) = (/) ) |
11 |
10
|
con4i |
|- ( ( F ` A ) = (/) -> ( ( F ''' A ) = (/) \/ ( F ''' A ) = _V ) ) |
12 |
|
afv0fv0 |
|- ( ( F ''' A ) = (/) -> ( F ` A ) = (/) ) |
13 |
|
afvpcfv0 |
|- ( ( F ''' A ) = _V -> ( F ` A ) = (/) ) |
14 |
12 13
|
jaoi |
|- ( ( ( F ''' A ) = (/) \/ ( F ''' A ) = _V ) -> ( F ` A ) = (/) ) |
15 |
11 14
|
impbii |
|- ( ( F ` A ) = (/) <-> ( ( F ''' A ) = (/) \/ ( F ''' A ) = _V ) ) |