Metamath Proof Explorer


Theorem ndfatafv2undef

Description: The alternate function value at a class A is undefined if the function, whose range is a set, is not defined at A . (Contributed by AV, 2-Sep-2022)

Ref Expression
Assertion ndfatafv2undef ( ( ran 𝐹𝑉 ∧ ¬ 𝐹 defAt 𝐴 ) → ( 𝐹 '''' 𝐴 ) = ( Undef ‘ ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ndfatafv2 ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = 𝒫 ran 𝐹 )
2 undefval ( ran 𝐹𝑉 → ( Undef ‘ ran 𝐹 ) = 𝒫 ran 𝐹 )
3 2 eqcomd ( ran 𝐹𝑉 → 𝒫 ran 𝐹 = ( Undef ‘ ran 𝐹 ) )
4 1 3 sylan9eqr ( ( ran 𝐹𝑉 ∧ ¬ 𝐹 defAt 𝐴 ) → ( 𝐹 '''' 𝐴 ) = ( Undef ‘ ran 𝐹 ) )