Theorem afvpcfv0

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

	Ref	Expression
Assertion	afvpcfv0	⊢ ( ( 𝐹 ''' 𝐴 ) = V → ( 𝐹 ‘ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		dfafv2	⊢ ( 𝐹 ''' 𝐴 ) = if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V )
2	1	eqeq1i	⊢ ( ( 𝐹 ''' 𝐴 ) = V ↔ if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) = V )
3		eqcom	⊢ ( if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) = V ↔ V = if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) )
4		eqif	⊢ ( V = if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) ↔ ( ( 𝐹 defAt 𝐴 ∧ V = ( 𝐹 ‘ 𝐴 ) ) ∨ ( ¬ 𝐹 defAt 𝐴 ∧ V = V ) ) )
5	3 4	bitri	⊢ ( if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) = V ↔ ( ( 𝐹 defAt 𝐴 ∧ V = ( 𝐹 ‘ 𝐴 ) ) ∨ ( ¬ 𝐹 defAt 𝐴 ∧ V = V ) ) )
6		fveqvfvv	⊢ ( ( 𝐹 ‘ 𝐴 ) = V → ( 𝐹 ‘ 𝐴 ) = ∅ )
7	6	eqcoms	⊢ ( V = ( 𝐹 ‘ 𝐴 ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
8	7	adantl	⊢ ( ( 𝐹 defAt 𝐴 ∧ V = ( 𝐹 ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
9		fvfundmfvn0	⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
10		df-dfat	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
11	9 10	sylibr	⊢ ( ( 𝐹 ‘ 𝐴 ) ≠ ∅ → 𝐹 defAt 𝐴 )
12	11	necon1bi	⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 ‘ 𝐴 ) = ∅ )
13	12	adantr	⊢ ( ( ¬ 𝐹 defAt 𝐴 ∧ V = V ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
14	8 13	jaoi	⊢ ( ( ( 𝐹 defAt 𝐴 ∧ V = ( 𝐹 ‘ 𝐴 ) ) ∨ ( ¬ 𝐹 defAt 𝐴 ∧ V = V ) ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
15	5 14	sylbi	⊢ ( if ( 𝐹 defAt 𝐴 , ( 𝐹 ‘ 𝐴 ) , V ) = V → ( 𝐹 ‘ 𝐴 ) = ∅ )
16	2 15	sylbi	⊢ ( ( 𝐹 ''' 𝐴 ) = V → ( 𝐹 ‘ 𝐴 ) = ∅ )