Metamath Proof Explorer


Theorem ndfatafv2nrn

Description: The alternate function value at a class A at which the function is not defined is undefined, i.e., not in the range of the function. (Contributed by AV, 2-Sep-2022)

Ref Expression
Assertion ndfatafv2nrn ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 ndfatafv2 ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = 𝒫 ran 𝐹 )
2 pwuninel ¬ 𝒫 ran 𝐹 ∈ ran 𝐹
3 df-nel ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ¬ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 )
4 eleq1 ( ( 𝐹 '''' 𝐴 ) = 𝒫 ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ 𝒫 ran 𝐹 ∈ ran 𝐹 ) )
5 4 notbid ( ( 𝐹 '''' 𝐴 ) = 𝒫 ran 𝐹 → ( ¬ ( 𝐹 '''' 𝐴 ) ∈ ran 𝐹 ↔ ¬ 𝒫 ran 𝐹 ∈ ran 𝐹 ) )
6 3 5 syl5bb ( ( 𝐹 '''' 𝐴 ) = 𝒫 ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ↔ ¬ 𝒫 ran 𝐹 ∈ ran 𝐹 ) )
7 2 6 mpbiri ( ( 𝐹 '''' 𝐴 ) = 𝒫 ran 𝐹 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )
8 1 7 syl ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )