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	⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ ↔ ( ( 𝐹 ''' 𝐴 ) = ∅ ∨ ( 𝐹 ''' 𝐴 ) = V ) )

Proof

Step	Hyp	Ref	Expression
1		ioran	⊢ ( ¬ ( ( 𝐹 ''' 𝐴 ) = ∅ ∨ ( 𝐹 ''' 𝐴 ) = V ) ↔ ( ¬ ( 𝐹 ''' 𝐴 ) = ∅ ∧ ¬ ( 𝐹 ''' 𝐴 ) = V ) )
2		df-ne	⊢ ( ( 𝐹 ''' 𝐴 ) ≠ V ↔ ¬ ( 𝐹 ''' 𝐴 ) = V )
3		afvnufveq	⊢ ( ( 𝐹 ''' 𝐴 ) ≠ V → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
4	2 3	sylbir	⊢ ( ¬ ( 𝐹 ''' 𝐴 ) = V → ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
5		eqeq1	⊢ ( ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) → ( ( 𝐹 ''' 𝐴 ) = ∅ ↔ ( 𝐹 ‘ 𝐴 ) = ∅ ) )
6	5	notbid	⊢ ( ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) → ( ¬ ( 𝐹 ''' 𝐴 ) = ∅ ↔ ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) )
7	6	biimpd	⊢ ( ( 𝐹 ''' 𝐴 ) = ( 𝐹 ‘ 𝐴 ) → ( ¬ ( 𝐹 ''' 𝐴 ) = ∅ → ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) )
8	4 7	syl	⊢ ( ¬ ( 𝐹 ''' 𝐴 ) = V → ( ¬ ( 𝐹 ''' 𝐴 ) = ∅ → ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) )
9	8	impcom	⊢ ( ( ¬ ( 𝐹 ''' 𝐴 ) = ∅ ∧ ¬ ( 𝐹 ''' 𝐴 ) = V ) → ¬ ( 𝐹 ‘ 𝐴 ) = ∅ )
10	1 9	sylbi	⊢ ( ¬ ( ( 𝐹 ''' 𝐴 ) = ∅ ∨ ( 𝐹 ''' 𝐴 ) = V ) → ¬ ( 𝐹 ‘ 𝐴 ) = ∅ )
11	10	con4i	⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ → ( ( 𝐹 ''' 𝐴 ) = ∅ ∨ ( 𝐹 ''' 𝐴 ) = V ) )
12		afv0fv0	⊢ ( ( 𝐹 ''' 𝐴 ) = ∅ → ( 𝐹 ‘ 𝐴 ) = ∅ )
13		afvpcfv0	⊢ ( ( 𝐹 ''' 𝐴 ) = V → ( 𝐹 ‘ 𝐴 ) = ∅ )
14	12 13	jaoi	⊢ ( ( ( 𝐹 ''' 𝐴 ) = ∅ ∨ ( 𝐹 ''' 𝐴 ) = V ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
15	11 14	impbii	⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ ↔ ( ( 𝐹 ''' 𝐴 ) = ∅ ∨ ( 𝐹 ''' 𝐴 ) = V ) )