Metamath Proof Explorer


Theorem afvfv0bi

Description: The function's value at an argument is the empty set if and only if the value of the alternative function at this argument is either the empty set or the universe. (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion afvfv0bi
|- ( ( F ` A ) = (/) <-> ( ( F ''' A ) = (/) \/ ( F ''' A ) = _V ) )

Proof

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 ) )